wdomtr

Description: Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

		Ref	Expression
	Assertion	wdomtr	$⊢ (X ≼^{} Y \land Y ≼^{} Z) \to X ≼^{*} Z$

Proof

Step	Hyp	Ref	Expression
1		relwdom	$⊢ Rel ≼^{*}$
2	1	brrelex2i	$⊢ Y ≼^{*} Z \to Z \in V$
3	2	adantl	$⊢ (X ≼^{} Y \land Y ≼^{} Z) \to Z \in V$
4		0wdom	$⊢ Z \in V \to \emptyset ≼^{*} Z$
5		breq1	$⊢ X = \emptyset \to (X ≼^{} Z \leftrightarrow \emptyset ≼^{} Z)$
6	4 5	syl5ibrcom	$⊢ Z \in V \to (X = \emptyset \to X ≼^{*} Z)$
7	3 6	syl	$⊢ (X ≼^{} Y \land Y ≼^{} Z) \to (X = \emptyset \to X ≼^{*} Z)$
8		simpll	$⊢ ((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \to X ≼^{*} Y$
9		brwdomn0	$⊢ X \neq \emptyset \to (X ≼^{*} Y \leftrightarrow \exists z z : Y \underset{onto}{⟶} X)$
10	9	adantl	$⊢ ((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \to (X ≼^{*} Y \leftrightarrow \exists z z : Y \underset{onto}{⟶} X)$
11	8 10	mpbid	$⊢ ((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \to \exists z z : Y \underset{onto}{⟶} X$
12		simpllr	$⊢ (((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \land z : Y \underset{onto}{⟶} X) \to Y ≼^{*} Z$
13		simplr	$⊢ (((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \land z : Y \underset{onto}{⟶} X) \to X \neq \emptyset$
14		dm0rn0	$⊢ dom z = \emptyset \leftrightarrow ran z = \emptyset$
15	14	necon3bii	$⊢ dom z \neq \emptyset \leftrightarrow ran z \neq \emptyset$
16	15	a1i	$⊢ z : Y \underset{onto}{⟶} X \to (dom z \neq \emptyset \leftrightarrow ran z \neq \emptyset)$
17		fof	$⊢ z : Y \underset{onto}{⟶} X \to z : Y ⟶ X$
18	17	fdmd	$⊢ z : Y \underset{onto}{⟶} X \to dom z = Y$
19	18	neeq1d	$⊢ z : Y \underset{onto}{⟶} X \to (dom z \neq \emptyset \leftrightarrow Y \neq \emptyset)$
20		forn	$⊢ z : Y \underset{onto}{⟶} X \to ran z = X$
21	20	neeq1d	$⊢ z : Y \underset{onto}{⟶} X \to (ran z \neq \emptyset \leftrightarrow X \neq \emptyset)$
22	16 19 21	3bitr3rd	$⊢ z : Y \underset{onto}{⟶} X \to (X \neq \emptyset \leftrightarrow Y \neq \emptyset)$
23	22	adantl	$⊢ (((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \land z : Y \underset{onto}{⟶} X) \to (X \neq \emptyset \leftrightarrow Y \neq \emptyset)$
24	13 23	mpbid	$⊢ (((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \land z : Y \underset{onto}{⟶} X) \to Y \neq \emptyset$
25		brwdomn0	$⊢ Y \neq \emptyset \to (Y ≼^{*} Z \leftrightarrow \exists y y : Z \underset{onto}{⟶} Y)$
26	24 25	syl	$⊢ (((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \land z : Y \underset{onto}{⟶} X) \to (Y ≼^{*} Z \leftrightarrow \exists y y : Z \underset{onto}{⟶} Y)$
27	12 26	mpbid	$⊢ (((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \land z : Y \underset{onto}{⟶} X) \to \exists y y : Z \underset{onto}{⟶} Y$
28		vex	$⊢ z \in V$
29		vex	$⊢ y \in V$
30	28 29	coex	$⊢ z \circ y \in V$
31		foco	$⊢ (z : Y \underset{onto}{⟶} X \land y : Z \underset{onto}{⟶} Y) \to (z \circ y) : Z \underset{onto}{⟶} X$
32		fowdom	$⊢ (z \circ y \in V \land (z \circ y) : Z \underset{onto}{⟶} X) \to X ≼^{*} Z$
33	30 31 32	sylancr	$⊢ (z : Y \underset{onto}{⟶} X \land y : Z \underset{onto}{⟶} Y) \to X ≼^{*} Z$
34	33	adantl	$⊢ (((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \land (z : Y \underset{onto}{⟶} X \land y : Z \underset{onto}{⟶} Y)) \to X ≼^{*} Z$
35	34	expr	$⊢ (((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \land z : Y \underset{onto}{⟶} X) \to (y : Z \underset{onto}{⟶} Y \to X ≼^{*} Z)$
36	35	exlimdv	$⊢ (((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \land z : Y \underset{onto}{⟶} X) \to (\exists y y : Z \underset{onto}{⟶} Y \to X ≼^{*} Z)$
37	27 36	mpd	$⊢ (((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \land z : Y \underset{onto}{⟶} X) \to X ≼^{*} Z$
38	11 37	exlimddv	$⊢ ((X ≼^{} Y \land Y ≼^{} Z) \land X \neq \emptyset) \to X ≼^{*} Z$
39	38	ex	$⊢ (X ≼^{} Y \land Y ≼^{} Z) \to (X \neq \emptyset \to X ≼^{*} Z)$
40	7 39	pm2.61dne	$⊢ (X ≼^{} Y \land Y ≼^{} Z) \to X ≼^{*} Z$

Metamath Proof Explorer

Theorem wdomtr

Proof