Metamath Proof Explorer

Theorem pw2f1ocnv

Description: Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en , which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Stefan O'Rear, 9-Jul-2015)

Ref Expression
Hypothesis pw2f1o2.f 
|- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )
Assertion pw2f1ocnv 
|- ( A e. V -> ( F : ( 2o ^m A ) -1-1-onto-> ~P A /\ `' F = ( y e. ~P A |-> ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pw2f1o2.f 
 |-  F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )
2 vex 
 |-  x e. _V
3 2 cnvex 
 |-  `' x e. _V
4 imaexg 
 |-  ( `' x e. _V -> ( `' x " { 1o } ) e. _V )
5 3 4 mp1i 
 |-  ( ( A e. V /\ x e. ( 2o ^m A ) ) -> ( `' x " { 1o } ) e. _V )
6 mptexg 
 |-  ( A e. V -> ( z e. A |-> if ( z e. y , 1o , (/) ) ) e. _V )
7 6 adantr 
 |-  ( ( A e. V /\ y e. ~P A ) -> ( z e. A |-> if ( z e. y , 1o , (/) ) ) e. _V )
8 2on 
 |-  2o e. On
9 elmapg 
 |-  ( ( 2o e. On /\ A e. V ) -> ( x e. ( 2o ^m A ) <-> x : A --> 2o ) )
10 8 9 mpan 
 |-  ( A e. V -> ( x e. ( 2o ^m A ) <-> x : A --> 2o ) )
11 10 anbi1d 
 |-  ( A e. V -> ( ( x e. ( 2o ^m A ) /\ y = ( `' x " { 1o } ) ) <-> ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) ) )
12 1oex 
 |-  1o e. _V
13 12 sucid 
 |-  1o e. suc 1o
14 df-2o 
 |-  2o = suc 1o
15 13 14 eleqtrri 
 |-  1o e. 2o
16 0ex 
 |-  (/) e. _V
17 16 prid1 
 |-  (/) e. { (/) , { (/) } }
18 df2o2 
 |-  2o = { (/) , { (/) } }
19 17 18 eleqtrri 
 |-  (/) e. 2o
20 15 19 ifcli 
 |-  if ( z e. y , 1o , (/) ) e. 2o
21 20 rgenw 
 |-  A. z e. A if ( z e. y , 1o , (/) ) e. 2o
22 eqid 
 |-  ( z e. A |-> if ( z e. y , 1o , (/) ) ) = ( z e. A |-> if ( z e. y , 1o , (/) ) )
23 22 fmpt 
 |-  ( A. z e. A if ( z e. y , 1o , (/) ) e. 2o <-> ( z e. A |-> if ( z e. y , 1o , (/) ) ) : A --> 2o )
24 21 23 mpbi 
 |-  ( z e. A |-> if ( z e. y , 1o , (/) ) ) : A --> 2o
25 simpr 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) )
26 25 feq1d 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> ( x : A --> 2o <-> ( z e. A |-> if ( z e. y , 1o , (/) ) ) : A --> 2o ) )
27 24 26 mpbiri 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> x : A --> 2o )
28 iftrue 
 |-  ( w e. y -> if ( w e. y , 1o , (/) ) = 1o )
29 noel 
 |-  -. (/) e. (/)
30 iffalse 
 |-  ( -. w e. y -> if ( w e. y , 1o , (/) ) = (/) )
31 30 eqeq1d 
 |-  ( -. w e. y -> ( if ( w e. y , 1o , (/) ) = 1o <-> (/) = 1o ) )
32 0lt1o 
 |-  (/) e. 1o
33 eleq2 
 |-  ( (/) = 1o -> ( (/) e. (/) <-> (/) e. 1o ) )
34 32 33 mpbiri 
 |-  ( (/) = 1o -> (/) e. (/) )
35 31 34 syl6bi 
 |-  ( -. w e. y -> ( if ( w e. y , 1o , (/) ) = 1o -> (/) e. (/) ) )
36 29 35 mtoi 
 |-  ( -. w e. y -> -. if ( w e. y , 1o , (/) ) = 1o )
37 36 con4i 
 |-  ( if ( w e. y , 1o , (/) ) = 1o -> w e. y )
38 28 37 impbii 
 |-  ( w e. y <-> if ( w e. y , 1o , (/) ) = 1o )
39 25 fveq1d 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> ( x ` w ) = ( ( z e. A |-> if ( z e. y , 1o , (/) ) ) ` w ) )
40 elequ1 
 |-  ( z = w -> ( z e. y <-> w e. y ) )
