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	$⊢ X ≼^{*} Y \to 𝒫 X ≼ 𝒫 Y$

Proof

Step	Hyp	Ref	Expression
1		relwdom	$⊢ Rel ≼^{*}$
2	1	brrelex2i	$⊢ X ≼^{*} Y \to Y \in V$
3	2	pwexd	$⊢ X ≼^{*} Y \to 𝒫 Y \in V$
4		0ss	$⊢ \emptyset \subseteq Y$
5	4	sspwi	$⊢ 𝒫 \emptyset \subseteq 𝒫 Y$
6		ssdomg	$⊢ 𝒫 Y \in V \to (𝒫 \emptyset \subseteq 𝒫 Y \to 𝒫 \emptyset ≼ 𝒫 Y)$
7	3 5 6	mpisyl	$⊢ X ≼^{*} Y \to 𝒫 \emptyset ≼ 𝒫 Y$
8		pweq	$⊢ X = \emptyset \to 𝒫 X = 𝒫 \emptyset$
9	8	breq1d	$⊢ X = \emptyset \to (𝒫 X ≼ 𝒫 Y \leftrightarrow 𝒫 \emptyset ≼ 𝒫 Y)$
10	7 9	imbitrrid	$⊢ X = \emptyset \to (X ≼^{*} Y \to 𝒫 X ≼ 𝒫 Y)$
11		brwdomn0	$⊢ X \neq \emptyset \to (X ≼^{*} Y \leftrightarrow \exists z z : Y \underset{onto}{⟶} X)$
12		vex	$⊢ z \in V$
13		fopwdom	$⊢ (z \in V \land z : Y \underset{onto}{⟶} X) \to 𝒫 X ≼ 𝒫 Y$
14	12 13	mpan	$⊢ z : Y \underset{onto}{⟶} X \to 𝒫 X ≼ 𝒫 Y$
15	14	exlimiv	$⊢ \exists z z : Y \underset{onto}{⟶} X \to 𝒫 X ≼ 𝒫 Y$
16	11 15	biimtrdi	$⊢ X \neq \emptyset \to (X ≼^{*} Y \to 𝒫 X ≼ 𝒫 Y)$
17	10 16	pm2.61ine	$⊢ X ≼^{*} Y \to 𝒫 X ≼ 𝒫 Y$