Theorem estrreslem2

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

	Ref	Expression
Hypotheses	estrres.c	⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
	estrres.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	estrres.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
	estrres.x	⊢ ( 𝜑 → · ∈ 𝑌 )
Assertion	estrreslem2	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐶 )

Proof

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