Metamath Proof Explorer

Theorem fsetsnf1

Description: The mapping of an element of a class to a singleton function is an injection. (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 fsetsnf1 
|- ( S e. V -> F : B -1-1-> 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 2 a1i 
 |-  ( ( m e. B /\ n e. B ) -> F = ( x e. B |-> { <. S , x >. } ) )
5 opeq2 
 |-  ( x = m -> <. S , x >. = <. S , m >. )
6 5 sneqd 
 |-  ( x = m -> { <. S , x >. } = { <. S , m >. } )
7 6 adantl 
 |-  ( ( ( m e. B /\ n e. B ) /\ x = m ) -> { <. S , x >. } = { <. S , m >. } )
8 simpl 
 |-  ( ( m e. B /\ n e. B ) -> m e. B )
9 snex 
 |-  { <. S , m >. } e. _V
10 9 a1i 
 |-  ( ( m e. B /\ n e. B ) -> { <. S , m >. } e. _V )
11 4 7 8 10 fvmptd 
 |-  ( ( m e. B /\ n e. B ) -> ( F ` m ) = { <. S , m >. } )
12 opeq2 
 |-  ( x = n -> <. S , x >. = <. S , n >. )
13 12 sneqd 
 |-  ( x = n -> { <. S , x >. } = { <. S , n >. } )
14 13 adantl 
 |-  ( ( ( m e. B /\ n e. B ) /\ x = n ) -> { <. S , x >. } = { <. S , n >. } )
15 simpr 
 |-  ( ( m e. B /\ n e. B ) -> n e. B )
16 snex 
 |-  { <. S , n >. } e. _V
17 16 a1i 
 |-  ( ( m e. B /\ n e. B ) -> { <. S , n >. } e. _V )
18 4 14 15 17 fvmptd 
 |-  ( ( m e. B /\ n e. B ) -> ( F ` n ) = { <. S , n >. } )
19 11 18 eqeq12d 
 |-  ( ( m e. B /\ n e. B ) -> ( ( F ` m ) = ( F ` n ) <-> { <. S , m >. } = { <. S , n >. } ) )
20 19 adantl 
 |-  ( ( S e. V /\ ( m e. B /\ n e. B ) ) -> ( ( F ` m ) = ( F ` n ) <-> { <. S , m >. } = { <. S , n >. } ) )
21 opex 
 |-  <. S , m >. e. _V
22 21 sneqr 
 |-  ( { <. S , m >. } = { <. S , n >. } -> <. S , m >. = <. S , n >. )
23 opthg 
 |-  ( ( S e. V /\ m e. B ) -> ( <. S , m >. = <. S , n >. <-> ( S = S /\ m = n ) ) )
24 23 adantrr 
 |-  ( ( S e. V /\ ( m e. B /\ n e. B ) ) -> ( <. S , m >. = <. S , n >. <-> ( S = S /\ m = n ) ) )
25 simpr 
 |-  ( ( S = S /\ m = n ) -> m = n )
26 24 25 syl6bi 
 |-  ( ( S e. V /\ ( m e. B /\ n e. B ) ) -> ( <. S , m >. = <. S , n >. -> m = n ) )
27 22 26 syl5 
 |-  ( ( S e. V /\ ( m e. B /\ n e. B ) ) -> ( { <. S , m >. } = { <. S , n >. } -> m = n ) )
28 20 27 sylbid 
 |-  ( ( S e. V /\ ( m e. B /\ n e. B ) ) -> ( ( F ` m ) = ( F ` n ) -> m = n ) )
29 28 ralrimivva 
 |-  ( S e. V -> A. m e. B A. n e. B ( ( F ` m ) = ( F ` n ) -> m = n ) )
30 dff13 
 |-  ( F : B -1-1-> A <-> ( F : B --> A /\ A. m e. B A. n e. B ( ( F ` m ) = ( F ` n ) -> m = n ) ) )
31 3 29 30 sylanbrc 
 |-  ( S e. V -> F : B -1-1-> A )