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	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑏 ∈ 𝒫 𝐴 ↦ ( 𝐹 “ 𝑏 ) ) : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
2		dff1o3	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Fun ◡ 𝐹 ) )
3		vex	⊢ 𝑎 ∈ V
4	3	funimaex	⊢ ( Fun ◡ 𝐹 → ( ◡ 𝐹 “ 𝑎 ) ∈ V )
5	2 4	simplbiim	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ 𝐹 “ 𝑎 ) ∈ V )
6		f1ofun	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → Fun 𝐹 )
7		vex	⊢ 𝑏 ∈ V
8	7	funimaex	⊢ ( Fun 𝐹 → ( 𝐹 “ 𝑏 ) ∈ V )
9	6 8	syl	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐹 “ 𝑏 ) ∈ V )
10	1 5 9	f1opw2	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑏 ∈ 𝒫 𝐴 ↦ ( 𝐹 “ 𝑏 ) ) : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐵 )