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	syl6bi	⊢ ( ¬ 𝑤 ∈ 𝑦 → ( 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		ffvelrn	⊢ ( ( 𝑥 : 𝐴 ⟶ 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 , ∅ ) ) ) ) )