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 ⊢ 𝑋 = dom 𝑅
ordtval.2 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
ordtval.3 ⊢ 𝐵 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
ordtval.4 ⊢ 𝐶 = ran ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
Assertion ordtbas ( 𝑅 ∈ TosetRel → ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∪ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ordtval.1 ⊢ 𝑋 = dom 𝑅
2 ordtval.2 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
3 ordtval.3 ⊢ 𝐵 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
4 ordtval.4 ⊢ 𝐶 = ran ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
5 snex ⊢ { 𝑋 } ∈ V
6 ssun2 ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) )
7 1 2 3 ordtuni ⊢ ( 𝑅 ∈ TosetRel → 𝑋 = ∪ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) )
8 dmexg ⊢ ( 𝑅 ∈ TosetRel → dom 𝑅 ∈ V )
9 1 8 eqeltrid ⊢ ( 𝑅 ∈ TosetRel → 𝑋 ∈ V )
10 7 9 eqeltrrd ⊢ ( 𝑅 ∈ TosetRel → ∪ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
11 uniexb ⊢ ( ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V ↔ ∪ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
12 10 11 sylibr ⊢ ( 𝑅 ∈ TosetRel → ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
13 ssexg ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∧ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
14 6 12 13 sylancr ⊢ ( 𝑅 ∈ TosetRel → ( 𝐴 ∪ 𝐵 ) ∈ V )
15 elfiun ⊢ ( ( { 𝑋 } ∈ V ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → ( 𝑧 ∈ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) ↔ ( 𝑧 ∈ ( fi ‘ { 𝑋 } ) ∨ 𝑧 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ∨ ∃ 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∃ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) 𝑧 = ( 𝑚 ∩ 𝑛 ) ) ) )
16 5 14 15 sylancr ⊢ ( 𝑅 ∈ TosetRel → ( 𝑧 ∈ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) ↔ ( 𝑧 ∈ ( fi ‘ { 𝑋 } ) ∨ 𝑧 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ∨ ∃ 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∃ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) 𝑧 = ( 𝑚 ∩ 𝑛 ) ) ) )
17 fisn ⊢ ( fi ‘ { 𝑋 } ) = { 𝑋 }
18 ssun1 ⊢ { 𝑋 } ⊆ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
19 17 18 eqsstri ⊢ ( fi ‘ { 𝑋 } ) ⊆ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
20 19 sseli ⊢ ( 𝑧 ∈ ( fi ‘ { 𝑋 } ) → 𝑧 ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
21 20 a1i ⊢ ( 𝑅 ∈ TosetRel → ( 𝑧 ∈ ( fi ‘ { 𝑋 } ) → 𝑧 ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) ) )
22 1 2 3 4 ordtbas2 ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
23 ssun2 ⊢ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ⊆ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
24 22 23 eqsstrdi ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
25 24 sseld ⊢ ( 𝑅 ∈ TosetRel → ( 𝑧 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) → 𝑧 ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) ) )
26 fipwuni ⊢ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝒫 ∪ ( 𝐴 ∪ 𝐵 )
27 26 sseli ⊢ ( 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) → 𝑛 ∈ 𝒫 ∪ ( 𝐴 ∪ 𝐵 ) )
28 27 elpwid ⊢ ( 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) → 𝑛 ⊆ ∪ ( 𝐴 ∪ 𝐵 ) )
29 28 ad2antll ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → 𝑛 ⊆ ∪ ( 𝐴 ∪ 𝐵 ) )
30 6 unissi ⊢ ∪ ( 𝐴 ∪ 𝐵 ) ⊆ ∪ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) )
31 30 7 sseqtrrid ⊢ ( 𝑅 ∈ TosetRel → ∪ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
32 31 adantr ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → ∪ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
33 29 32 sstrd ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → 𝑛 ⊆ 𝑋 )
34 simprl ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → 𝑚 ∈ ( fi ‘ { 𝑋 } ) )
35 34 17 eleqtrdi ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → 𝑚 ∈ { 𝑋 } )
36 elsni ⊢ ( 𝑚 ∈ { 𝑋 } → 𝑚 = 𝑋 )
37 35 36 syl ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → 𝑚 = 𝑋 )
38 33 37 sseqtrrd ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → 𝑛 ⊆ 𝑚 )
39 sseqin2 ⊢ ( 𝑛 ⊆ 𝑚 ↔ ( 𝑚 ∩ 𝑛 ) = 𝑛 )
40 38 39 sylib ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → ( 𝑚 ∩ 𝑛 ) = 𝑛 )
41 24 sselda ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) → 𝑛 ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
42 41 adantrl ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → 𝑛 ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
43 40 42 eqeltrd ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → ( 𝑚 ∩ 𝑛 ) ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
44 eleq1 ⊢ ( 𝑧 = ( 𝑚 ∩ 𝑛 ) → ( 𝑧 ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) ↔ ( 𝑚 ∩ 𝑛 ) ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) ) )
45 43 44 syl5ibrcom ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∧ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) → ( 𝑧 = ( 𝑚 ∩ 𝑛 ) → 𝑧 ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) ) )
46 45 rexlimdvva ⊢ ( 𝑅 ∈ TosetRel → ( ∃ 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∃ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) 𝑧 = ( 𝑚 ∩ 𝑛 ) → 𝑧 ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) ) )
47 21 25 46 3jaod ⊢ ( 𝑅 ∈ TosetRel → ( ( 𝑧 ∈ ( fi ‘ { 𝑋 } ) ∨ 𝑧 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ∨ ∃ 𝑚 ∈ ( fi ‘ { 𝑋 } ) ∃ 𝑛 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) 𝑧 = ( 𝑚 ∩ 𝑛 ) ) → 𝑧 ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) ) )
48 16 47 sylbid ⊢ ( 𝑅 ∈ TosetRel → ( 𝑧 ∈ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) → 𝑧 ∈ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) ) )
49 48 ssrdv ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) ⊆ ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
50 ssfii ⊢ ( ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V → ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) )
51 12 50 syl ⊢ ( 𝑅 ∈ TosetRel → ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) )
52 51 unssad ⊢ ( 𝑅 ∈ TosetRel → { 𝑋 } ⊆ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) )
53 fiss ⊢ ( ( ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) → ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) )
54 12 6 53 sylancl ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) )
55 22 54 eqsstrrd ⊢ ( 𝑅 ∈ TosetRel → ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) )
56 52 55 unssd ⊢ ( 𝑅 ∈ TosetRel → ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) )
57 49 56 eqssd ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
58 unass ⊢ ( ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∪ 𝐶 ) = ( { 𝑋 } ∪ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
59 57 58 eqtr4di ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) = ( ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∪ 𝐶 ) )