Metamath Proof Explorer

Theorem ixpsnf1o

Description: A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypothesis ixpsnf1o.f 
|- F = ( x e. A |-> ( { I } X. { x } ) )
Assertion ixpsnf1o 
|- ( I e. V -> F : A -1-1-onto-> X_ y e. { I } A )

Proof

Step Hyp Ref Expression
1 ixpsnf1o.f 
 |-  F = ( x e. A |-> ( { I } X. { x } ) )
2 snex 
 |-  { I } e. _V
3 snex 
 |-  { x } e. _V
4 2 3 xpex 
 |-  ( { I } X. { x } ) e. _V
5 4 a1i 
 |-  ( ( I e. V /\ x e. A ) -> ( { I } X. { x } ) e. _V )
6 vex 
 |-  a e. _V
7 6 rnex 
 |-  ran a e. _V
8 7 uniex 
 |-  U. ran a e. _V
9 8 a1i 
 |-  ( ( I e. V /\ a e. X_ y e. { I } A ) -> U. ran a e. _V )
10 sneq 
 |-  ( b = I -> { b } = { I } )
11 10 xpeq1d 
 |-  ( b = I -> ( { b } X. { x } ) = ( { I } X. { x } ) )
12 11 eqeq2d 
 |-  ( b = I -> ( a = ( { b } X. { x } ) <-> a = ( { I } X. { x } ) ) )
13 12 anbi2d 
 |-  ( b = I -> ( ( x e. A /\ a = ( { b } X. { x } ) ) <-> ( x e. A /\ a = ( { I } X. { x } ) ) ) )
14 elixpsn 
 |-  ( b e. _V -> ( a e. X_ y e. { b } A <-> E. c e. A a = { <. b , c >. } ) )
15 14 elv 
 |-  ( a e. X_ y e. { b } A <-> E. c e. A a = { <. b , c >. } )
16 10 ixpeq1d 
 |-  ( b = I -> X_ y e. { b } A = X_ y e. { I } A )
17 16 eleq2d 
 |-  ( b = I -> ( a e. X_ y e. { b } A <-> a e. X_ y e. { I } A ) )
18 15 17 bitr3id 
 |-  ( b = I -> ( E. c e. A a = { <. b , c >. } <-> a e. X_ y e. { I } A ) )
19 18 anbi1d 
 |-  ( b = I -> ( ( E. c e. A a = { <. b , c >. } /\ x = U. ran a ) <-> ( a e. X_ y e. { I } A /\ x = U. ran a ) ) )
20 vex 
 |-  b e. _V
21 vex 
 |-  x e. _V
22 20 21 xpsn 
 |-  ( { b } X. { x } ) = { <. b , x >. }
23 22 eqeq2i 
 |-  ( a = ( { b } X. { x } ) <-> a = { <. b , x >. } )
24 23 anbi2i 
 |-  ( ( x e. A /\ a = ( { b } X. { x } ) ) <-> ( x e. A /\ a = { <. b , x >. } ) )
25 eqid 
 |-  { <. b , x >. } = { <. b , x >. }
26 opeq2 
 |-  ( c = x -> <. b , c >. = <. b , x >. )
27 26 sneqd 
 |-  ( c = x -> { <. b , c >. } = { <. b , x >. } )
28 27 rspceeqv 
 |-  ( ( x e. A /\ { <. b , x >. } = { <. b , x >. } ) -> E. c e. A { <. b , x >. } = { <. b , c >. } )
29 25 28 mpan2 
 |-  ( x e. A -> E. c e. A { <. b , x >. } = { <. b , c >. } )
30 20 21 op2nda 
 |-  U. ran { <. b , x >. } = x
31 30 eqcomi 
 |-  x = U. ran { <. b , x >. }
32 29 31 jctir 
 |-  ( x e. A -> ( E. c e. A { <. b , x >. } = { <. b , c >. } /\ x = U. ran { <. b , x >. } ) )
33 eqeq1 
 |-  ( a = { <. b , x >. } -> ( a = { <. b , c >. } <-> { <. b , x >. } = { <. b , c >. } ) )
34 33 rexbidv 
 |-  ( a = { <. b , x >. } -> ( E. c e. A a = { <. b , c >. } <-> E. c e. A { <. b , x >. } = { <. b , c >. } ) )
35 rneq 
 |-  ( a = { <. b , x >. } -> ran a = ran { <. b , x >. } )
36 35 unieqd 
 |-  ( a = { <. b , x >. } -> U. ran a = U. ran { <. b , x >. } )
37 36 eqeq2d 
 |-  ( a = { <. b , x >. } -> ( x = U. ran a <-> x = U. ran { <. b , x >. } ) )
