brwdom3

Description: Condition for weak dominance with a condition reminiscent of wdomd . (Contributed by Stefan O'Rear, 13-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)

		Ref	Expression
	Assertion	brwdom3	$⊢ (X \in V \land Y \in W) \to (X ≼^{*} Y \leftrightarrow \exists f \forall x \in X \exists y \in Y x = f (y))$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ X \in V \to X \in V$
2		elex	$⊢ Y \in W \to Y \in V$
3		brwdom2	$⊢ Y \in V \to (X ≼^{*} Y \leftrightarrow \exists z \in 𝒫 Y \exists f f : z \underset{onto}{⟶} X)$
4	3	adantl	$⊢ (X \in V \land Y \in V) \to (X ≼^{*} Y \leftrightarrow \exists z \in 𝒫 Y \exists f f : z \underset{onto}{⟶} X)$
5		dffo3	$⊢ f : z \underset{onto}{⟶} X \leftrightarrow (f : z ⟶ X \land \forall x \in X \exists y \in z x = f (y))$
6	5	simprbi	$⊢ f : z \underset{onto}{⟶} X \to \forall x \in X \exists y \in z x = f (y)$
7		elpwi	$⊢ z \in 𝒫 Y \to z \subseteq Y$
8		ssrexv	$⊢ z \subseteq Y \to (\exists y \in z x = f (y) \to \exists y \in Y x = f (y))$
9	7 8	syl	$⊢ z \in 𝒫 Y \to (\exists y \in z x = f (y) \to \exists y \in Y x = f (y))$
10	9	adantl	$⊢ ((X \in V \land Y \in V) \land z \in 𝒫 Y) \to (\exists y \in z x = f (y) \to \exists y \in Y x = f (y))$
11	10	ralimdv	$⊢ ((X \in V \land Y \in V) \land z \in 𝒫 Y) \to (\forall x \in X \exists y \in z x = f (y) \to \forall x \in X \exists y \in Y x = f (y))$
12	6 11	syl5	$⊢ ((X \in V \land Y \in V) \land z \in 𝒫 Y) \to (f : z \underset{onto}{⟶} X \to \forall x \in X \exists y \in Y x = f (y))$
13	12	eximdv	$⊢ ((X \in V \land Y \in V) \land z \in 𝒫 Y) \to (\exists f f : z \underset{onto}{⟶} X \to \exists f \forall x \in X \exists y \in Y x = f (y))$
14	13	rexlimdva	$⊢ (X \in V \land Y \in V) \to (\exists z \in 𝒫 Y \exists f f : z \underset{onto}{⟶} X \to \exists f \forall x \in X \exists y \in Y x = f (y))$
15	4 14	sylbid	$⊢ (X \in V \land Y \in V) \to (X ≼^{*} Y \to \exists f \forall x \in X \exists y \in Y x = f (y))$
16		simpll	$⊢ ((X \in V \land Y \in V) \land \forall x \in X \exists y \in Y x = f (y)) \to X \in V$
17		simplr	$⊢ ((X \in V \land Y \in V) \land \forall x \in X \exists y \in Y x = f (y)) \to Y \in V$
18		eqeq1	$⊢ x = z \to (x = f (y) \leftrightarrow z = f (y))$
19	18	rexbidv	$⊢ x = z \to (\exists y \in Y x = f (y) \leftrightarrow \exists y \in Y z = f (y))$
20		fveq2	$⊢ y = w \to f (y) = f (w)$
21	20	eqeq2d	$⊢ y = w \to (z = f (y) \leftrightarrow z = f (w))$
22	21	cbvrexvw	$⊢ \exists y \in Y z = f (y) \leftrightarrow \exists w \in Y z = f (w)$
23	19 22	bitrdi	$⊢ x = z \to (\exists y \in Y x = f (y) \leftrightarrow \exists w \in Y z = f (w))$
24	23	cbvralvw	$⊢ \forall x \in X \exists y \in Y x = f (y) \leftrightarrow \forall z \in X \exists w \in Y z = f (w)$
25	24	biimpi	$⊢ \forall x \in X \exists y \in Y x = f (y) \to \forall z \in X \exists w \in Y z = f (w)$
26	25	adantl	$⊢ ((X \in V \land Y \in V) \land \forall x \in X \exists y \in Y x = f (y)) \to \forall z \in X \exists w \in Y z = f (w)$
27	26	r19.21bi	$⊢ (((X \in V \land Y \in V) \land \forall x \in X \exists y \in Y x = f (y)) \land z \in X) \to \exists w \in Y z = f (w)$
28	16 17 27	wdom2d	$⊢ ((X \in V \land Y \in V) \land \forall x \in X \exists y \in Y x = f (y)) \to X ≼^{*} Y$
29	28	ex	$⊢ (X \in V \land Y \in V) \to (\forall x \in X \exists y \in Y x = f (y) \to X ≼^{*} Y)$
30	29	exlimdv	$⊢ (X \in V \land Y \in V) \to (\exists f \forall x \in X \exists y \in Y x = f (y) \to X ≼^{*} Y)$
31	15 30	impbid	$⊢ (X \in V \land Y \in V) \to (X ≼^{*} Y \leftrightarrow \exists f \forall x \in X \exists y \in Y x = f (y))$
32	1 2 31	syl2an	$⊢ (X \in V \land Y \in W) \to (X ≼^{*} Y \leftrightarrow \exists f \forall x \in X \exists y \in Y x = f (y))$

Metamath Proof Explorer

Theorem brwdom3

Proof