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 )