Theorem estrreslem2

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

	Ref	Expression
Hypotheses	estrres.c	$$⊢\phi \to C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
	estrres.b	$$⊢\phi \to B\in V$$
	estrres.h	$$⊢\phi \to H\in X$$
	estrres.x	$$⊢\phi \to \underset{\dot{}}{·}\in Y$$
Assertion	estrreslem2	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}C$$

Proof

Step	Hyp	Ref	Expression
1		estrres.c	$$⊢\phi \to C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
2		estrres.b	$$⊢\phi \to B\in V$$
3		estrres.h	$$⊢\phi \to H\in X$$
4		estrres.x	$$⊢\phi \to \underset{\dot{}}{·}\in Y$$
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\}\leftrightarrow \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\}\leftrightarrow \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	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right\}\cup \left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
12	11	a1i	$$⊢\phi \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right\}\cup \left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
13	12	dmeqd	$$⊢\phi \to \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}=\mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right\}\cup \left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\right)$$
14		dmun	$$⊢\mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right\}\cup \left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\right)=\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
15	14	a1i	$$⊢\phi \to \mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right\}\cup \left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\right)=\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
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	$$⊢\underset{\dot{}}{·}\in Y\to \mathrm{dom}\left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}=\left\{\mathrm{comp}\left(\mathrm{ndx}\right)\right\}$$
19	4 18	syl	$$⊢\phi \to \mathrm{dom}\left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}=\left\{\mathrm{comp}\left(\mathrm{ndx}\right)\right\}$$
20	17 19	uneq12d	$$⊢\phi \to \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right)\right\}\cup \left\{\mathrm{comp}\left(\mathrm{ndx}\right)\right\}$$
21	13 15 20	3eqtrd	$$⊢\phi \to \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Hom}\left(\mathrm{ndx}\right)\right\}\cup \left\{\mathrm{comp}\left(\mathrm{ndx}\right)\right\}$$
22	1	dmeqd	$$⊢\phi \to \mathrm{dom}C=\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
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$$