38 34 37 anbi12d 
 |-  ( a = { <. b , x >. } -> ( ( E. c e. A a = { <. b , c >. } /\ x = U. ran a ) <-> ( E. c e. A { <. b , x >. } = { <. b , c >. } /\ x = U. ran { <. b , x >. } ) ) )
39 32 38 syl5ibrcom 
 |-  ( x e. A -> ( a = { <. b , x >. } -> ( E. c e. A a = { <. b , c >. } /\ x = U. ran a ) ) )
40 39 imp 
 |-  ( ( x e. A /\ a = { <. b , x >. } ) -> ( E. c e. A a = { <. b , c >. } /\ x = U. ran a ) )
41 vex 
 |-  c e. _V
42 20 41 op2nda 
 |-  U. ran { <. b , c >. } = c
43 42 eqeq2i 
 |-  ( x = U. ran { <. b , c >. } <-> x = c )
44 eqidd 
 |-  ( c e. A -> { <. b , c >. } = { <. b , c >. } )
45 44 ancli 
 |-  ( c e. A -> ( c e. A /\ { <. b , c >. } = { <. b , c >. } ) )
46 eleq1w 
 |-  ( x = c -> ( x e. A <-> c e. A ) )
47 opeq2 
 |-  ( x = c -> <. b , x >. = <. b , c >. )
48 47 sneqd 
 |-  ( x = c -> { <. b , x >. } = { <. b , c >. } )
49 48 eqeq2d 
 |-  ( x = c -> ( { <. b , c >. } = { <. b , x >. } <-> { <. b , c >. } = { <. b , c >. } ) )
50 46 49 anbi12d 
 |-  ( x = c -> ( ( x e. A /\ { <. b , c >. } = { <. b , x >. } ) <-> ( c e. A /\ { <. b , c >. } = { <. b , c >. } ) ) )
51 45 50 syl5ibrcom 
 |-  ( c e. A -> ( x = c -> ( x e. A /\ { <. b , c >. } = { <. b , x >. } ) ) )
52 43 51 biimtrid 
 |-  ( c e. A -> ( x = U. ran { <. b , c >. } -> ( x e. A /\ { <. b , c >. } = { <. b , x >. } ) ) )
53 rneq 
 |-  ( a = { <. b , c >. } -> ran a = ran { <. b , c >. } )
54 53 unieqd 
 |-  ( a = { <. b , c >. } -> U. ran a = U. ran { <. b , c >. } )
55 54 eqeq2d 
 |-  ( a = { <. b , c >. } -> ( x = U. ran a <-> x = U. ran { <. b , c >. } ) )
56 eqeq1 
 |-  ( a = { <. b , c >. } -> ( a = { <. b , x >. } <-> { <. b , c >. } = { <. b , x >. } ) )
57 56 anbi2d 
 |-  ( a = { <. b , c >. } -> ( ( x e. A /\ a = { <. b , x >. } ) <-> ( x e. A /\ { <. b , c >. } = { <. b , x >. } ) ) )
58 55 57 imbi12d 
 |-  ( a = { <. b , c >. } -> ( ( x = U. ran a -> ( x e. A /\ a = { <. b , x >. } ) ) <-> ( x = U. ran { <. b , c >. } -> ( x e. A /\ { <. b , c >. } = { <. b , x >. } ) ) ) )
59 52 58 syl5ibrcom 
 |-  ( c e. A -> ( a = { <. b , c >. } -> ( x = U. ran a -> ( x e. A /\ a = { <. b , x >. } ) ) ) )
60 59 rexlimiv 
 |-  ( E. c e. A a = { <. b , c >. } -> ( x = U. ran a -> ( x e. A /\ a = { <. b , x >. } ) ) )
61 60 imp 
 |-  ( ( E. c e. A a = { <. b , c >. } /\ x = U. ran a ) -> ( x e. A /\ a = { <. b , x >. } ) )
62 40 61 impbii 
 |-  ( ( x e. A /\ a = { <. b , x >. } ) <-> ( E. c e. A a = { <. b , c >. } /\ x = U. ran a ) )
63 24 62 bitri 
 |-  ( ( x e. A /\ a = ( { b } X. { x } ) ) <-> ( E. c e. A a = { <. b , c >. } /\ x = U. ran a ) )
64 13 19 63 vtoclbg 
 |-  ( I e. V -> ( ( x e. A /\ a = ( { I } X. { x } ) ) <-> ( a e. X_ y e. { I } A /\ x = U. ran a ) ) )
65 1 5 9 64 f1od 
 |-  ( I e. V -> F : A -1-1-onto-> X_ y e. { I } A )