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|¬yRx
ordtval.3 ⊢B=ran⁡x∈X⟼y∈X|¬xRy
ordtval.4 ⊢C=ran⁡a∈X,b∈X⟼y∈X|¬yRa∧¬bRy
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|¬yRx
3 ordtval.3 ⊢B=ran⁡x∈X⟼y∈X|¬xRy
4 ordtval.4 ⊢C=ran⁡a∈X,b∈X⟼y∈X|¬yRa∧¬bRy
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∪Bz=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∪Bz=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∪Bz=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∪Bz=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