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

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	imbitrrid	⊢ ( 𝑋 = ∅ → ( 𝑋 ≼^* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) )
11		brwdomn0	⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼^* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )
12		vex	⊢ 𝑧 ∈ V
13		fopwdom	⊢ ( ( 𝑧 ∈ V ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → 𝒫 𝑋 ≼ 𝒫 𝑌 )
14	12 13	mpan	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → 𝒫 𝑋 ≼ 𝒫 𝑌 )
15	14	exlimiv	⊢ ( ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 → 𝒫 𝑋 ≼ 𝒫 𝑌 )
16	11 15	biimtrdi	⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼^* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) )
17	10 16	pm2.61ine	⊢ ( 𝑋 ≼^* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 )