Proof of Theorem estrres
| Step | Hyp | Ref
| Expression |
| 1 | | ovex 7464 |
. . 3
⊢ (𝐶 ↾s 𝐴) ∈ V |
| 2 | | estrres.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝑊) |
| 3 | | setsval 17204 |
. . 3
⊢ (((𝐶 ↾s 𝐴) ∈ V ∧ 𝐺 ∈ 𝑊) → ((𝐶 ↾s 𝐴) sSet 〈(Hom ‘ndx), 𝐺〉) = (((𝐶 ↾s 𝐴) ↾ (V ∖ {(Hom ‘ndx)}))
∪ {〈(Hom ‘ndx), 𝐺〉})) |
| 4 | 1, 2, 3 | sylancr 587 |
. 2
⊢ (𝜑 → ((𝐶 ↾s 𝐴) sSet 〈(Hom ‘ndx), 𝐺〉) = (((𝐶 ↾s 𝐴) ↾ (V ∖ {(Hom ‘ndx)}))
∪ {〈(Hom ‘ndx), 𝐺〉})) |
| 5 | | eqid 2737 |
. . . . 5
⊢ (𝐶 ↾s 𝐴) = (𝐶 ↾s 𝐴) |
| 6 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 7 | | eqid 2737 |
. . . . 5
⊢
(Base‘ndx) = (Base‘ndx) |
| 8 | | estrres.c |
. . . . . 6
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉}) |
| 9 | | tpex 7766 |
. . . . . 6
⊢
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∈ V |
| 10 | 8, 9 | eqeltrdi 2849 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ V) |
| 11 | | fvex 6919 |
. . . . . . . . 9
⊢
(Base‘ndx) ∈ V |
| 12 | | fvex 6919 |
. . . . . . . . 9
⊢ (Hom
‘ndx) ∈ V |
| 13 | | fvex 6919 |
. . . . . . . . 9
⊢
(comp‘ndx) ∈ V |
| 14 | 11, 12, 13 | 3pm3.2i 1340 |
. . . . . . . 8
⊢
((Base‘ndx) ∈ V ∧ (Hom ‘ndx) ∈ V ∧
(comp‘ndx) ∈ V) |
| 15 | 14 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((Base‘ndx) ∈ V
∧ (Hom ‘ndx) ∈ V ∧ (comp‘ndx) ∈
V)) |
| 16 | | estrres.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
| 17 | | estrres.h |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ 𝑋) |
| 18 | | estrres.x |
. . . . . . 7
⊢ (𝜑 → · ∈ 𝑌) |
| 19 | | slotsbhcdif 17459 |
. . . . . . . 8
⊢
((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) |
| 20 | 19 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((Base‘ndx) ≠
(Hom ‘ndx) ∧ (Base‘ndx) ≠ (comp‘ndx) ∧ (Hom
‘ndx) ≠ (comp‘ndx))) |
| 21 | | funtpg 6621 |
. . . . . . 7
⊢
((((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 1385 |
. . . . . 6
⊢ (𝜑 → Fun
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉}) |
| 23 | 8 | funeqd 6588 |
. . . . . 6
⊢ (𝜑 → (Fun 𝐶 ↔ Fun {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐻〉,
〈(comp‘ndx), ·
〉})) |
| 24 | 22, 23 | mpbird 257 |
. . . . 5
⊢ (𝜑 → Fun 𝐶) |
| 25 | 8, 16, 17, 18 | estrreslem2 18183 |
. . . . 5
⊢ (𝜑 → (Base‘ndx) ∈
dom 𝐶) |
| 26 | | estrres.u |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| 27 | 8, 16 | estrreslem1 18181 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
| 28 | 26, 27 | sseqtrd 4020 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ (Base‘𝐶)) |
| 29 | 5, 6, 7, 10, 24, 25, 28 | ressval3d 17292 |
. . . 4
⊢ (𝜑 → (𝐶 ↾s 𝐴) = (𝐶 sSet 〈(Base‘ndx), 𝐴〉)) |
| 30 | 29 | reseq1d 5996 |
. . 3
⊢ (𝜑 → ((𝐶 ↾s 𝐴) ↾ (V ∖ {(Hom ‘ndx)})) =
((𝐶 sSet
〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)}))) |
| 31 | 30 | uneq1d 4167 |
. 2
⊢ (𝜑 → (((𝐶 ↾s 𝐴) ↾ (V ∖ {(Hom ‘ndx)}))
∪ {〈(Hom ‘ndx), 𝐺〉}) = (((𝐶 sSet 〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)})) ∪ {〈(Hom ‘ndx), 𝐺〉})) |
| 32 | 16, 26 | ssexd 5324 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ V) |
| 33 | | setsval 17204 |
. . . . . . 7
⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 sSet 〈(Base‘ndx),
𝐴〉) = ((𝐶 ↾ (V ∖
{(Base‘ndx)})) ∪ {〈(Base‘ndx), 𝐴〉})) |
| 34 | 10, 32, 33 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐶 sSet 〈(Base‘ndx), 𝐴〉) = ((𝐶 ↾ (V ∖ {(Base‘ndx)}))
∪ {〈(Base‘ndx), 𝐴〉})) |
| 35 | 34 | reseq1d 5996 |
. . . . 5
⊢ (𝜑 → ((𝐶 sSet 〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)})) = (((𝐶
↾ (V ∖ {(Base‘ndx)})) ∪ {〈(Base‘ndx), 𝐴〉}) ↾ (V ∖
{(Hom ‘ndx)}))) |
| 36 | | fvexd 6921 |
. . . . . . . . 9
⊢ (𝜑 → (Hom ‘ndx) ∈
V) |
| 37 | | fvexd 6921 |
. . . . . . . . 9
⊢ (𝜑 → (comp‘ndx) ∈
V) |
| 38 | 17 | elexd 3504 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ V) |
| 39 | 18 | elexd 3504 |
. . . . . . . . 9
⊢ (𝜑 → · ∈
V) |
| 40 | | simp1 1137 |
. . . . . . . . . . 11
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) →
(Base‘ndx) ≠ (Hom ‘ndx)) |
| 41 | 40 | necomd 2996 |
. . . . . . . . . 10
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) → (Hom
‘ndx) ≠ (Base‘ndx)) |
| 42 | 19, 41 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (Hom ‘ndx) ≠
(Base‘ndx)) |
| 43 | | simp2 1138 |
. . . . . . . . . . 11
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) →
(Base‘ndx) ≠ (comp‘ndx)) |
| 44 | 43 | necomd 2996 |
. . . . . . . . . 10
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) →
(comp‘ndx) ≠ (Base‘ndx)) |
| 45 | 19, 44 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (comp‘ndx) ≠
(Base‘ndx)) |
| 46 | 8, 36, 37, 38, 39, 42, 45 | tpres 7221 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ↾ (V ∖ {(Base‘ndx)})) =
{〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), ·
〉}) |
| 47 | 46 | uneq1d 4167 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 ↾ (V ∖ {(Base‘ndx)}))
∪ {〈(Base‘ndx), 𝐴〉}) = ({〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∪ {〈(Base‘ndx), 𝐴〉})) |
| 48 | | df-tp 4631 |
. . . . . . 7
⊢
{〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), ·
〉, 〈(Base‘ndx), 𝐴〉} = ({〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉} ∪ {〈(Base‘ndx), 𝐴〉}) |
| 49 | 47, 48 | eqtr4di 2795 |
. . . . . 6
⊢ (𝜑 → ((𝐶 ↾ (V ∖ {(Base‘ndx)}))
∪ {〈(Base‘ndx), 𝐴〉}) = {〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx),
·
〉, 〈(Base‘ndx), 𝐴〉}) |
| 50 | | fvexd 6921 |
. . . . . 6
⊢ (𝜑 → (Base‘ndx) ∈
V) |
| 51 | | simp3 1139 |
. . . . . . . 8
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) → (Hom
‘ndx) ≠ (comp‘ndx)) |
| 52 | 51 | necomd 2996 |
. . . . . . 7
⊢
(((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠
(comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) →
(comp‘ndx) ≠ (Hom ‘ndx)) |
| 53 | 19, 52 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (comp‘ndx) ≠ (Hom
‘ndx)) |
| 54 | 19, 40 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (Base‘ndx) ≠ (Hom
‘ndx)) |
| 55 | 49, 37, 50, 39, 32, 53, 54 | tpres 7221 |
. . . . 5
⊢ (𝜑 → (((𝐶 ↾ (V ∖ {(Base‘ndx)}))
∪ {〈(Base‘ndx), 𝐴〉}) ↾ (V ∖ {(Hom
‘ndx)})) = {〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉}) |
| 56 | 35, 55 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ((𝐶 sSet 〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)})) = {〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉}) |
| 57 | 56 | uneq1d 4167 |
. . 3
⊢ (𝜑 → (((𝐶 sSet 〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)})) ∪ {〈(Hom ‘ndx), 𝐺〉}) = ({〈(comp‘ndx), ·
〉, 〈(Base‘ndx), 𝐴〉} ∪ {〈(Hom ‘ndx), 𝐺〉})) |
| 58 | | df-tp 4631 |
. . . 4
⊢
{〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉} =
({〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉} ∪ {〈(Hom ‘ndx), 𝐺〉}) |
| 59 | | tprot 4749 |
. . . 4
⊢
{〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉} =
{〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉, 〈(comp‘ndx),
·
〉} |
| 60 | 58, 59 | eqtr3i 2767 |
. . 3
⊢
({〈(comp‘ndx), · 〉,
〈(Base‘ndx), 𝐴〉} ∪ {〈(Hom ‘ndx), 𝐺〉}) =
{〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉, 〈(comp‘ndx),
·
〉} |
| 61 | 57, 60 | eqtrdi 2793 |
. 2
⊢ (𝜑 → (((𝐶 sSet 〈(Base‘ndx), 𝐴〉) ↾ (V ∖ {(Hom
‘ndx)})) ∪ {〈(Hom ‘ndx), 𝐺〉}) = {〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx),
𝐺〉,
〈(comp‘ndx), ·
〉}) |
| 62 | 4, 31, 61 | 3eqtrd 2781 |
1
⊢ (𝜑 → ((𝐶 ↾s 𝐴) sSet 〈(Hom ‘ndx), 𝐺〉) =
{〈(Base‘ndx), 𝐴〉, 〈(Hom ‘ndx), 𝐺〉, 〈(comp‘ndx),
·
〉}) |