ordthauslem

		Ref	Expression
	Hypothesis	ordthauslem.1	$⊢ X = dom R$
	Assertion	ordthauslem	$⊢ (R \in TosetRel \land A \in X \land B \in X) \to (A R B \to (A \neq B \to \exists m \in ordTop (R) \exists n \in ordTop (R) (A \in m \land B \in n \land m \cap n = \emptyset)))$

Proof

Step	Hyp	Ref	Expression
1		ordthauslem.1	$⊢ X = dom R$
2		simpll1	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset) \to R \in TosetRel$
3		simpll3	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset) \to B \in X$
4	1	ordtopn2	$⊢ (R \in TosetRel \land B \in X) \to \{x \in X \| \neg B R x\} \in ordTop (R)$
5	2 3 4	syl2anc	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset) \to \{x \in X \| \neg B R x\} \in ordTop (R)$
6		simpll2	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset) \to A \in X$
7	1	ordtopn1	$⊢ (R \in TosetRel \land A \in X) \to \{x \in X \| \neg x R A\} \in ordTop (R)$
8	2 6 7	syl2anc	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset) \to \{x \in X \| \neg x R A\} \in ordTop (R)$
9		breq2	$⊢ x = A \to (B R x \leftrightarrow B R A)$
10	9	notbid	$⊢ x = A \to (\neg B R x \leftrightarrow \neg B R A)$
11		simprr	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to A \neq B$
12		simpl1	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to R \in TosetRel$
13		tsrps	$⊢ R \in TosetRel \to R \in PosetRel$
14	12 13	syl	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to R \in PosetRel$
15		simprl	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to A R B$
16		psasym	$⊢ (R \in PosetRel \land A R B \land B R A) \to A = B$
17	16	3expia	$⊢ (R \in PosetRel \land A R B) \to (B R A \to A = B)$
18	14 15 17	syl2anc	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to (B R A \to A = B)$
19	18	necon3ad	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to (A \neq B \to \neg B R A)$
20	11 19	mpd	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to \neg B R A$
21	20	adantr	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset) \to \neg B R A$
22	10 6 21	elrabd	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset) \to A \in \{x \in X \| \neg B R x\}$
23		breq1	$⊢ x = B \to (x R A \leftrightarrow B R A)$
24	23	notbid	$⊢ x = B \to (\neg x R A \leftrightarrow \neg B R A)$
25	24 3 21	elrabd	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset) \to B \in \{x \in X \| \neg x R A\}$
26		simpr	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset) \to \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset$
27		eleq2	$⊢ m = \{x \in X \| \neg B R x\} \to (A \in m \leftrightarrow A \in \{x \in X \| \neg B R x\})$
28		ineq1	$⊢ m = \{x \in X \| \neg B R x\} \to m \cap n = \{x \in X \| \neg B R x\} \cap n$
29	28	eqeq1d	$⊢ m = \{x \in X \| \neg B R x\} \to (m \cap n = \emptyset \leftrightarrow \{x \in X \| \neg B R x\} \cap n = \emptyset)$
30	27 29	3anbi13d	$⊢ m = \{x \in X \| \neg B R x\} \to ((A \in m \land B \in n \land m \cap n = \emptyset) \leftrightarrow (A \in \{x \in X \| \neg B R x\} \land B \in n \land \{x \in X \| \neg B R x\} \cap n = \emptyset))$
31		eleq2	$⊢ n = \{x \in X \| \neg x R A\} \to (B \in n \leftrightarrow B \in \{x \in X \| \neg x R A\})$
32		ineq2	$⊢ n = \{x \in X \| \neg x R A\} \to \{x \in X \| \neg B R x\} \cap n = \{x \in X \| \neg B R x\} \cap \{x \in X \| \neg x R A\}$
33		inrab	$⊢ \{x \in X \| \neg B R x\} \cap \{x \in X \| \neg x R A\} = \{x \in X \| (\neg B R x \land \neg x R A)\}$
34	32 33	eqtrdi	$⊢ n = \{x \in X \| \neg x R A\} \to \{x \in X \| \neg B R x\} \cap n = \{x \in X \| (\neg B R x \land \neg x R A)\}$
35	34	eqeq1d	$⊢ n = \{x \in X \| \neg x R A\} \to (\{x \in X \| \neg B R x\} \cap n = \emptyset \leftrightarrow \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset)$
36	31 35	3anbi23d	$⊢ n = \{x \in X \| \neg x R A\} \to ((A \in \{x \in X \| \neg B R x\} \land B \in n \land \{x \in X \| \neg B R x\} \cap n = \emptyset) \leftrightarrow (A \in \{x \in X \| \neg B R x\} \land B \in \{x \in X \| \neg x R A\} \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset))$
37	30 36	rspc2ev	$⊢ (\{x \in X \| \neg B R x\} \in ordTop (R) \land \{x \in X \| \neg x R A\} \in ordTop (R) \land (A \in \{x \in X \| \neg B R x\} \land B \in \{x \in X \| \neg x R A\} \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset)) \to \exists m \in ordTop (R) \exists n \in ordTop (R) (A \in m \land B \in n \land m \cap n = \emptyset)$
38	5 8 22 25 26 37	syl113anc	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land \{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset) \to \exists m \in ordTop (R) \exists n \in ordTop (R) (A \in m \land B \in n \land m \cap n = \emptyset)$
39	38	ex	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to (\{x \in X \| (\neg B R x \land \neg x R A)\} = \emptyset \to \exists m \in ordTop (R) \exists n \in ordTop (R) (A \in m \land B \in n \land m \cap n = \emptyset))$
40		rabn0	$⊢ \{x \in X \| (\neg B R x \land \neg x R A)\} \neq \emptyset \leftrightarrow \exists x \in X (\neg B R x \land \neg x R A)$
41		simpll1	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to R \in TosetRel$
42		simprl	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to x \in X$
43	1	ordtopn2	$⊢ (R \in TosetRel \land x \in X) \to \{y \in X \| \neg x R y\} \in ordTop (R)$
44	41 42 43	syl2anc	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to \{y \in X \| \neg x R y\} \in ordTop (R)$
45	1	ordtopn1	$⊢ (R \in TosetRel \land x \in X) \to \{y \in X \| \neg y R x\} \in ordTop (R)$
46	41 42 45	syl2anc	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to \{y \in X \| \neg y R x\} \in ordTop (R)$
47		breq2	$⊢ y = A \to (x R y \leftrightarrow x R A)$
48	47	notbid	$⊢ y = A \to (\neg x R y \leftrightarrow \neg x R A)$
49		simpll2	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to A \in X$
50		simprrr	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to \neg x R A$
51	48 49 50	elrabd	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to A \in \{y \in X \| \neg x R y\}$
52		breq1	$⊢ y = B \to (y R x \leftrightarrow B R x)$
53	52	notbid	$⊢ y = B \to (\neg y R x \leftrightarrow \neg B R x)$
54		simpll3	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to B \in X$
55		simprrl	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to \neg B R x$
56	53 54 55	elrabd	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to B \in \{y \in X \| \neg y R x\}$
57	41 42	jca	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to (R \in TosetRel \land x \in X)$
58	1	tsrlin	$⊢ (R \in TosetRel \land x \in X \land y \in X) \to (x R y \lor y R x)$
59	58	3expa	$⊢ ((R \in TosetRel \land x \in X) \land y \in X) \to (x R y \lor y R x)$
60	57 59	sylan	$⊢ ((((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \land y \in X) \to (x R y \lor y R x)$
61		oran	$⊢ (x R y \lor y R x) \leftrightarrow \neg (\neg x R y \land \neg y R x)$
62	60 61	sylib	$⊢ ((((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \land y \in X) \to \neg (\neg x R y \land \neg y R x)$
63	62	ralrimiva	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to \forall y \in X \neg (\neg x R y \land \neg y R x)$
64		rabeq0	$⊢ \{y \in X \| (\neg x R y \land \neg y R x)\} = \emptyset \leftrightarrow \forall y \in X \neg (\neg x R y \land \neg y R x)$
65	63 64	sylibr	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to \{y \in X \| (\neg x R y \land \neg y R x)\} = \emptyset$
66		eleq2	$⊢ m = \{y \in X \| \neg x R y\} \to (A \in m \leftrightarrow A \in \{y \in X \| \neg x R y\})$
67		ineq1	$⊢ m = \{y \in X \| \neg x R y\} \to m \cap n = \{y \in X \| \neg x R y\} \cap n$
68	67	eqeq1d	$⊢ m = \{y \in X \| \neg x R y\} \to (m \cap n = \emptyset \leftrightarrow \{y \in X \| \neg x R y\} \cap n = \emptyset)$
69	66 68	3anbi13d	$⊢ m = \{y \in X \| \neg x R y\} \to ((A \in m \land B \in n \land m \cap n = \emptyset) \leftrightarrow (A \in \{y \in X \| \neg x R y\} \land B \in n \land \{y \in X \| \neg x R y\} \cap n = \emptyset))$
70		eleq2	$⊢ n = \{y \in X \| \neg y R x\} \to (B \in n \leftrightarrow B \in \{y \in X \| \neg y R x\})$
71		ineq2	$⊢ n = \{y \in X \| \neg y R x\} \to \{y \in X \| \neg x R y\} \cap n = \{y \in X \| \neg x R y\} \cap \{y \in X \| \neg y R x\}$
72		inrab	$⊢ \{y \in X \| \neg x R y\} \cap \{y \in X \| \neg y R x\} = \{y \in X \| (\neg x R y \land \neg y R x)\}$
73	71 72	eqtrdi	$⊢ n = \{y \in X \| \neg y R x\} \to \{y \in X \| \neg x R y\} \cap n = \{y \in X \| (\neg x R y \land \neg y R x)\}$
74	73	eqeq1d	$⊢ n = \{y \in X \| \neg y R x\} \to (\{y \in X \| \neg x R y\} \cap n = \emptyset \leftrightarrow \{y \in X \| (\neg x R y \land \neg y R x)\} = \emptyset)$
75	70 74	3anbi23d	$⊢ n = \{y \in X \| \neg y R x\} \to ((A \in \{y \in X \| \neg x R y\} \land B \in n \land \{y \in X \| \neg x R y\} \cap n = \emptyset) \leftrightarrow (A \in \{y \in X \| \neg x R y\} \land B \in \{y \in X \| \neg y R x\} \land \{y \in X \| (\neg x R y \land \neg y R x)\} = \emptyset))$
76	69 75	rspc2ev	$⊢ (\{y \in X \| \neg x R y\} \in ordTop (R) \land \{y \in X \| \neg y R x\} \in ordTop (R) \land (A \in \{y \in X \| \neg x R y\} \land B \in \{y \in X \| \neg y R x\} \land \{y \in X \| (\neg x R y \land \neg y R x)\} = \emptyset)) \to \exists m \in ordTop (R) \exists n \in ordTop (R) (A \in m \land B \in n \land m \cap n = \emptyset)$
77	44 46 51 56 65 76	syl113anc	$⊢ (((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \land (x \in X \land (\neg B R x \land \neg x R A))) \to \exists m \in ordTop (R) \exists n \in ordTop (R) (A \in m \land B \in n \land m \cap n = \emptyset)$
78	77	rexlimdvaa	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to (\exists x \in X (\neg B R x \land \neg x R A) \to \exists m \in ordTop (R) \exists n \in ordTop (R) (A \in m \land B \in n \land m \cap n = \emptyset))$
79	40 78	biimtrid	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to (\{x \in X \| (\neg B R x \land \neg x R A)\} \neq \emptyset \to \exists m \in ordTop (R) \exists n \in ordTop (R) (A \in m \land B \in n \land m \cap n = \emptyset))$
80	39 79	pm2.61dne	$⊢ ((R \in TosetRel \land A \in X \land B \in X) \land (A R B \land A \neq B)) \to \exists m \in ordTop (R) \exists n \in ordTop (R) (A \in m \land B \in n \land m \cap n = \emptyset)$
81	80	exp32	$⊢ (R \in TosetRel \land A \in X \land B \in X) \to (A R B \to (A \neq B \to \exists m \in ordTop (R) \exists n \in ordTop (R) (A \in m \land B \in n \land m \cap n = \emptyset)))$

Metamath Proof Explorer

Theorem ordthauslem

Proof