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 
|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
estrres.b 
|- ( ph -> B e. V )
estrres.h 
|- ( ph -> H e. X )
estrres.x 
|- ( ph -> .x. e. Y )
Assertion estrreslem2 
|- ( ph -> ( Base ` ndx ) e. dom C )

Proof

Step Hyp Ref Expression
1 estrres.c 
 |-  ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
2 estrres.b 
 |-  ( ph -> B e. V )
3 estrres.h 
 |-  ( ph -> H e. X )
4 estrres.x 
 |-  ( ph -> .x. e. Y )
5 eqidd 
 |-  ( ph -> ( Base ` ndx ) = ( Base ` ndx ) )
6 5 3mix1d 
 |-  ( ph -> ( ( Base ` ndx ) = ( Base ` ndx ) \/ ( Base ` ndx ) = ( Hom ` ndx ) \/ ( Base ` ndx ) = ( comp ` ndx ) ) )
7 fvex 
 |-  ( Base ` ndx ) e. _V
8 eltpg 
 |-  ( ( Base ` ndx ) e. _V -> ( ( Base ` ndx ) e. { ( Base ` ndx ) , ( Hom ` ndx ) , ( comp ` ndx ) } <-> ( ( Base ` ndx ) = ( Base ` ndx ) \/ ( Base ` ndx ) = ( Hom ` ndx ) \/ ( Base ` ndx ) = ( comp ` ndx ) ) ) )
9 7 8 mp1i 
 |-  ( ph -> ( ( Base ` ndx ) e. { ( Base ` ndx ) , ( Hom ` ndx ) , ( comp ` ndx ) } <-> ( ( Base ` ndx ) = ( Base ` ndx ) \/ ( Base ` ndx ) = ( Hom ` ndx ) \/ ( Base ` ndx ) = ( comp ` ndx ) ) ) )
10 6 9 mpbird 
 |-  ( ph -> ( Base ` ndx ) e. { ( Base ` ndx ) , ( Hom ` ndx ) , ( comp ` ndx ) } )
11 df-tp 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } = ( { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. } u. { <. ( comp ` ndx ) , .x. >. } )
12 11 a1i 
 |-  ( ph -> { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } = ( { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. } u. { <. ( comp ` ndx ) , .x. >. } ) )
13 12 dmeqd 
 |-  ( ph -> dom { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } = dom ( { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. } u. { <. ( comp ` ndx ) , .x. >. } ) )
14 dmun 
 |-  dom ( { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. } u. { <. ( comp ` ndx ) , .x. >. } ) = ( dom { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. } u. dom { <. ( comp ` ndx ) , .x. >. } )
15 14 a1i 
 |-  ( ph -> dom ( { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. } u. { <. ( comp ` ndx ) , .x. >. } ) = ( dom { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. } u. dom { <. ( comp ` ndx ) , .x. >. } ) )
16 dmpropg 
 |-  ( ( B e. V /\ H e. X ) -> dom { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. } = { ( Base ` ndx ) , ( Hom ` ndx ) } )
17 2 3 16 syl2anc 
 |-  ( ph -> dom { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. } = { ( Base ` ndx ) , ( Hom ` ndx ) } )
18 dmsnopg 
 |-  ( .x. e. Y -> dom { <. ( comp ` ndx ) , .x. >. } = { ( comp ` ndx ) } )
19 4 18 syl 
 |-  ( ph -> dom { <. ( comp ` ndx ) , .x. >. } = { ( comp ` ndx ) } )
20 17 19 uneq12d 
 |-  ( ph -> ( dom { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. } u. dom { <. ( comp ` ndx ) , .x. >. } ) = ( { ( Base ` ndx ) , ( Hom ` ndx ) } u. { ( comp ` ndx ) } ) )
21 13 15 20 3eqtrd 
 |-  ( ph -> dom { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } = ( { ( Base ` ndx ) , ( Hom ` ndx ) } u. { ( comp ` ndx ) } ) )
22 1 dmeqd 
 |-  ( ph -> dom C = dom { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
23 df-tp 
 |-  { ( Base ` ndx ) , ( Hom ` ndx ) , ( comp ` ndx ) } = ( { ( Base ` ndx ) , ( Hom ` ndx ) } u. { ( comp ` ndx ) } )
24 23 a1i 
 |-  ( ph -> { ( Base ` ndx ) , ( Hom ` ndx ) , ( comp ` ndx ) } = ( { ( Base ` ndx ) , ( Hom ` ndx ) } u. { ( comp ` ndx ) } ) )
25 21 22 24 3eqtr4d 
 |-  ( ph -> dom C = { ( Base ` ndx ) , ( Hom ` ndx ) , ( comp ` ndx ) } )
26 10 25 eleqtrrd 
 |-  ( ph -> ( Base ` ndx ) e. dom C )