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		sspwb	⊢ ( ∅ ⊆ 𝑌 ↔ 𝒫 ∅ ⊆ 𝒫 𝑌 )
6	4 5	mpbi	⊢ 𝒫 ∅ ⊆ 𝒫 𝑌
7		ssdomg	⊢ ( 𝒫 𝑌 ∈ V → ( 𝒫 ∅ ⊆ 𝒫 𝑌 → 𝒫 ∅ ≼ 𝒫 𝑌 ) )
8	3 6 7	mpisyl	⊢ ( 𝑋 ≼* 𝑌 → 𝒫 ∅ ≼ 𝒫 𝑌 )
9		pweq	⊢ ( 𝑋 = ∅ → 𝒫 𝑋 = 𝒫 ∅ )
10	9	breq1d	⊢ ( 𝑋 = ∅ → ( 𝒫 𝑋 ≼ 𝒫 𝑌 ↔ 𝒫 ∅ ≼ 𝒫 𝑌 ) )
11	8 10	syl5ibr	⊢ ( 𝑋 = ∅ → ( 𝑋 ≼* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) )
12		brwdomn0	⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )
13		vex	⊢ 𝑧 ∈ V
14		fopwdom	⊢ ( ( 𝑧 ∈ V ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → 𝒫 𝑋 ≼ 𝒫 𝑌 )
15	13 14	mpan	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → 𝒫 𝑋 ≼ 𝒫 𝑌 )
16	15	exlimiv	⊢ ( ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 → 𝒫 𝑋 ≼ 𝒫 𝑌 )
17	12 16	syl6bi	⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) )
18	11 17	pm2.61ine	⊢ ( 𝑋 ≼* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 )