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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ≼ 𝐵 → 𝒫 𝐴 ≼ 𝒫 𝐵 )