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=\left(x\in \left({2_{𝑜}}^A\right)⟼x^{-1}\left[\left\{1_{𝑜}\right\}\right]\right)$$
Assertion	pw2f1ocnv	$$⊢A\in V\to \left(F:{2_{𝑜}}^A\underset{1-1\; onto}{⟶}𝒫A\wedge F^{-1}=\left(y\in 𝒫A⟼\left(z\in A⟼if\left(z\in y,1_{𝑜},\varnothing \right)\right)\right)\right)$$

Proof

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