Metamath Proof Explorer

Theorem 1stconst

Description: The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion 1stconst 
|- ( B e. V -> ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -1-1-onto-> A )

Proof

Step Hyp Ref Expression
1 snnzg 
 |-  ( B e. V -> { B } =/= (/) )
2 fo1stres 
 |-  ( { B } =/= (/) -> ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -onto-> A )
3 1 2 syl 
 |-  ( B e. V -> ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -onto-> A )
4 moeq 
 |-  E* x x = <. y , B >.
5 4 moani 
 |-  E* x ( y e. A /\ x = <. y , B >. )
6 vex 
 |-  y e. _V
7 6 brresi 
 |-  ( x ( 1st |` ( A X. { B } ) ) y <-> ( x e. ( A X. { B } ) /\ x 1st y ) )
8 fo1st 
 |-  1st : _V -onto-> _V
9 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
10 8 9 ax-mp 
 |-  1st Fn _V
11 vex 
 |-  x e. _V
12 fnbrfvb 
 |-  ( ( 1st Fn _V /\ x e. _V ) -> ( ( 1st ` x ) = y <-> x 1st y ) )
13 10 11 12 mp2an 
 |-  ( ( 1st ` x ) = y <-> x 1st y )
14 13 anbi2i 
 |-  ( ( x e. ( A X. { B } ) /\ ( 1st ` x ) = y ) <-> ( x e. ( A X. { B } ) /\ x 1st y ) )
15 elxp7 
 |-  ( x e. ( A X. { B } ) <-> ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. { B } ) ) )
16 eleq1 
 |-  ( ( 1st ` x ) = y -> ( ( 1st ` x ) e. A <-> y e. A ) )
17 16 biimpac 
 |-  ( ( ( 1st ` x ) e. A /\ ( 1st ` x ) = y ) -> y e. A )
18 17 adantlr 
 |-  ( ( ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. { B } ) /\ ( 1st ` x ) = y ) -> y e. A )
19 18 adantll 
 |-  ( ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. { B } ) ) /\ ( 1st ` x ) = y ) -> y e. A )
20 elsni 
 |-  ( ( 2nd ` x ) e. { B } -> ( 2nd ` x ) = B )
21 eqopi 
 |-  ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) = y /\ ( 2nd ` x ) = B ) ) -> x = <. y , B >. )
22 21 anass1rs 
 |-  ( ( ( x e. ( _V X. _V ) /\ ( 2nd ` x ) = B ) /\ ( 1st ` x ) = y ) -> x = <. y , B >. )
23 20 22 sylanl2 
 |-  ( ( ( x e. ( _V X. _V ) /\ ( 2nd ` x ) e. { B } ) /\ ( 1st ` x ) = y ) -> x = <. y , B >. )
24 23 adantlrl 
 |-  ( ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. { B } ) ) /\ ( 1st ` x ) = y ) -> x = <. y , B >. )
25 19 24 jca 
 |-  ( ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. { B } ) ) /\ ( 1st ` x ) = y ) -> ( y e. A /\ x = <. y , B >. ) )
26 15 25 sylanb 
 |-  ( ( x e. ( A X. { B } ) /\ ( 1st ` x ) = y ) -> ( y e. A /\ x = <. y , B >. ) )
27 26 adantl 
 |-  ( ( B e. V /\ ( x e. ( A X. { B } ) /\ ( 1st ` x ) = y ) ) -> ( y e. A /\ x = <. y , B >. ) )
28 simprr 
 |-  ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> x = <. y , B >. )
29 simprl 
 |-  ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> y e. A )
30 snidg 
 |-  ( B e. V -> B e. { B } )
31 30 adantr 
 |-  ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> B e. { B } )
32 29 31 opelxpd 
 |-  ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> <. y , B >. e. ( A X. { B } ) )
33 28 32 eqeltrd 
 |-  ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> x e. ( A X. { B } ) )
34 28 fveq2d 
 |-  ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> ( 1st ` x ) = ( 1st ` <. y , B >. ) )
35 simpl 
 |-  ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> B e. V )
36 op1stg 
 |-  ( ( y e. A /\ B e. V ) -> ( 1st ` <. y , B >. ) = y )
37 29 35 36 syl2anc 
 |-  ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> ( 1st ` <. y , B >. ) = y )
38 34 37 eqtrd 
 |-  ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> ( 1st ` x ) = y )
39 33 38 jca 
 |-  ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> ( x e. ( A X. { B } ) /\ ( 1st ` x ) = y ) )
40 27 39 impbida 
 |-  ( B e. V -> ( ( x e. ( A X. { B } ) /\ ( 1st ` x ) = y ) <-> ( y e. A /\ x = <. y , B >. ) ) )
41 14 40 bitr3id 
 |-  ( B e. V -> ( ( x e. ( A X. { B } ) /\ x 1st y ) <-> ( y e. A /\ x = <. y , B >. ) ) )
42 7 41 syl5bb 
 |-  ( B e. V -> ( x ( 1st |` ( A X. { B } ) ) y <-> ( y e. A /\ x = <. y , B >. ) ) )
43 42 mobidv 
 |-  ( B e. V -> ( E* x x ( 1st |` ( A X. { B } ) ) y <-> E* x ( y e. A /\ x = <. y , B >. ) ) )
44 5 43 mpbiri 
 |-  ( B e. V -> E* x x ( 1st |` ( A X. { B } ) ) y )
45 44 alrimiv 
 |-  ( B e. V -> A. y E* x x ( 1st |` ( A X. { B } ) ) y )
46 funcnv2 
 |-  ( Fun `' ( 1st |` ( A X. { B } ) ) <-> A. y E* x x ( 1st |` ( A X. { B } ) ) y )
47 45 46 sylibr 
 |-  ( B e. V -> Fun `' ( 1st |` ( A X. { B } ) ) )
48 dff1o3 
 |-  ( ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -1-1-onto-> A <-> ( ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -onto-> A /\ Fun `' ( 1st |` ( A X. { B } ) ) ) )
49 3 47 48 sylanbrc 
 |-  ( B e. V -> ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -1-1-onto-> A )