This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑥 “ { 1o } ) )
Assertion pw2f1ocnv ( 𝐴 ∈ 𝑉 → ( 𝐹 : ( 2o ↑m 𝐴 ) –1-1-onto→ 𝒫 𝐴 ∧ ◡ 𝐹 = ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑦 , 1o , ∅ ) ) ) ) )

Proof

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