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 𝐴 ) )