Proof of Theorem estrres
Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . 3
⊢ (𝐶 ↾s 𝐴) ∈ V |
2 | | estrres.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝑊) |
3 | | setsval 15720 |
. . 3
⊢ (((𝐶 ↾s 𝐴) ∈ V ∧ 𝐺 ∈ 𝑊) → ((𝐶 ↾s 𝐴) sSet 〈(Hom ‘ndx), 𝐺〉) = (((𝐶 ↾s 𝐴) ↾ (V ∖ {(Hom ‘ndx)}))
∪ {〈(Hom ‘ndx), 𝐺〉})) |
4 | 1, 2, 3 | sylancr 694 |
. 2
⊢ (𝜑 → ((𝐶 ↾s 𝐴) sSet 〈(Hom ‘ndx), 𝐺〉) = (((𝐶 ↾s 𝐴) ↾ (V ∖ {(Hom ‘ndx)}))
∪ {〈(Hom ‘ndx), 𝐺〉})) |
5 | | eqid 2610 |
. . . . . 6
⊢ (𝐶 ↾s 𝐴) = (𝐶 ↾s 𝐴) |
6 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
7 | | eqid 2610 |
. . . . . 6
⊢
(Base‘ndx) = (Base‘ndx) |
8 | | estrres.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |
9 | | tpex 6855 |
. . . . . . 7
⊢
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∈ V |
10 | 8, 9 | syl6eqel 2696 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ V) |
11 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘ndx) ∈ V |
12 | | fvex 6113 |
. . . . . . . . . 10
⊢ (Hom
‘ndx) ∈ V |
13 | | fvex 6113 |
. . . . . . . . . 10
⊢
(comp‘ndx) ∈ V |
14 | 11, 12, 13 | 3pm3.2i 1232 |
. . . . . . . . 9
⊢
((Base‘ndx) ∈ V ∧ (Hom ‘ndx) ∈ V ∧
(comp‘ndx) ∈ V) |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ((Base‘ndx) ∈ V
∧ (Hom ‘ndx) ∈ V ∧ (comp‘ndx) ∈
V)) |
16 | | estrres.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
17 | | estrres.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ 𝑋) |
18 | | estrres.x |
. . . . . . . 8
⊢ (𝜑 → · ∈ 𝑌) |
19 | | slotsbhcdif 15903 |
. . . . . . . . 9
⊢
((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) |
20 | 19 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ((Base‘ndx) ≠
(Hom ‘ndx) ∧ (Base‘ndx) ≠ (comp‘ndx) ∧ (Hom
‘ndx) ≠ (comp‘ndx))) |
21 | | funtpg 5856 |
. . . . . . . 8
⊢
((((Base‘ndx) ∈ V ∧ (Hom ‘ndx) ∈ V ∧
(comp‘ndx) ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝐻 ∈ 𝑋 ∧ · ∈ 𝑌) ∧ ((Base‘ndx) ≠
(Hom ‘ndx) ∧ (Base‘ndx) ≠ (comp‘ndx) ∧ (Hom
‘ndx) ≠ (comp‘ndx))) → Fun {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |
22 | 15, 16, 17, 18, 20, 21 | syl131anc 1331 |
. . . . . . 7
⊢ (𝜑 → Fun
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉}) |
23 | 8 | funeqd 5825 |
. . . . . . 7
⊢ (𝜑 → (Fun 𝐶 ↔ Fun {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉})) |
24 | 22, 23 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → Fun 𝐶) |
25 | 8, 16, 17, 18 | estrreslem2 16601 |
. . . . . 6
⊢ (𝜑 → (Base‘ndx) ∈
dom 𝐶) |
26 | | estrres.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
27 | | estrres.u |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
28 | 8, 16 | estrreslem1 16600 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
29 | 27, 28 | sseqtrd 3604 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ (Base‘𝐶)) |
30 | 5, 6, 7, 10, 24, 25, 26, 29 | ressval3d 15764 |
. . . . 5
⊢ (𝜑 → (𝐶 ↾s 𝐴) = (𝐶 sSet 〈(Base‘ndx), 𝐴〉)) |
31 | 30 | reseq1d 5316 |
. . . 4
⊢ (𝜑 → ((𝐶 ↾s 𝐴) ↾ (V ∖ {(Hom ‘ndx)})) =
((𝐶 sSet
〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)}))) |
32 | 31 | uneq1d 3728 |
. . 3
⊢ (𝜑 → (((𝐶 ↾s 𝐴) ↾ (V ∖ {(Hom ‘ndx)}))
∪ {〈(Hom ‘ndx), 𝐺〉}) = (((𝐶 sSet 〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)})) ∪ {〈(Hom ‘ndx), 𝐺〉})) |
33 | | setsval 15720 |
. . . . . . . 8
⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ 𝑈) → (𝐶 sSet 〈(Base‘ndx), 𝐴〉) = ((𝐶 ↾ (V ∖ {(Base‘ndx)}))
∪ {〈(Base‘ndx), 𝐴〉})) |
34 | 10, 26, 33 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐶 sSet 〈(Base‘ndx), 𝐴〉) = ((𝐶 ↾ (V ∖ {(Base‘ndx)}))
∪ {〈(Base‘ndx), 𝐴〉})) |
35 | 34 | reseq1d 5316 |
. . . . . 6
⊢ (𝜑 → ((𝐶 sSet 〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)})) = (((𝐶
↾ (V ∖ {(Base‘ndx)})) ∪ {〈(Base‘ndx), 𝐴〉}) ↾ (V ∖
{(Hom ‘ndx)}))) |
36 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (Hom ‘ndx) ∈
V) |
37 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (comp‘ndx) ∈
V) |
38 | | elex 3185 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ 𝑋 → 𝐻 ∈ V) |
39 | 17, 38 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ V) |
40 | | elex 3185 |
. . . . . . . . . . 11
⊢ ( · ∈
𝑌 → · ∈
V) |
41 | 18, 40 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → · ∈
V) |
42 | | simp1 1054 |
. . . . . . . . . . . 12
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) →
(Base‘ndx) ≠ (Hom ‘ndx)) |
43 | 42 | necomd 2837 |
. . . . . . . . . . 11
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) → (Hom
‘ndx) ≠ (Base‘ndx)) |
44 | 19, 43 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → (Hom ‘ndx) ≠
(Base‘ndx)) |
45 | | simp2 1055 |
. . . . . . . . . . . 12
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) →
(Base‘ndx) ≠ (comp‘ndx)) |
46 | 45 | necomd 2837 |
. . . . . . . . . . 11
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) →
(comp‘ndx) ≠ (Base‘ndx)) |
47 | 19, 46 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → (comp‘ndx) ≠
(Base‘ndx)) |
48 | 8, 36, 37, 39, 41, 44, 47 | tpres 6371 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ↾ (V ∖ {(Base‘ndx)})) =
{〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), ·
〉}) |
49 | 48 | uneq1d 3728 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 ↾ (V ∖ {(Base‘ndx)}))
∪ {〈(Base‘ndx), 𝐴〉}) = ({〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∪ {〈(Base‘ndx), 𝐴〉})) |
50 | | df-tp 4130 |
. . . . . . . 8
⊢
{〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), ·
〉, 〈(Base‘ndx), 𝐴〉} = ({〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∪ {〈(Base‘ndx), 𝐴〉}) |
51 | 49, 50 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 ↾ (V ∖ {(Base‘ndx)}))
∪ {〈(Base‘ndx), 𝐴〉}) = {〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉, 〈(Base‘ndx), 𝐴〉}) |
52 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (Base‘ndx) ∈
V) |
53 | 16, 27 | ssexd 4733 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ V) |
54 | | simp3 1056 |
. . . . . . . . 9
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) → (Hom
‘ndx) ≠ (comp‘ndx)) |
55 | 54 | necomd 2837 |
. . . . . . . 8
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) →
(comp‘ndx) ≠ (Hom ‘ndx)) |
56 | 19, 55 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (comp‘ndx) ≠ (Hom
‘ndx)) |
57 | 19, 42 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (Base‘ndx) ≠ (Hom
‘ndx)) |
58 | 51, 37, 52, 41, 53, 56, 57 | tpres 6371 |
. . . . . 6
⊢ (𝜑 → (((𝐶 ↾ (V ∖ {(Base‘ndx)}))
∪ {〈(Base‘ndx), 𝐴〉}) ↾ (V ∖ {(Hom
‘ndx)})) = {〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉}) |
59 | 35, 58 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → ((𝐶 sSet 〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)})) = {〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉}) |
60 | 59 | uneq1d 3728 |
. . . 4
⊢ (𝜑 → (((𝐶 sSet 〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)})) ∪ {〈(Hom ‘ndx), 𝐺〉}) = ({〈(comp‘ndx), ·
〉, 〈(Base‘ndx), 𝐴〉} ∪ {〈(Hom ‘ndx), 𝐺〉})) |
61 | | df-tp 4130 |
. . . . . 6
⊢
{〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉} =
({〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉} ∪ {〈(Hom ‘ndx), 𝐺〉}) |
62 | | tprot 4228 |
. . . . . 6
⊢
{〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉} =
{〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉, 〈(comp‘ndx),
·
〉} |
63 | 61, 62 | eqtr3i 2634 |
. . . . 5
⊢
({〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉} ∪ {〈(Hom ‘ndx), 𝐺〉}) =
{〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉, 〈(comp‘ndx),
·
〉} |
64 | 63 | a1i 11 |
. . . 4
⊢ (𝜑 → ({〈(comp‘ndx),
·
〉, 〈(Base‘ndx), 𝐴〉} ∪ {〈(Hom ‘ndx), 𝐺〉}) =
{〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉, 〈(comp‘ndx),
·
〉}) |
65 | 60, 64 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (((𝐶 sSet 〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)})) ∪ {〈(Hom ‘ndx), 𝐺〉}) = {〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx),
𝐺〉,
〈(comp‘ndx), ·
〉}) |
66 | 32, 65 | eqtrd 2644 |
. 2
⊢ (𝜑 → (((𝐶 ↾s 𝐴) ↾ (V ∖ {(Hom ‘ndx)}))
∪ {〈(Hom ‘ndx), 𝐺〉}) = {〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx),
𝐺〉,
〈(comp‘ndx), ·
〉}) |
67 | 4, 66 | eqtrd 2644 |
1
⊢ (𝜑 → ((𝐶 ↾s 𝐴) sSet 〈(Hom ‘ndx), 𝐺〉) =
{〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉, 〈(comp‘ndx),
·
〉}) |