Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. . . 4
⊢ (𝜑 → (Base‘ndx) =
(Base‘ndx)) |
2 | 1 | 3mix1d 1337 |
. . 3
⊢ (𝜑 → ((Base‘ndx) =
(Base‘ndx) ∨ (Base‘ndx) = (Hom ‘ndx) ∨ (Base‘ndx)
= (comp‘ndx))) |
3 | | fvex 6856 |
. . . 4
⊢
(Base‘ndx) ∈ V |
4 | | eltpg 4647 |
. . . 4
⊢
((Base‘ndx) ∈ V → ((Base‘ndx) ∈
{(Base‘ndx), (Hom ‘ndx), (comp‘ndx)} ↔ ((Base‘ndx)
= (Base‘ndx) ∨ (Base‘ndx) = (Hom ‘ndx) ∨
(Base‘ndx) = (comp‘ndx)))) |
5 | 3, 4 | mp1i 13 |
. . 3
⊢ (𝜑 → ((Base‘ndx) ∈
{(Base‘ndx), (Hom ‘ndx), (comp‘ndx)} ↔ ((Base‘ndx)
= (Base‘ndx) ∨ (Base‘ndx) = (Hom ‘ndx) ∨
(Base‘ndx) = (comp‘ndx)))) |
6 | 2, 5 | mpbird 257 |
. 2
⊢ (𝜑 → (Base‘ndx) ∈
{(Base‘ndx), (Hom ‘ndx), (comp‘ndx)}) |
7 | | df-tp 4592 |
. . . . . 6
⊢
{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx),
·
⟩} = ({⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩} ∪
{⟨(comp‘ndx), ·
⟩}) |
8 | 7 | a1i 11 |
. . . . 5
⊢ (𝜑 → {⟨(Base‘ndx),
𝐵⟩, ⟨(Hom
‘ndx), 𝐻⟩,
⟨(comp‘ndx), · ⟩} =
({⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩} ∪
{⟨(comp‘ndx), ·
⟩})) |
9 | 8 | dmeqd 5862 |
. . . 4
⊢ (𝜑 → dom
{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx),
·
⟩} = dom ({⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩} ∪
{⟨(comp‘ndx), ·
⟩})) |
10 | | dmun 5867 |
. . . . 5
⊢ dom
({⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩} ∪
{⟨(comp‘ndx), · ⟩}) = (dom
{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩} ∪ dom
{⟨(comp‘ndx), ·
⟩}) |
11 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 → dom
({⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩} ∪
{⟨(comp‘ndx), · ⟩}) = (dom
{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩} ∪ dom
{⟨(comp‘ndx), ·
⟩})) |
12 | | estrres.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
13 | | estrres.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ 𝑋) |
14 | | dmpropg 6168 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐻 ∈ 𝑋) → dom {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx),
𝐻⟩} =
{(Base‘ndx), (Hom ‘ndx)}) |
15 | 12, 13, 14 | syl2anc 585 |
. . . . 5
⊢ (𝜑 → dom
{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩} = {(Base‘ndx),
(Hom ‘ndx)}) |
16 | | estrres.x |
. . . . . 6
⊢ (𝜑 → · ∈ 𝑌) |
17 | | dmsnopg 6166 |
. . . . . 6
⊢ ( · ∈
𝑌 → dom
{⟨(comp‘ndx), · ⟩} =
{(comp‘ndx)}) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → dom
{⟨(comp‘ndx), · ⟩} =
{(comp‘ndx)}) |
19 | 15, 18 | uneq12d 4125 |
. . . 4
⊢ (𝜑 → (dom
{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩} ∪ dom
{⟨(comp‘ndx), · ⟩}) =
({(Base‘ndx), (Hom ‘ndx)} ∪
{(comp‘ndx)})) |
20 | 9, 11, 19 | 3eqtrd 2777 |
. . 3
⊢ (𝜑 → dom
{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx),
·
⟩} = ({(Base‘ndx), (Hom ‘ndx)} ∪
{(comp‘ndx)})) |
21 | | estrres.c |
. . . 4
⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx),
𝐻⟩,
⟨(comp‘ndx), ·
⟩}) |
22 | 21 | dmeqd 5862 |
. . 3
⊢ (𝜑 → dom 𝐶 = dom {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx),
𝐻⟩,
⟨(comp‘ndx), ·
⟩}) |
23 | | df-tp 4592 |
. . . 4
⊢
{(Base‘ndx), (Hom ‘ndx), (comp‘ndx)} =
({(Base‘ndx), (Hom ‘ndx)} ∪
{(comp‘ndx)}) |
24 | 23 | a1i 11 |
. . 3
⊢ (𝜑 → {(Base‘ndx), (Hom
‘ndx), (comp‘ndx)} = ({(Base‘ndx), (Hom ‘ndx)} ∪
{(comp‘ndx)})) |
25 | 20, 22, 24 | 3eqtr4d 2783 |
. 2
⊢ (𝜑 → dom 𝐶 = {(Base‘ndx), (Hom ‘ndx),
(comp‘ndx)}) |
26 | 6, 25 | eleqtrrd 2837 |
1
⊢ (𝜑 → (Base‘ndx) ∈
dom 𝐶) |