# Metamath Proof Explorer

## Theorem estrreslem2

Description: Lemma 2 for estrres . (Contributed by AV, 14-Mar-2020)

Ref Expression
Hypotheses estrres.c
estrres.b ${⊢}{\phi }\to {B}\in {V}$
estrres.h ${⊢}{\phi }\to {H}\in {X}$
estrres.x
Assertion estrreslem2 ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}{C}$

### Proof

Step Hyp Ref Expression
1 estrres.c
2 estrres.b ${⊢}{\phi }\to {B}\in {V}$
3 estrres.h ${⊢}{\phi }\to {H}\in {X}$
4 estrres.x
5 eqidd ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}={\mathrm{Base}}_{\mathrm{ndx}}$
6 5 3mix1d ${⊢}{\phi }\to \left({\mathrm{Base}}_{\mathrm{ndx}}={\mathrm{Base}}_{\mathrm{ndx}}\vee {\mathrm{Base}}_{\mathrm{ndx}}=\mathrm{Hom}\left(\mathrm{ndx}\right)\vee {\mathrm{Base}}_{\mathrm{ndx}}=\mathrm{comp}\left(\mathrm{ndx}\right)\right)$
7 fvex ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$
8 eltpg ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}\to \left({\mathrm{Base}}_{\mathrm{ndx}}\in \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right),\mathrm{comp}\left(\mathrm{ndx}\right)\right\}↔\left({\mathrm{Base}}_{\mathrm{ndx}}={\mathrm{Base}}_{\mathrm{ndx}}\vee {\mathrm{Base}}_{\mathrm{ndx}}=\mathrm{Hom}\left(\mathrm{ndx}\right)\vee {\mathrm{Base}}_{\mathrm{ndx}}=\mathrm{comp}\left(\mathrm{ndx}\right)\right)\right)$
9 7 8 mp1i ${⊢}{\phi }\to \left({\mathrm{Base}}_{\mathrm{ndx}}\in \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right),\mathrm{comp}\left(\mathrm{ndx}\right)\right\}↔\left({\mathrm{Base}}_{\mathrm{ndx}}={\mathrm{Base}}_{\mathrm{ndx}}\vee {\mathrm{Base}}_{\mathrm{ndx}}=\mathrm{Hom}\left(\mathrm{ndx}\right)\vee {\mathrm{Base}}_{\mathrm{ndx}}=\mathrm{comp}\left(\mathrm{ndx}\right)\right)\right)$
10 6 9 mpbird ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right),\mathrm{comp}\left(\mathrm{ndx}\right)\right\}$
11 df-tp
12 11 a1i
13 12 dmeqd
14 dmun
15 14 a1i
16 dmpropg ${⊢}\left({B}\in {V}\wedge {H}\in {X}\right)\to \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right)\right\}$
17 2 3 16 syl2anc ${⊢}{\phi }\to \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right)\right\}$
18 dmsnopg
19 4 18 syl
20 17 19 uneq12d
21 13 15 20 3eqtrd
22 1 dmeqd
23 df-tp ${⊢}\left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right),\mathrm{comp}\left(\mathrm{ndx}\right)\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right)\right\}\cup \left\{\mathrm{comp}\left(\mathrm{ndx}\right)\right\}$
24 23 a1i ${⊢}{\phi }\to \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right),\mathrm{comp}\left(\mathrm{ndx}\right)\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right)\right\}\cup \left\{\mathrm{comp}\left(\mathrm{ndx}\right)\right\}$
25 21 22 24 3eqtr4d ${⊢}{\phi }\to \mathrm{dom}{C}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right),\mathrm{comp}\left(\mathrm{ndx}\right)\right\}$
26 10 25 eleqtrrd ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}{C}$