brwdom2

Description: Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015)

		Ref	Expression
	Assertion	brwdom2	$⊢ Y \in V \to (X ≼^{*} Y \leftrightarrow \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X)$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ Y \in V \to Y \in V$
2		0wdom	$⊢ Y \in V \to \emptyset ≼^{*} Y$
3		breq1	$⊢ X = \emptyset \to (X ≼^{} Y \leftrightarrow \emptyset ≼^{} Y)$
4	2 3	syl5ibrcom	$⊢ Y \in V \to (X = \emptyset \to X ≼^{*} Y)$
5	4	imp	$⊢ (Y \in V \land X = \emptyset) \to X ≼^{*} Y$
6		0elpw	$⊢ \emptyset \in 𝒫 Y$
7		f1o0	$⊢ \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset$
8		f1ofo	$⊢ \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset \to \emptyset : \emptyset \underset{onto}{⟶} \emptyset$
9		0ex	$⊢ \emptyset \in V$
10		foeq1	$⊢ z = \emptyset \to (z : \emptyset \underset{onto}{⟶} \emptyset \leftrightarrow \emptyset : \emptyset \underset{onto}{⟶} \emptyset)$
11	9 10	spcev	$⊢ \emptyset : \emptyset \underset{onto}{⟶} \emptyset \to \exists z z : \emptyset \underset{onto}{⟶} \emptyset$
12	7 8 11	mp2b	$⊢ \exists z z : \emptyset \underset{onto}{⟶} \emptyset$
13		foeq2	$⊢ y = \emptyset \to (z : y \underset{onto}{⟶} \emptyset \leftrightarrow z : \emptyset \underset{onto}{⟶} \emptyset)$
14	13	exbidv	$⊢ y = \emptyset \to (\exists z z : y \underset{onto}{⟶} \emptyset \leftrightarrow \exists z z : \emptyset \underset{onto}{⟶} \emptyset)$
15	14	rspcev	$⊢ (\emptyset \in 𝒫 Y \land \exists z z : \emptyset \underset{onto}{⟶} \emptyset) \to \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} \emptyset$
16	6 12 15	mp2an	$⊢ \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} \emptyset$
17		foeq3	$⊢ X = \emptyset \to (z : y \underset{onto}{⟶} X \leftrightarrow z : y \underset{onto}{⟶} \emptyset)$
18	17	exbidv	$⊢ X = \emptyset \to (\exists z z : y \underset{onto}{⟶} X \leftrightarrow \exists z z : y \underset{onto}{⟶} \emptyset)$
19	18	rexbidv	$⊢ X = \emptyset \to (\exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X \leftrightarrow \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} \emptyset)$
20	16 19	mpbiri	$⊢ X = \emptyset \to \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X$
21	20	adantl	$⊢ (Y \in V \land X = \emptyset) \to \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X$
22	5 21	2thd	$⊢ (Y \in V \land X = \emptyset) \to (X ≼^{*} Y \leftrightarrow \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X)$
23		brwdomn0	$⊢ X \neq \emptyset \to (X ≼^{*} Y \leftrightarrow \exists x x : Y \underset{onto}{⟶} X)$
24	23	adantl	$⊢ (Y \in V \land X \neq \emptyset) \to (X ≼^{*} Y \leftrightarrow \exists x x : Y \underset{onto}{⟶} X)$
25		foeq1	$⊢ x = z \to (x : Y \underset{onto}{⟶} X \leftrightarrow z : Y \underset{onto}{⟶} X)$
26	25	cbvexvw	$⊢ \exists x x : Y \underset{onto}{⟶} X \leftrightarrow \exists z z : Y \underset{onto}{⟶} X$
27		pwidg	$⊢ Y \in V \to Y \in 𝒫 Y$
28	27	ad2antrr	$⊢ ((Y \in V \land X \neq \emptyset) \land \exists z z : Y \underset{onto}{⟶} X) \to Y \in 𝒫 Y$
29		foeq2	$⊢ y = Y \to (z : y \underset{onto}{⟶} X \leftrightarrow z : Y \underset{onto}{⟶} X)$
30	29	exbidv	$⊢ y = Y \to (\exists z z : y \underset{onto}{⟶} X \leftrightarrow \exists z z : Y \underset{onto}{⟶} X)$
31	30	rspcev	$⊢ (Y \in 𝒫 Y \land \exists z z : Y \underset{onto}{⟶} X) \to \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X$
32	28 31	sylancom	$⊢ ((Y \in V \land X \neq \emptyset) \land \exists z z : Y \underset{onto}{⟶} X) \to \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X$
33	32	ex	$⊢ (Y \in V \land X \neq \emptyset) \to (\exists z z : Y \underset{onto}{⟶} X \to \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X)$
34	26 33	syl5bi	$⊢ (Y \in V \land X \neq \emptyset) \to (\exists x x : Y \underset{onto}{⟶} X \to \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X)$
35		n0	$⊢ X \neq \emptyset \leftrightarrow \exists w w \in X$
36	35	biimpi	$⊢ X \neq \emptyset \to \exists w w \in X$
37	36	ad2antlr	$⊢ ((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \to \exists w w \in X$
38		vex	$⊢ z \in V$
39		difexg	$⊢ Y \in V \to Y ∖ y \in V$
40		snex	$⊢ \{w\} \in V$
41		xpexg	$⊢ (Y ∖ y \in V \land \{w\} \in V) \to (Y ∖ y) \times \{w\} \in V$
42	39 40 41	sylancl	$⊢ Y \in V \to (Y ∖ y) \times \{w\} \in V$
43		unexg	$⊢ (z \in V \land (Y ∖ y) \times \{w\} \in V) \to z \cup ((Y ∖ y) \times \{w\}) \in V$
44	38 42 43	sylancr	$⊢ Y \in V \to z \cup ((Y ∖ y) \times \{w\}) \in V$
45	44	adantr	$⊢ (Y \in V \land X \neq \emptyset) \to z \cup ((Y ∖ y) \times \{w\}) \in V$
46	45	ad2antrr	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to z \cup ((Y ∖ y) \times \{w\}) \in V$
47		fofn	$⊢ z : y \underset{onto}{⟶} X \to z Fn y$
48	47	adantl	$⊢ (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X) \to z Fn y$
49	48	ad2antlr	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to z Fn y$
50		vex	$⊢ w \in V$
51		fnconstg	$⊢ w \in V \to ((Y ∖ y) \times \{w\}) Fn (Y ∖ y)$
52	50 51	mp1i	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to ((Y ∖ y) \times \{w\}) Fn (Y ∖ y)$
53		disjdif	$⊢ y \cap (Y ∖ y) = \emptyset$
54	53	a1i	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to y \cap (Y ∖ y) = \emptyset$
55	49 52 54	fnund	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to (z \cup ((Y ∖ y) \times \{w\})) Fn (y \cup (Y ∖ y))$
56		elpwi	$⊢ y \in 𝒫 Y \to y \subseteq Y$
57		undif	$⊢ y \subseteq Y \leftrightarrow y \cup (Y ∖ y) = Y$
58	56 57	sylib	$⊢ y \in 𝒫 Y \to y \cup (Y ∖ y) = Y$
59	58	ad2antrl	$⊢ ((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \to y \cup (Y ∖ y) = Y$
60	59	adantr	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to y \cup (Y ∖ y) = Y$
61	60	fneq2d	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to ((z \cup ((Y ∖ y) \times \{w\})) Fn (y \cup (Y ∖ y)) \leftrightarrow (z \cup ((Y ∖ y) \times \{w\})) Fn Y)$
62	55 61	mpbid	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to (z \cup ((Y ∖ y) \times \{w\})) Fn Y$
63		rnun	$⊢ ran (z \cup ((Y ∖ y) \times \{w\})) = ran z \cup ran ((Y ∖ y) \times \{w\})$
64		forn	$⊢ z : y \underset{onto}{⟶} X \to ran z = X$
65	64	ad2antll	$⊢ ((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \to ran z = X$
66	65	adantr	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to ran z = X$
67	66	uneq1d	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to ran z \cup ran ((Y ∖ y) \times \{w\}) = X \cup ran ((Y ∖ y) \times \{w\})$
68		fconst6g	$⊢ w \in X \to ((Y ∖ y) \times \{w\}) : Y ∖ y ⟶ X$
69	68	frnd	$⊢ w \in X \to ran ((Y ∖ y) \times \{w\}) \subseteq X$
70	69	adantl	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to ran ((Y ∖ y) \times \{w\}) \subseteq X$
71		ssequn2	$⊢ ran ((Y ∖ y) \times \{w\}) \subseteq X \leftrightarrow X \cup ran ((Y ∖ y) \times \{w\}) = X$
72	70 71	sylib	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to X \cup ran ((Y ∖ y) \times \{w\}) = X$
73	67 72	eqtrd	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to ran z \cup ran ((Y ∖ y) \times \{w\}) = X$
74	63 73	syl5eq	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to ran (z \cup ((Y ∖ y) \times \{w\})) = X$
75		df-fo	$⊢ (z \cup ((Y ∖ y) \times \{w\})) : Y \underset{onto}{⟶} X \leftrightarrow ((z \cup ((Y ∖ y) \times \{w\})) Fn Y \land ran (z \cup ((Y ∖ y) \times \{w\})) = X)$
76	62 74 75	sylanbrc	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to (z \cup ((Y ∖ y) \times \{w\})) : Y \underset{onto}{⟶} X$
77		foeq1	$⊢ x = z \cup ((Y ∖ y) \times \{w\}) \to (x : Y \underset{onto}{⟶} X \leftrightarrow (z \cup ((Y ∖ y) \times \{w\})) : Y \underset{onto}{⟶} X)$
78	46 76 77	spcedv	$⊢ (((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \land w \in X) \to \exists x x : Y \underset{onto}{⟶} X$
79	37 78	exlimddv	$⊢ ((Y \in V \land X \neq \emptyset) \land (y \in 𝒫 Y \land z : y \underset{onto}{⟶} X)) \to \exists x x : Y \underset{onto}{⟶} X$
80	79	expr	$⊢ ((Y \in V \land X \neq \emptyset) \land y \in 𝒫 Y) \to (z : y \underset{onto}{⟶} X \to \exists x x : Y \underset{onto}{⟶} X)$
81	80	exlimdv	$⊢ ((Y \in V \land X \neq \emptyset) \land y \in 𝒫 Y) \to (\exists z z : y \underset{onto}{⟶} X \to \exists x x : Y \underset{onto}{⟶} X)$
82	81	rexlimdva	$⊢ (Y \in V \land X \neq \emptyset) \to (\exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X \to \exists x x : Y \underset{onto}{⟶} X)$
83	34 82	impbid	$⊢ (Y \in V \land X \neq \emptyset) \to (\exists x x : Y \underset{onto}{⟶} X \leftrightarrow \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X)$
84	24 83	bitrd	$⊢ (Y \in V \land X \neq \emptyset) \to (X ≼^{*} Y \leftrightarrow \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X)$
85	22 84	pm2.61dane	$⊢ Y \in V \to (X ≼^{*} Y \leftrightarrow \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X)$
86	1 85	syl	$⊢ Y \in V \to (X ≼^{*} Y \leftrightarrow \exists y \in 𝒫 Y \exists z z : y \underset{onto}{⟶} X)$

Metamath Proof Explorer

Theorem brwdom2

Proof