Metamath Proof Explorer

Theorem embedsetcestrclem

Description: Lemma for embedsetcestrc . (Contributed by AV, 31-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s 
|- S = ( SetCat ` U )
funcsetcestrc.c 
|- C = ( Base ` S )
funcsetcestrc.f 
|- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )
funcsetcestrc.u 
|- ( ph -> U e. WUni )
funcsetcestrc.o 
|- ( ph -> _om e. U )
funcsetcestrclem3.e 
|- E = ( ExtStrCat ` U )
funcsetcestrclem3.b 
|- B = ( Base ` E )
Assertion embedsetcestrclem 
|- ( ph -> F : C -1-1-> B )

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s 
 |-  S = ( SetCat ` U )
2 funcsetcestrc.c 
 |-  C = ( Base ` S )
3 funcsetcestrc.f 
 |-  ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )
4 funcsetcestrc.u 
 |-  ( ph -> U e. WUni )
5 funcsetcestrc.o 
 |-  ( ph -> _om e. U )
6 funcsetcestrclem3.e 
 |-  E = ( ExtStrCat ` U )
7 funcsetcestrclem3.b 
 |-  B = ( Base ` E )
8 1 2 3 4 5 6 7 funcsetcestrclem3 
 |-  ( ph -> F : C --> B )
9 1 2 3 funcsetcestrclem1 
 |-  ( ( ph /\ y e. C ) -> ( F ` y ) = { <. ( Base ` ndx ) , y >. } )
10 9 adantrr 
 |-  ( ( ph /\ ( y e. C /\ z e. C ) ) -> ( F ` y ) = { <. ( Base ` ndx ) , y >. } )
11 1 2 3 funcsetcestrclem1 
 |-  ( ( ph /\ z e. C ) -> ( F ` z ) = { <. ( Base ` ndx ) , z >. } )
12 11 adantrl 
 |-  ( ( ph /\ ( y e. C /\ z e. C ) ) -> ( F ` z ) = { <. ( Base ` ndx ) , z >. } )
13 10 12 eqeq12d 
 |-  ( ( ph /\ ( y e. C /\ z e. C ) ) -> ( ( F ` y ) = ( F ` z ) <-> { <. ( Base ` ndx ) , y >. } = { <. ( Base ` ndx ) , z >. } ) )
14 opex 
 |-  <. ( Base ` ndx ) , y >. e. _V
15 sneqbg 
 |-  ( <. ( Base ` ndx ) , y >. e. _V -> ( { <. ( Base ` ndx ) , y >. } = { <. ( Base ` ndx ) , z >. } <-> <. ( Base ` ndx ) , y >. = <. ( Base ` ndx ) , z >. ) )
16 14 15 mp1i 
 |-  ( ( ph /\ ( y e. C /\ z e. C ) ) -> ( { <. ( Base ` ndx ) , y >. } = { <. ( Base ` ndx ) , z >. } <-> <. ( Base ` ndx ) , y >. = <. ( Base ` ndx ) , z >. ) )
17 fvexd 
 |-  ( ph -> ( Base ` ndx ) e. _V )
18 simpl 
 |-  ( ( y e. C /\ z e. C ) -> y e. C )
19 opthg 
 |-  ( ( ( Base ` ndx ) e. _V /\ y e. C ) -> ( <. ( Base ` ndx ) , y >. = <. ( Base ` ndx ) , z >. <-> ( ( Base ` ndx ) = ( Base ` ndx ) /\ y = z ) ) )
20 17 18 19 syl2an 
 |-  ( ( ph /\ ( y e. C /\ z e. C ) ) -> ( <. ( Base ` ndx ) , y >. = <. ( Base ` ndx ) , z >. <-> ( ( Base ` ndx ) = ( Base ` ndx ) /\ y = z ) ) )
21 simpr 
 |-  ( ( ( Base ` ndx ) = ( Base ` ndx ) /\ y = z ) -> y = z )
22 20 21 biimtrdi 
 |-  ( ( ph /\ ( y e. C /\ z e. C ) ) -> ( <. ( Base ` ndx ) , y >. = <. ( Base ` ndx ) , z >. -> y = z ) )
23 16 22 sylbid 
 |-  ( ( ph /\ ( y e. C /\ z e. C ) ) -> ( { <. ( Base ` ndx ) , y >. } = { <. ( Base ` ndx ) , z >. } -> y = z ) )
24 13 23 sylbid 
 |-  ( ( ph /\ ( y e. C /\ z e. C ) ) -> ( ( F ` y ) = ( F ` z ) -> y = z ) )
25 24 ralrimivva 
 |-  ( ph -> A. y e. C A. z e. C ( ( F ` y ) = ( F ` z ) -> y = z ) )
26 dff13 
 |-  ( F : C -1-1-> B <-> ( F : C --> B /\ A. y e. C A. z e. C ( ( F ` y ) = ( F ` z ) -> y = z ) ) )
27 8 25 26 sylanbrc 
 |-  ( ph -> F : C -1-1-> B )