Theorem pwdom

Description: Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015)

	Ref	Expression
Assertion	pwdom	⊢ ( 𝐴 ≼ 𝐵 → 𝒫 𝐴 ≼ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		pweq	⊢ ( 𝐴 = ∅ → 𝒫 𝐴 = 𝒫 ∅ )
2	1	breq1d	⊢ ( 𝐴 = ∅ → ( 𝒫 𝐴 ≼ 𝒫 𝐵 ↔ 𝒫 ∅ ≼ 𝒫 𝐵 ) )
3		reldom	⊢ Rel ≼
4	3	brrelex1i	⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ V )
5		0sdomg	⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
6	4 5	syl	⊢ ( 𝐴 ≼ 𝐵 → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
7	6	biimpar	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐴 ≠ ∅ ) → ∅ ≺ 𝐴 )
8		simpl	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐴 ≠ ∅ ) → 𝐴 ≼ 𝐵 )
9		fodomr	⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 )
10	7 8 9	syl2anc	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 )
11		vex	⊢ 𝑓 ∈ V
12		fopwdom	⊢ ( ( 𝑓 ∈ V ∧ 𝑓 : 𝐵 –onto→ 𝐴 ) → 𝒫 𝐴 ≼ 𝒫 𝐵 )
13	11 12	mpan	⊢ ( 𝑓 : 𝐵 –onto→ 𝐴 → 𝒫 𝐴 ≼ 𝒫 𝐵 )
14	13	exlimiv	⊢ ( ∃ 𝑓 𝑓 : 𝐵 –onto→ 𝐴 → 𝒫 𝐴 ≼ 𝒫 𝐵 )
15	10 14	syl	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐴 ≠ ∅ ) → 𝒫 𝐴 ≼ 𝒫 𝐵 )
16	3	brrelex2i	⊢ ( 𝐴 ≼ 𝐵 → 𝐵 ∈ V )
17	16	pwexd	⊢ ( 𝐴 ≼ 𝐵 → 𝒫 𝐵 ∈ V )
18		0ss	⊢ ∅ ⊆ 𝐵
19	18	sspwi	⊢ 𝒫 ∅ ⊆ 𝒫 𝐵
20		ssdomg	⊢ ( 𝒫 𝐵 ∈ V → ( 𝒫 ∅ ⊆ 𝒫 𝐵 → 𝒫 ∅ ≼ 𝒫 𝐵 ) )
21	17 19 20	mpisyl	⊢ ( 𝐴 ≼ 𝐵 → 𝒫 ∅ ≼ 𝒫 𝐵 )
22	2 15 21	pm2.61ne	⊢ ( 𝐴 ≼ 𝐵 → 𝒫 𝐴 ≼ 𝒫 𝐵 )