dirge

Description: For any two elements of a directed set, there exists a third element greater than or equal to both. Note that this does not say that the two elements have aleast upper bound. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

		Ref	Expression
	Hypothesis	dirge.1	$⊢ X = dom R$
	Assertion	dirge	$⊢ (R \in DirRel \land A \in X \land B \in X) \to \exists x \in X (A R x \land B R x)$

Proof

Step	Hyp	Ref	Expression
1		dirge.1	$⊢ X = dom R$
2		dirdm	$⊢ R \in DirRel \to dom R = ⋃ ⋃ R$
3	1 2	eqtrid	$⊢ R \in DirRel \to X = ⋃ ⋃ R$
4	3	eleq2d	$⊢ R \in DirRel \to (A \in X \leftrightarrow A \in ⋃ ⋃ R)$
5	3	eleq2d	$⊢ R \in DirRel \to (B \in X \leftrightarrow B \in ⋃ ⋃ R)$
6	4 5	anbi12d	$⊢ R \in DirRel \to ((A \in X \land B \in X) \leftrightarrow (A \in ⋃ ⋃ R \land B \in ⋃ ⋃ R))$
7		eqid	$⊢ ⋃ ⋃ R = ⋃ ⋃ R$
8	7	isdir	$⊢ R \in DirRel \to (R \in DirRel \leftrightarrow ((Rel R \land {I ↾}_{⋃ ⋃ R} \subseteq R) \land (R \circ R \subseteq R \land ⋃ ⋃ R \times ⋃ ⋃ R \subseteq R^{-1} \circ R)))$
9	8	ibi	$⊢ R \in DirRel \to ((Rel R \land {I ↾}_{⋃ ⋃ R} \subseteq R) \land (R \circ R \subseteq R \land ⋃ ⋃ R \times ⋃ ⋃ R \subseteq R^{-1} \circ R))$
10	9	simprrd	$⊢ R \in DirRel \to ⋃ ⋃ R \times ⋃ ⋃ R \subseteq R^{-1} \circ R$
11		codir	$⊢ ⋃ ⋃ R \times ⋃ ⋃ R \subseteq R^{-1} \circ R \leftrightarrow \forall y \in ⋃ ⋃ R \forall z \in ⋃ ⋃ R \exists x (y R x \land z R x)$
12	10 11	sylib	$⊢ R \in DirRel \to \forall y \in ⋃ ⋃ R \forall z \in ⋃ ⋃ R \exists x (y R x \land z R x)$
13		breq1	$⊢ y = A \to (y R x \leftrightarrow A R x)$
14	13	anbi1d	$⊢ y = A \to ((y R x \land z R x) \leftrightarrow (A R x \land z R x))$
15	14	exbidv	$⊢ y = A \to (\exists x (y R x \land z R x) \leftrightarrow \exists x (A R x \land z R x))$
16		breq1	$⊢ z = B \to (z R x \leftrightarrow B R x)$
17	16	anbi2d	$⊢ z = B \to ((A R x \land z R x) \leftrightarrow (A R x \land B R x))$
18	17	exbidv	$⊢ z = B \to (\exists x (A R x \land z R x) \leftrightarrow \exists x (A R x \land B R x))$
19	15 18	rspc2v	$⊢ (A \in ⋃ ⋃ R \land B \in ⋃ ⋃ R) \to (\forall y \in ⋃ ⋃ R \forall z \in ⋃ ⋃ R \exists x (y R x \land z R x) \to \exists x (A R x \land B R x))$
20	12 19	syl5com	$⊢ R \in DirRel \to ((A \in ⋃ ⋃ R \land B \in ⋃ ⋃ R) \to \exists x (A R x \land B R x))$
21	6 20	sylbid	$⊢ R \in DirRel \to ((A \in X \land B \in X) \to \exists x (A R x \land B R x))$
22		reldir	$⊢ R \in DirRel \to Rel R$
23		relelrn	$⊢ (Rel R \land A R x) \to x \in ran R$
24	22 23	sylan	$⊢ (R \in DirRel \land A R x) \to x \in ran R$
25	24	ex	$⊢ R \in DirRel \to (A R x \to x \in ran R)$
26		ssun2	$⊢ ran R \subseteq dom R \cup ran R$
27		dmrnssfld	$⊢ dom R \cup ran R \subseteq ⋃ ⋃ R$
28	26 27	sstri	$⊢ ran R \subseteq ⋃ ⋃ R$
29	28 3	sseqtrrid	$⊢ R \in DirRel \to ran R \subseteq X$
30	29	sseld	$⊢ R \in DirRel \to (x \in ran R \to x \in X)$
31	25 30	syld	$⊢ R \in DirRel \to (A R x \to x \in X)$
32	31	adantrd	$⊢ R \in DirRel \to ((A R x \land B R x) \to x \in X)$
33	32	ancrd	$⊢ R \in DirRel \to ((A R x \land B R x) \to (x \in X \land (A R x \land B R x)))$
34	33	eximdv	$⊢ R \in DirRel \to (\exists x (A R x \land B R x) \to \exists x (x \in X \land (A R x \land B R x)))$
35		df-rex	$⊢ \exists x \in X (A R x \land B R x) \leftrightarrow \exists x (x \in X \land (A R x \land B R x))$
36	34 35	imbitrrdi	$⊢ R \in DirRel \to (\exists x (A R x \land B R x) \to \exists x \in X (A R x \land B R x))$
37	21 36	syld	$⊢ R \in DirRel \to ((A \in X \land B \in X) \to \exists x \in X (A R x \land B R x))$
38	37	3impib	$⊢ (R \in DirRel \land A \in X \land B \in X) \to \exists x \in X (A R x \land B R x)$

Metamath Proof Explorer

Theorem dirge

Proof