Theorem f1opw

Description: A one-to-one mapping induces a one-to-one mapping on power sets. (Contributed by Stefan O'Rear, 18-Nov-2014) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Assertion	f1opw	$$⊢F:A\underset{1-1\; onto}{⟶}B\to \left(b\in 𝒫A⟼F\left[b\right]\right):𝒫A\underset{1-1\; onto}{⟶}𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F:A\underset{1-1\; onto}{⟶}B$$
2		dff1o3	$$⊢F:A\underset{1-1\; onto}{⟶}B\leftrightarrow \left(F:A\underset{onto}{⟶}B\wedge \mathrm{Fun}{F}^{-1}\right)$$
3		vex	$$⊢a\in \mathrm{V}$$
4	3	funimaex	$$⊢\mathrm{Fun}{F}^{-1}\to F^{-1}\left[a\right]\in \mathrm{V}$$
5	2 4	simplbiim	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F^{-1}\left[a\right]\in \mathrm{V}$$
6		f1ofun	$$⊢F:A\underset{1-1\; onto}{⟶}B\to \mathrm{Fun}F$$
7		vex	$$⊢b\in \mathrm{V}$$
8	7	funimaex	$$⊢\mathrm{Fun}F\to F\left[b\right]\in \mathrm{V}$$
9	6 8	syl	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F\left[b\right]\in \mathrm{V}$$
10	1 5 9	f1opw2	$$⊢F:A\underset{1-1\; onto}{⟶}B\to \left(b\in 𝒫A⟼F\left[b\right]\right):𝒫A\underset{1-1\; onto}{⟶}𝒫B$$