ordtbaslem

Description: Lemma for ordtbas . In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypotheses	ordtval.1	$⊢ X = dom R$
	ordtval.2	$⊢ A = ran (x \in X ⟼ \{y \in X \| \neg y R x\})$
Assertion	ordtbaslem	$⊢ R \in TosetRel \to fi (A) = A$

Proof

Step	Hyp	Ref	Expression
1		ordtval.1	$⊢ X = dom R$
2		ordtval.2	$⊢ A = ran (x \in X ⟼ \{y \in X \| \neg y R x\})$
3		3anrot	$⊢ (y \in X \land a \in X \land b \in X) \leftrightarrow (a \in X \land b \in X \land y \in X)$
4	1	tsrlemax	$⊢ (R \in TosetRel \land (y \in X \land a \in X \land b \in X)) \to (y R if (a R b, b, a) \leftrightarrow (y R a \lor y R b))$
5	3 4	sylan2br	$⊢ (R \in TosetRel \land (a \in X \land b \in X \land y \in X)) \to (y R if (a R b, b, a) \leftrightarrow (y R a \lor y R b))$
6	5	3exp2	$⊢ R \in TosetRel \to (a \in X \to (b \in X \to (y \in X \to (y R if (a R b, b, a) \leftrightarrow (y R a \lor y R b)))))$
7	6	imp42	$⊢ ((R \in TosetRel \land (a \in X \land b \in X)) \land y \in X) \to (y R if (a R b, b, a) \leftrightarrow (y R a \lor y R b))$
8	7	notbid	$⊢ ((R \in TosetRel \land (a \in X \land b \in X)) \land y \in X) \to (\neg y R if (a R b, b, a) \leftrightarrow \neg (y R a \lor y R b))$
9		ioran	$⊢ \neg (y R a \lor y R b) \leftrightarrow (\neg y R a \land \neg y R b)$
10	8 9	bitrdi	$⊢ ((R \in TosetRel \land (a \in X \land b \in X)) \land y \in X) \to (\neg y R if (a R b, b, a) \leftrightarrow (\neg y R a \land \neg y R b))$
11	10	rabbidva	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg y R if (a R b, b, a)\} = \{y \in X \| (\neg y R a \land \neg y R b)\}$
12		ifcl	$⊢ (b \in X \land a \in X) \to if (a R b, b, a) \in X$
13	12	ancoms	$⊢ (a \in X \land b \in X) \to if (a R b, b, a) \in X$
14		dmexg	$⊢ R \in TosetRel \to dom R \in V$
15	1 14	eqeltrid	$⊢ R \in TosetRel \to X \in V$
16	15	adantr	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to X \in V$
17		rabexg	$⊢ X \in V \to \{y \in X \| (\neg y R a \land \neg y R b)\} \in V$
18	16 17	syl	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| (\neg y R a \land \neg y R b)\} \in V$
19	11 18	eqeltrd	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg y R if (a R b, b, a)\} \in V$
20		eqid	$⊢ (x \in X ⟼ \{y \in X \| \neg y R x\}) = (x \in X ⟼ \{y \in X \| \neg y R x\})$
21		breq2	$⊢ x = if (a R b, b, a) \to (y R x \leftrightarrow y R if (a R b, b, a))$
22	21	notbid	$⊢ x = if (a R b, b, a) \to (\neg y R x \leftrightarrow \neg y R if (a R b, b, a))$
23	22	rabbidv	$⊢ x = if (a R b, b, a) \to \{y \in X \| \neg y R x\} = \{y \in X \| \neg y R if (a R b, b, a)\}$
24	20 23	elrnmpt1s	$⊢ (if (a R b, b, a) \in X \land \{y \in X \| \neg y R if (a R b, b, a)\} \in V) \to \{y \in X \| \neg y R if (a R b, b, a)\} \in ran (x \in X ⟼ \{y \in X \| \neg y R x\})$
25	24 2	eleqtrrdi	$⊢ (if (a R b, b, a) \in X \land \{y \in X \| \neg y R if (a R b, b, a)\} \in V) \to \{y \in X \| \neg y R if (a R b, b, a)\} \in A$
26	13 19 25	syl2an2	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| \neg y R if (a R b, b, a)\} \in A$
27	11 26	eqeltrrd	$⊢ (R \in TosetRel \land (a \in X \land b \in X)) \to \{y \in X \| (\neg y R a \land \neg y R b)\} \in A$
28	27	ralrimivva	$⊢ R \in TosetRel \to \forall a \in X \forall b \in X \{y \in X \| (\neg y R a \land \neg y R b)\} \in A$
29		rabexg	$⊢ X \in V \to \{y \in X \| \neg y R a\} \in V$
30	15 29	syl	$⊢ R \in TosetRel \to \{y \in X \| \neg y R a\} \in V$
31	30	ralrimivw	$⊢ R \in TosetRel \to \forall a \in X \{y \in X \| \neg y R a\} \in V$
32		breq2	$⊢ x = a \to (y R x \leftrightarrow y R a)$
33	32	notbid	$⊢ x = a \to (\neg y R x \leftrightarrow \neg y R a)$
34	33	rabbidv	$⊢ x = a \to \{y \in X \| \neg y R x\} = \{y \in X \| \neg y R a\}$
35	34	cbvmptv	$⊢ (x \in X ⟼ \{y \in X \| \neg y R x\}) = (a \in X ⟼ \{y \in X \| \neg y R a\})$
36		ineq1	$⊢ z = \{y \in X \| \neg y R a\} \to z \cap \{y \in X \| \neg y R b\} = \{y \in X \| \neg y R a\} \cap \{y \in X \| \neg y R b\}$
37		inrab	$⊢ \{y \in X \| \neg y R a\} \cap \{y \in X \| \neg y R b\} = \{y \in X \| (\neg y R a \land \neg y R b)\}$
38	36 37	eqtrdi	$⊢ z = \{y \in X \| \neg y R a\} \to z \cap \{y \in X \| \neg y R b\} = \{y \in X \| (\neg y R a \land \neg y R b)\}$
39	38	eleq1d	$⊢ z = \{y \in X \| \neg y R a\} \to (z \cap \{y \in X \| \neg y R b\} \in A \leftrightarrow \{y \in X \| (\neg y R a \land \neg y R b)\} \in A)$
40	39	ralbidv	$⊢ z = \{y \in X \| \neg y R a\} \to (\forall b \in X z \cap \{y \in X \| \neg y R b\} \in A \leftrightarrow \forall b \in X \{y \in X \| (\neg y R a \land \neg y R b)\} \in A)$
41	35 40	ralrnmptw	$⊢ \forall a \in X \{y \in X \| \neg y R a\} \in V \to (\forall z \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \forall b \in X z \cap \{y \in X \| \neg y R b\} \in A \leftrightarrow \forall a \in X \forall b \in X \{y \in X \| (\neg y R a \land \neg y R b)\} \in A)$
42	31 41	syl	$⊢ R \in TosetRel \to (\forall z \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \forall b \in X z \cap \{y \in X \| \neg y R b\} \in A \leftrightarrow \forall a \in X \forall b \in X \{y \in X \| (\neg y R a \land \neg y R b)\} \in A)$
43	28 42	mpbird	$⊢ R \in TosetRel \to \forall z \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \forall b \in X z \cap \{y \in X \| \neg y R b\} \in A$
44		rabexg	$⊢ X \in V \to \{y \in X \| \neg y R b\} \in V$
45	15 44	syl	$⊢ R \in TosetRel \to \{y \in X \| \neg y R b\} \in V$
46	45	ralrimivw	$⊢ R \in TosetRel \to \forall b \in X \{y \in X \| \neg y R b\} \in V$
47		breq2	$⊢ x = b \to (y R x \leftrightarrow y R b)$
48	47	notbid	$⊢ x = b \to (\neg y R x \leftrightarrow \neg y R b)$
49	48	rabbidv	$⊢ x = b \to \{y \in X \| \neg y R x\} = \{y \in X \| \neg y R b\}$
50	49	cbvmptv	$⊢ (x \in X ⟼ \{y \in X \| \neg y R x\}) = (b \in X ⟼ \{y \in X \| \neg y R b\})$
51		ineq2	$⊢ w = \{y \in X \| \neg y R b\} \to z \cap w = z \cap \{y \in X \| \neg y R b\}$
52	51	eleq1d	$⊢ w = \{y \in X \| \neg y R b\} \to (z \cap w \in A \leftrightarrow z \cap \{y \in X \| \neg y R b\} \in A)$
53	50 52	ralrnmptw	$⊢ \forall b \in X \{y \in X \| \neg y R b\} \in V \to (\forall w \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) z \cap w \in A \leftrightarrow \forall b \in X z \cap \{y \in X \| \neg y R b\} \in A)$
54	46 53	syl	$⊢ R \in TosetRel \to (\forall w \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) z \cap w \in A \leftrightarrow \forall b \in X z \cap \{y \in X \| \neg y R b\} \in A)$
55	54	ralbidv	$⊢ R \in TosetRel \to (\forall z \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \forall w \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) z \cap w \in A \leftrightarrow \forall z \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \forall b \in X z \cap \{y \in X \| \neg y R b\} \in A)$
56	43 55	mpbird	$⊢ R \in TosetRel \to \forall z \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \forall w \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) z \cap w \in A$
57	2	raleqi	$⊢ \forall w \in A z \cap w \in A \leftrightarrow \forall w \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) z \cap w \in A$
58	2 57	raleqbii	$⊢ \forall z \in A \forall w \in A z \cap w \in A \leftrightarrow \forall z \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \forall w \in ran (x \in X ⟼ \{y \in X \| \neg y R x\}) z \cap w \in A$
59	56 58	sylibr	$⊢ R \in TosetRel \to \forall z \in A \forall w \in A z \cap w \in A$
60	15	pwexd	$⊢ R \in TosetRel \to 𝒫 X \in V$
61		ssrab2	$⊢ \{y \in X \| \neg y R x\} \subseteq X$
62	15	adantr	$⊢ (R \in TosetRel \land x \in X) \to X \in V$
63		elpw2g	$⊢ X \in V \to (\{y \in X \| \neg y R x\} \in 𝒫 X \leftrightarrow \{y \in X \| \neg y R x\} \subseteq X)$
64	62 63	syl	$⊢ (R \in TosetRel \land x \in X) \to (\{y \in X \| \neg y R x\} \in 𝒫 X \leftrightarrow \{y \in X \| \neg y R x\} \subseteq X)$
65	61 64	mpbiri	$⊢ (R \in TosetRel \land x \in X) \to \{y \in X \| \neg y R x\} \in 𝒫 X$
66	65	fmpttd	$⊢ R \in TosetRel \to (x \in X ⟼ \{y \in X \| \neg y R x\}) : X ⟶ 𝒫 X$
67	66	frnd	$⊢ R \in TosetRel \to ran (x \in X ⟼ \{y \in X \| \neg y R x\}) \subseteq 𝒫 X$
68	2 67	eqsstrid	$⊢ R \in TosetRel \to A \subseteq 𝒫 X$
69	60 68	ssexd	$⊢ R \in TosetRel \to A \in V$
70		inficl	$⊢ A \in V \to (\forall z \in A \forall w \in A z \cap w \in A \leftrightarrow fi (A) = A)$
71	69 70	syl	$⊢ R \in TosetRel \to (\forall z \in A \forall w \in A z \cap w \in A \leftrightarrow fi (A) = A)$
72	59 71	mpbid	$⊢ R \in TosetRel \to fi (A) = A$

Metamath Proof Explorer

Theorem ordtbaslem

Proof