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