This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⟶ 1-1 onto B → b ∈ 𝒫 A ⟼ F b : 𝒫 A ⟶ 1-1 onto 𝒫 B

Proof

Step Hyp Ref Expression
1 id ⊢ F : A ⟶ 1-1 onto B → F : A ⟶ 1-1 onto B
2 dff1o3 ⊢ F : A ⟶ 1-1 onto B ↔ F : A ⟶ onto B ∧ Fun ⁡ F -1
3 vex ⊢ a ∈ V
4 3 funimaex ⊢ Fun ⁡ F -1 → F -1 a ∈ V
5 2 4 simplbiim ⊢ F : A ⟶ 1-1 onto B → F -1 a ∈ V
6 f1ofun ⊢ F : A ⟶ 1-1 onto B → Fun ⁡ F
7 vex ⊢ b ∈ V
8 7 funimaex ⊢ Fun ⁡ F → F b ∈ V
9 6 8 syl ⊢ F : A ⟶ 1-1 onto B → F b ∈ V
10 1 5 9 f1opw2 ⊢ F : A ⟶ 1-1 onto B → b ∈ 𝒫 A ⟼ F b : 𝒫 A ⟶ 1-1 onto 𝒫 B