41 40 ifbid 
 |-  ( z = w -> if ( z e. y , 1o , (/) ) = if ( w e. y , 1o , (/) ) )
42 12 16 ifcli 
 |-  if ( w e. y , 1o , (/) ) e. _V
43 41 22 42 fvmpt 
 |-  ( w e. A -> ( ( z e. A |-> if ( z e. y , 1o , (/) ) ) ` w ) = if ( w e. y , 1o , (/) ) )
44 39 43 sylan9eq 
 |-  ( ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) /\ w e. A ) -> ( x ` w ) = if ( w e. y , 1o , (/) ) )
45 44 eqeq1d 
 |-  ( ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) /\ w e. A ) -> ( ( x ` w ) = 1o <-> if ( w e. y , 1o , (/) ) = 1o ) )
46 38 45 bitr4id 
 |-  ( ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) /\ w e. A ) -> ( w e. y <-> ( x ` w ) = 1o ) )
47 fvex 
 |-  ( x ` w ) e. _V
48 47 elsn 
 |-  ( ( x ` w ) e. { 1o } <-> ( x ` w ) = 1o )
49 46 48 bitr4di 
 |-  ( ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) /\ w e. A ) -> ( w e. y <-> ( x ` w ) e. { 1o } ) )
50 49 pm5.32da 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> ( ( w e. A /\ w e. y ) <-> ( w e. A /\ ( x ` w ) e. { 1o } ) ) )
51 ssel 
 |-  ( y C_ A -> ( w e. y -> w e. A ) )
52 51 adantr 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> ( w e. y -> w e. A ) )
53 52 pm4.71rd 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> ( w e. y <-> ( w e. A /\ w e. y ) ) )
54 ffn 
 |-  ( x : A --> 2o -> x Fn A )
55 elpreima 
 |-  ( x Fn A -> ( w e. ( `' x " { 1o } ) <-> ( w e. A /\ ( x ` w ) e. { 1o } ) ) )
56 27 54 55 3syl 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> ( w e. ( `' x " { 1o } ) <-> ( w e. A /\ ( x ` w ) e. { 1o } ) ) )
57 50 53 56 3bitr4d 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> ( w e. y <-> w e. ( `' x " { 1o } ) ) )
58 57 eqrdv 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> y = ( `' x " { 1o } ) )
59 27 58 jca 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) -> ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) )
60 simpr 
 |-  ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) -> y = ( `' x " { 1o } ) )
61 cnvimass 
 |-  ( `' x " { 1o } ) C_ dom x
62 fdm 
 |-  ( x : A --> 2o -> dom x = A )
63 62 adantr 
 |-  ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) -> dom x = A )
64 61 63 sseqtrid 
 |-  ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) -> ( `' x " { 1o } ) C_ A )
65 60 64 eqsstrd 
 |-  ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) -> y C_ A )
66 simplr 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> y = ( `' x " { 1o } ) )
67 66 eleq2d 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( w e. y <-> w e. ( `' x " { 1o } ) ) )
68 54 adantr 
 |-  ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) -> x Fn A )
69 fnbrfvb 
 |-  ( ( x Fn A /\ w e. A ) -> ( ( x ` w ) = 1o <-> w x 1o ) )
70 68 69 sylan 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( ( x ` w ) = 1o <-> w x 1o ) )
71 1on 
 |-  1o e. On
72 vex 
 |-  w e. _V
73 72 eliniseg 
 |-  ( 1o e. On -> ( w e. ( `' x " { 1o } ) <-> w x 1o ) )
74 71 73 ax-mp 
 |-  ( w e. ( `' x " { 1o } ) <-> w x 1o )
75 70 74 bitr4di 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( ( x ` w ) = 1o <-> w e. ( `' x " { 1o } ) ) )
76 67 75 bitr4d 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( w e. y <-> ( x ` w ) = 1o ) )
77 76 biimpa 
 |-  ( ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) /\ w e. y ) -> ( x ` w ) = 1o )
78 28 adantl 
 |-  ( ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) /\ w e. y ) -> if ( w e. y , 1o , (/) ) = 1o )
79 77 78 eqtr4d 
 |-  ( ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) /\ w e. y ) -> ( x ` w ) = if ( w e. y , 1o , (/) ) )
