Metamath Proof Explorer


Theorem wdompwdom

Description: Weak dominance strengthens to usual dominance on the power sets. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion wdompwdom ( 𝑋* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 )

Proof

Step Hyp Ref Expression
1 relwdom Rel ≼*
2 1 brrelex2i ( 𝑋* 𝑌𝑌 ∈ V )
3 2 pwexd ( 𝑋* 𝑌 → 𝒫 𝑌 ∈ V )
4 0ss ∅ ⊆ 𝑌
5 4 sspwi 𝒫 ∅ ⊆ 𝒫 𝑌
6 ssdomg ( 𝒫 𝑌 ∈ V → ( 𝒫 ∅ ⊆ 𝒫 𝑌 → 𝒫 ∅ ≼ 𝒫 𝑌 ) )
7 3 5 6 mpisyl ( 𝑋* 𝑌 → 𝒫 ∅ ≼ 𝒫 𝑌 )
8 pweq ( 𝑋 = ∅ → 𝒫 𝑋 = 𝒫 ∅ )
9 8 breq1d ( 𝑋 = ∅ → ( 𝒫 𝑋 ≼ 𝒫 𝑌 ↔ 𝒫 ∅ ≼ 𝒫 𝑌 ) )
10 7 9 syl5ibr ( 𝑋 = ∅ → ( 𝑋* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) )
11 brwdomn0 ( 𝑋 ≠ ∅ → ( 𝑋* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌onto𝑋 ) )
12 vex 𝑧 ∈ V
13 fopwdom ( ( 𝑧 ∈ V ∧ 𝑧 : 𝑌onto𝑋 ) → 𝒫 𝑋 ≼ 𝒫 𝑌 )
14 12 13 mpan ( 𝑧 : 𝑌onto𝑋 → 𝒫 𝑋 ≼ 𝒫 𝑌 )
15 14 exlimiv ( ∃ 𝑧 𝑧 : 𝑌onto𝑋 → 𝒫 𝑋 ≼ 𝒫 𝑌 )
16 11 15 syl6bi ( 𝑋 ≠ ∅ → ( 𝑋* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) )
17 10 16 pm2.61ine ( 𝑋* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 )