This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐶 )