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

Metamath Proof Explorer

Theorem pw2f1o

Description: The power set of a set is equinumerous to set exponentiation with an unordered pair base of ordinal 2. Generalized from Proposition 10.44 of TakeutiZaring p. 96. (Contributed by Mario Carneiro, 6-Oct-2014)

Ref Expression
Hypotheses pw2f1o.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
pw2f1o.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
pw2f1o.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
pw2f1o.4 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
pw2f1o.5 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) )
Assertion pw2f1o ( 𝜑 → 𝐹 : 𝒫 𝐴 –1-1-onto→ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) )

Proof

Step Hyp Ref Expression
1 pw2f1o.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 pw2f1o.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 pw2f1o.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
4 pw2f1o.4 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
5 pw2f1o.5 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) )
6 eqid ⊢ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) = ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) )
7 1 2 3 4 pw2f1olem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) = ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) ) ↔ ( ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) ∧ 𝑥 = ( ◡ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) “ { 𝐶 } ) ) ) )
8 7 biimpa ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) = ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) ) ) → ( ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) ∧ 𝑥 = ( ◡ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) “ { 𝐶 } ) ) )
9 6 8 mpanr2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) ∧ 𝑥 = ( ◡ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) “ { 𝐶 } ) ) )
10 9 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) )
11 vex ⊢ 𝑦 ∈ V
12 11 cnvex ⊢ ◡ 𝑦 ∈ V
13 12 imaex ⊢ ( ◡ 𝑦 “ { 𝐶 } ) ∈ V
14 13 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) ) → ( ◡ 𝑦 “ { 𝐶 } ) ∈ V )
15 1 2 3 4 pw2f1olem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , 𝐶 , 𝐵 ) ) ) ↔ ( 𝑦 ∈ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) ∧ 𝑥 = ( ◡ 𝑦 “ { 𝐶 } ) ) ) )
16 5 10 14 15 f1od ⊢ ( 𝜑 → 𝐹 : 𝒫 𝐴 –1-1-onto→ ( { 𝐵 , 𝐶 } ↑m 𝐴 ) )