Theorem f1opw2

Description: A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw avoids the Axiom of Replacement. (Contributed by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	f1opw2.1	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
	f1opw2.2	$$⊢\phi \to F^{-1}\left[a\right]\in \mathrm{V}$$
	f1opw2.3	$$⊢\phi \to F\left[b\right]\in \mathrm{V}$$
Assertion	f1opw2	$$⊢\phi \to \left(b\in 𝒫A⟼F\left[b\right]\right):𝒫A\underset{1-1\; onto}{⟶}𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		f1opw2.1	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
2		f1opw2.2	$$⊢\phi \to F^{-1}\left[a\right]\in \mathrm{V}$$
3		f1opw2.3	$$⊢\phi \to F\left[b\right]\in \mathrm{V}$$
4		eqid	$$⊢\left(b\in 𝒫A⟼F\left[b\right]\right)=\left(b\in 𝒫A⟼F\left[b\right]\right)$$
5		imassrn	$$⊢F\left[b\right]\subseteq \mathrm{ran}F$$
6		f1ofo	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F:A\underset{onto}{⟶}B$$
7	1 6	syl	$$⊢\phi \to F:A\underset{onto}{⟶}B$$
8		forn	$$⊢F:A\underset{onto}{⟶}B\to \mathrm{ran}F=B$$
9	7 8	syl	$$⊢\phi \to \mathrm{ran}F=B$$
10	5 9	sseqtrid	$$⊢\phi \to F\left[b\right]\subseteq B$$
11	3 10	elpwd	$$⊢\phi \to F\left[b\right]\in 𝒫B$$
12	11	adantr	$$⊢\left(\phi \wedge b\in 𝒫A\right)\to F\left[b\right]\in 𝒫B$$
13		imassrn	$$⊢F^{-1}\left[a\right]\subseteq \mathrm{ran}{F}^{-1}$$
14		dfdm4	$$⊢\mathrm{dom}F=\mathrm{ran}{F}^{-1}$$
15		f1odm	$$⊢F:A\underset{1-1\; onto}{⟶}B\to \mathrm{dom}F=A$$
16	1 15	syl	$$⊢\phi \to \mathrm{dom}F=A$$
17	14 16	eqtr3id	$$⊢\phi \to \mathrm{ran}{F}^{-1}=A$$
18	13 17	sseqtrid	$$⊢\phi \to F^{-1}\left[a\right]\subseteq A$$
19	2 18	elpwd	$$⊢\phi \to F^{-1}\left[a\right]\in 𝒫A$$
20	19	adantr	$$⊢\left(\phi \wedge a\in 𝒫B\right)\to F^{-1}\left[a\right]\in 𝒫A$$
21		elpwi	$$⊢a\in 𝒫B\to a\subseteq B$$
22	21	adantl	$$⊢\left(b\in 𝒫A\wedge a\in 𝒫B\right)\to a\subseteq B$$
23		foimacnv	$$⊢\left(F:A\underset{onto}{⟶}B\wedge a\subseteq B\right)\to F\left[F^{-1}\left[a\right]\right]=a$$
24	7 22 23	syl2an	$$⊢\left(\phi \wedge \left(b\in 𝒫A\wedge a\in 𝒫B\right)\right)\to F\left[F^{-1}\left[a\right]\right]=a$$
25	24	eqcomd	$$⊢\left(\phi \wedge \left(b\in 𝒫A\wedge a\in 𝒫B\right)\right)\to a=F\left[F^{-1}\left[a\right]\right]$$
26		imaeq2	$$⊢b=F^{-1}\left[a\right]\to F\left[b\right]=F\left[F^{-1}\left[a\right]\right]$$
27	26	eqeq2d	$$⊢b=F^{-1}\left[a\right]\to \left(a=F\left[b\right]\leftrightarrow a=F\left[F^{-1}\left[a\right]\right]\right)$$
28	25 27	syl5ibrcom	$$⊢\left(\phi \wedge \left(b\in 𝒫A\wedge a\in 𝒫B\right)\right)\to \left(b=F^{-1}\left[a\right]\to a=F\left[b\right]\right)$$
29		f1of1	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F:A\underset{1-1}{⟶}B$$
30	1 29	syl	$$⊢\phi \to F:A\underset{1-1}{⟶}B$$
31		elpwi	$$⊢b\in 𝒫A\to b\subseteq A$$
32	31	adantr	$$⊢\left(b\in 𝒫A\wedge a\in 𝒫B\right)\to b\subseteq A$$
33		f1imacnv	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge b\subseteq A\right)\to F^{-1}\left[F\left[b\right]\right]=b$$
34	30 32 33	syl2an	$$⊢\left(\phi \wedge \left(b\in 𝒫A\wedge a\in 𝒫B\right)\right)\to F^{-1}\left[F\left[b\right]\right]=b$$
35	34	eqcomd	$$⊢\left(\phi \wedge \left(b\in 𝒫A\wedge a\in 𝒫B\right)\right)\to b=F^{-1}\left[F\left[b\right]\right]$$
36		imaeq2	$$⊢a=F\left[b\right]\to F^{-1}\left[a\right]=F^{-1}\left[F\left[b\right]\right]$$
37	36	eqeq2d	$$⊢a=F\left[b\right]\to \left(b=F^{-1}\left[a\right]\leftrightarrow b=F^{-1}\left[F\left[b\right]\right]\right)$$
38	35 37	syl5ibrcom	$$⊢\left(\phi \wedge \left(b\in 𝒫A\wedge a\in 𝒫B\right)\right)\to \left(a=F\left[b\right]\to b=F^{-1}\left[a\right]\right)$$
39	28 38	impbid	$$⊢\left(\phi \wedge \left(b\in 𝒫A\wedge a\in 𝒫B\right)\right)\to \left(b=F^{-1}\left[a\right]\leftrightarrow a=F\left[b\right]\right)$$
40	4 12 20 39	f1o2d	$$⊢\phi \to \left(b\in 𝒫A⟼F\left[b\right]\right):𝒫A\underset{1-1\; onto}{⟶}𝒫B$$