80 ffvelrn 
 |-  ( ( x : A --> 2o /\ w e. A ) -> ( x ` w ) e. 2o )
81 80 adantlr 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( x ` w ) e. 2o )
82 df2o3 
 |-  2o = { (/) , 1o }
83 81 82 eleqtrdi 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( x ` w ) e. { (/) , 1o } )
84 47 elpr 
 |-  ( ( x ` w ) e. { (/) , 1o } <-> ( ( x ` w ) = (/) \/ ( x ` w ) = 1o ) )
85 83 84 sylib 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( ( x ` w ) = (/) \/ ( x ` w ) = 1o ) )
86 85 ord 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( -. ( x ` w ) = (/) -> ( x ` w ) = 1o ) )
87 86 76 sylibrd 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( -. ( x ` w ) = (/) -> w e. y ) )
88 87 con1d 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( -. w e. y -> ( x ` w ) = (/) ) )
89 88 imp 
 |-  ( ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) /\ -. w e. y ) -> ( x ` w ) = (/) )
90 30 adantl 
 |-  ( ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) /\ -. w e. y ) -> if ( w e. y , 1o , (/) ) = (/) )
91 89 90 eqtr4d 
 |-  ( ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) /\ -. w e. y ) -> ( x ` w ) = if ( w e. y , 1o , (/) ) )
92 79 91 pm2.61dan 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( x ` w ) = if ( w e. y , 1o , (/) ) )
93 43 adantl 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( ( z e. A |-> if ( z e. y , 1o , (/) ) ) ` w ) = if ( w e. y , 1o , (/) ) )
94 92 93 eqtr4d 
 |-  ( ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) /\ w e. A ) -> ( x ` w ) = ( ( z e. A |-> if ( z e. y , 1o , (/) ) ) ` w ) )
95 94 ralrimiva 
 |-  ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) -> A. w e. A ( x ` w ) = ( ( z e. A |-> if ( z e. y , 1o , (/) ) ) ` w ) )
96 ffn 
 |-  ( ( z e. A |-> if ( z e. y , 1o , (/) ) ) : A --> 2o -> ( z e. A |-> if ( z e. y , 1o , (/) ) ) Fn A )
97 24 96 ax-mp 
 |-  ( z e. A |-> if ( z e. y , 1o , (/) ) ) Fn A
98 eqfnfv 
 |-  ( ( x Fn A /\ ( z e. A |-> if ( z e. y , 1o , (/) ) ) Fn A ) -> ( x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) <-> A. w e. A ( x ` w ) = ( ( z e. A |-> if ( z e. y , 1o , (/) ) ) ` w ) ) )
99 68 97 98 sylancl 
 |-  ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) -> ( x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) <-> A. w e. A ( x ` w ) = ( ( z e. A |-> if ( z e. y , 1o , (/) ) ) ` w ) ) )
100 95 99 mpbird 
 |-  ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) -> x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) )
101 65 100 jca 
 |-  ( ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) -> ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) )
102 59 101 impbii 
 |-  ( ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) <-> ( x : A --> 2o /\ y = ( `' x " { 1o } ) ) )
103 11 102 bitr4di 
 |-  ( A e. V -> ( ( x e. ( 2o ^m A ) /\ y = ( `' x " { 1o } ) ) <-> ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) ) )
104 velpw 
 |-  ( y e. ~P A <-> y C_ A )
105 104 anbi1i 
 |-  ( ( y e. ~P A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) <-> ( y C_ A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) )
106 103 105 bitr4di 
 |-  ( A e. V -> ( ( x e. ( 2o ^m A ) /\ y = ( `' x " { 1o } ) ) <-> ( y e. ~P A /\ x = ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) ) )
107 1 5 7 106 f1ocnvd 
 |-  ( A e. V -> ( F : ( 2o ^m A ) -1-1-onto-> ~P A /\ `' F = ( y e. ~P A |-> ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) ) )