Metamath Proof Explorer

Theorem ordtbas

Description: In a total order, the finite intersections of the open rays generates the set of open intervals, but no more - these four collections form a subbasis for the order topology. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ordtval.1 ⊢ X = dom ⁡ R
ordtval.2 ⊢ A = ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x
ordtval.3 ⊢ B = ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
ordtval.4 ⊢ C = ran ⁡ a ∈ X , b ∈ X ⟼ y ∈ X | ¬ y R a ∧ ¬ b R y
Assertion ordtbas ⊢ R ∈ TosetRel → fi ⁡ X ∪ A ∪ B = X ∪ A ∪ B ∪ C

Proof

Step Hyp Ref Expression
1 ordtval.1 ⊢ X = dom ⁡ R
2 ordtval.2 ⊢ A = ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x
3 ordtval.3 ⊢ B = ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
4 ordtval.4 ⊢ C = ran ⁡ a ∈ X , b ∈ X ⟼ y ∈ X | ¬ y R a ∧ ¬ b R y
5 snex ⊢ X ∈ V
6 ssun2 ⊢ A ∪ B ⊆ X ∪ A ∪ B
7 1 2 3 ordtuni ⊢ R ∈ TosetRel → X = ⋃ X ∪ A ∪ B
8 dmexg ⊢ R ∈ TosetRel → dom ⁡ R ∈ V
9 1 8 eqeltrid ⊢ R ∈ TosetRel → X ∈ V
10 7 9 eqeltrrd ⊢ R ∈ TosetRel → ⋃ X ∪ A ∪ B ∈ V
11 uniexb ⊢ X ∪ A ∪ B ∈ V ↔ ⋃ X ∪ A ∪ B ∈ V
12 10 11 sylibr ⊢ R ∈ TosetRel → X ∪ A ∪ B ∈ V
13 ssexg ⊢ A ∪ B ⊆ X ∪ A ∪ B ∧ X ∪ A ∪ B ∈ V → A ∪ B ∈ V
14 6 12 13 sylancr ⊢ R ∈ TosetRel → A ∪ B ∈ V
15 elfiun ⊢ X ∈ V ∧ A ∪ B ∈ V → z ∈ fi ⁡ X ∪ A ∪ B ↔ z ∈ fi ⁡ X ∨ z ∈ fi ⁡ A ∪ B ∨ ∃ m ∈ fi ⁡ X ∃ n ∈ fi ⁡ A ∪ B z = m ∩ n
16 5 14 15 sylancr ⊢ R ∈ TosetRel → z ∈ fi ⁡ X ∪ A ∪ B ↔ z ∈ fi ⁡ X ∨ z ∈ fi ⁡ A ∪ B ∨ ∃ m ∈ fi ⁡ X ∃ n ∈ fi ⁡ A ∪ B z = m ∩ n
17 fisn ⊢ fi ⁡ X = X
18 ssun1 ⊢ X ⊆ X ∪ A ∪ B ∪ C
19 17 18 eqsstri ⊢ fi ⁡ X ⊆ X ∪ A ∪ B ∪ C
20 19 sseli ⊢ z ∈ fi ⁡ X → z ∈ X ∪ A ∪ B ∪ C
21 20 a1i ⊢ R ∈ TosetRel → z ∈ fi ⁡ X → z ∈ X ∪ A ∪ B ∪ C
22 1 2 3 4 ordtbas2 ⊢ R ∈ TosetRel → fi ⁡ A ∪ B = A ∪ B ∪ C
23 ssun2 ⊢ A ∪ B ∪ C ⊆ X ∪ A ∪ B ∪ C
24 22 23 eqsstrdi ⊢ R ∈ TosetRel → fi ⁡ A ∪ B ⊆ X ∪ A ∪ B ∪ C
25 24 sseld ⊢ R ∈ TosetRel → z ∈ fi ⁡ A ∪ B → z ∈ X ∪ A ∪ B ∪ C
26 fipwuni ⊢ fi ⁡ A ∪ B ⊆ 𝒫 ⋃ A ∪ B
27 26 sseli ⊢ n ∈ fi ⁡ A ∪ B → n ∈ 𝒫 ⋃ A ∪ B
28 27 elpwid ⊢ n ∈ fi ⁡ A ∪ B → n ⊆ ⋃ A ∪ B
29 28 ad2antll ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → n ⊆ ⋃ A ∪ B
30 6 unissi ⊢ ⋃ A ∪ B ⊆ ⋃ X ∪ A ∪ B
31 30 7 sseqtrrid ⊢ R ∈ TosetRel → ⋃ A ∪ B ⊆ X
32 31 adantr ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → ⋃ A ∪ B ⊆ X
33 29 32 sstrd ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → n ⊆ X
34 simprl ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → m ∈ fi ⁡ X
35 34 17 eleqtrdi ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → m ∈ X
36 elsni ⊢ m ∈ X → m = X
37 35 36 syl ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → m = X
38 33 37 sseqtrrd ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → n ⊆ m
39 sseqin2 ⊢ n ⊆ m ↔ m ∩ n = n
40 38 39 sylib ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → m ∩ n = n
41 24 sselda ⊢ R ∈ TosetRel ∧ n ∈ fi ⁡ A ∪ B → n ∈ X ∪ A ∪ B ∪ C
42 41 adantrl ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → n ∈ X ∪ A ∪ B ∪ C
43 40 42 eqeltrd ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → m ∩ n ∈ X ∪ A ∪ B ∪ C
44 eleq1 ⊢ z = m ∩ n → z ∈ X ∪ A ∪ B ∪ C ↔ m ∩ n ∈ X ∪ A ∪ B ∪ C
45 43 44 syl5ibrcom ⊢ R ∈ TosetRel ∧ m ∈ fi ⁡ X ∧ n ∈ fi ⁡ A ∪ B → z = m ∩ n → z ∈ X ∪ A ∪ B ∪ C
46 45 rexlimdvva ⊢ R ∈ TosetRel → ∃ m ∈ fi ⁡ X ∃ n ∈ fi ⁡ A ∪ B z = m ∩ n → z ∈ X ∪ A ∪ B ∪ C
47 21 25 46 3jaod ⊢ R ∈ TosetRel → z ∈ fi ⁡ X ∨ z ∈ fi ⁡ A ∪ B ∨ ∃ m ∈ fi ⁡ X ∃ n ∈ fi ⁡ A ∪ B z = m ∩ n → z ∈ X ∪ A ∪ B ∪ C
48 16 47 sylbid ⊢ R ∈ TosetRel → z ∈ fi ⁡ X ∪ A ∪ B → z ∈ X ∪ A ∪ B ∪ C
49 48 ssrdv ⊢ R ∈ TosetRel → fi ⁡ X ∪ A ∪ B ⊆ X ∪ A ∪ B ∪ C
50 ssfii ⊢ X ∪ A ∪ B ∈ V → X ∪ A ∪ B ⊆ fi ⁡ X ∪ A ∪ B
51 12 50 syl ⊢ R ∈ TosetRel → X ∪ A ∪ B ⊆ fi ⁡ X ∪ A ∪ B
52 51 unssad ⊢ R ∈ TosetRel → X ⊆ fi ⁡ X ∪ A ∪ B
53 fiss ⊢ X ∪ A ∪ B ∈ V ∧ A ∪ B ⊆ X ∪ A ∪ B → fi ⁡ A ∪ B ⊆ fi ⁡ X ∪ A ∪ B
54 12 6 53 sylancl ⊢ R ∈ TosetRel → fi ⁡ A ∪ B ⊆ fi ⁡ X ∪ A ∪ B
55 22 54 eqsstrrd ⊢ R ∈ TosetRel → A ∪ B ∪ C ⊆ fi ⁡ X ∪ A ∪ B
56 52 55 unssd ⊢ R ∈ TosetRel → X ∪ A ∪ B ∪ C ⊆ fi ⁡ X ∪ A ∪ B
57 49 56 eqssd ⊢ R ∈ TosetRel → fi ⁡ X ∪ A ∪ B = X ∪ A ∪ B ∪ C
58 unass ⊢ X ∪ A ∪ B ∪ C = X ∪ A ∪ B ∪ C
59 57 58 eqtr4di ⊢ R ∈ TosetRel → fi ⁡ X ∪ A ∪ B = X ∪ A ∪ B ∪ C