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 syl5bi
 |-  ( 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 )