Metamath Proof Explorer

Theorem fsetsnfo

Description: The mapping of an element of a class to a singleton function is a surjection. (Contributed by AV, 13-Sep-2024)

Ref Expression
Hypotheses fsetsnf.a 
|- A = { y | E. b e. B y = { <. S , b >. } }
fsetsnf.f 
|- F = ( x e. B |-> { <. S , x >. } )
Assertion fsetsnfo 
|- ( S e. V -> F : B -onto-> A )

Proof

Step Hyp Ref Expression
1 fsetsnf.a 
 |-  A = { y | E. b e. B y = { <. S , b >. } }
2 fsetsnf.f 
 |-  F = ( x e. B |-> { <. S , x >. } )
3 1 2 fsetsnf 
 |-  ( S e. V -> F : B --> A )
4 vex 
 |-  m e. _V
5 eqeq1 
 |-  ( y = m -> ( y = { <. S , b >. } <-> m = { <. S , b >. } ) )
6 5 rexbidv 
 |-  ( y = m -> ( E. b e. B y = { <. S , b >. } <-> E. b e. B m = { <. S , b >. } ) )
7 4 6 1 elab2 
 |-  ( m e. A <-> E. b e. B m = { <. S , b >. } )
8 opeq2 
 |-  ( b = n -> <. S , b >. = <. S , n >. )
9 8 sneqd 
 |-  ( b = n -> { <. S , b >. } = { <. S , n >. } )
10 9 eqeq2d 
 |-  ( b = n -> ( m = { <. S , b >. } <-> m = { <. S , n >. } ) )
11 10 cbvrexvw 
 |-  ( E. b e. B m = { <. S , b >. } <-> E. n e. B m = { <. S , n >. } )
12 simpr 
 |-  ( ( ( S e. V /\ n e. B ) /\ m = { <. S , n >. } ) -> m = { <. S , n >. } )
13 2 a1i 
 |-  ( ( S e. V /\ n e. B ) -> F = ( x e. B |-> { <. S , x >. } ) )
14 opeq2 
 |-  ( x = n -> <. S , x >. = <. S , n >. )
15 14 sneqd 
 |-  ( x = n -> { <. S , x >. } = { <. S , n >. } )
16 15 adantl 
 |-  ( ( ( S e. V /\ n e. B ) /\ x = n ) -> { <. S , x >. } = { <. S , n >. } )
17 simpr 
 |-  ( ( S e. V /\ n e. B ) -> n e. B )
18 snex 
 |-  { <. S , n >. } e. _V
19 18 a1i 
 |-  ( ( S e. V /\ n e. B ) -> { <. S , n >. } e. _V )
20 13 16 17 19 fvmptd 
 |-  ( ( S e. V /\ n e. B ) -> ( F ` n ) = { <. S , n >. } )
21 20 eqcomd 
 |-  ( ( S e. V /\ n e. B ) -> { <. S , n >. } = ( F ` n ) )
22 21 adantr 
 |-  ( ( ( S e. V /\ n e. B ) /\ m = { <. S , n >. } ) -> { <. S , n >. } = ( F ` n ) )
23 12 22 eqtrd 
 |-  ( ( ( S e. V /\ n e. B ) /\ m = { <. S , n >. } ) -> m = ( F ` n ) )
24 23 ex 
 |-  ( ( S e. V /\ n e. B ) -> ( m = { <. S , n >. } -> m = ( F ` n ) ) )
25 24 reximdva 
 |-  ( S e. V -> ( E. n e. B m = { <. S , n >. } -> E. n e. B m = ( F ` n ) ) )
26 11 25 biimtrid 
 |-  ( S e. V -> ( E. b e. B m = { <. S , b >. } -> E. n e. B m = ( F ` n ) ) )
27 7 26 biimtrid 
 |-  ( S e. V -> ( m e. A -> E. n e. B m = ( F ` n ) ) )
28 27 imp 
 |-  ( ( S e. V /\ m e. A ) -> E. n e. B m = ( F ` n ) )
29 28 ralrimiva 
 |-  ( S e. V -> A. m e. A E. n e. B m = ( F ` n ) )
30 dffo3 
 |-  ( F : B -onto-> A <-> ( F : B --> A /\ A. m e. A E. n e. B m = ( F ` n ) ) )
31 3 29 30 sylanbrc 
 |-  ( S e. V -> F : B -onto-> A )