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 e. X |-> { y e. X | -. y R x } )
ordtval.3 
|- B = ran ( x e. X |-> { y e. X | -. x R y } )
ordtval.4 
|- C = ran ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } )
Assertion ordtbas 
|- ( R e. TosetRel -> ( fi ` ( { X } u. ( A u. B ) ) ) = ( ( { X } u. ( A u. B ) ) u. C ) )

Proof

Step Hyp Ref Expression
1 ordtval.1 
 |-  X = dom R
2 ordtval.2 
 |-  A = ran ( x e. X |-> { y e. X | -. y R x } )
3 ordtval.3 
 |-  B = ran ( x e. X |-> { y e. X | -. x R y } )
4 ordtval.4 
 |-  C = ran ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } )
5 snex 
 |-  { X } e. _V
6 ssun2 
 |-  ( A u. B ) C_ ( { X } u. ( A u. B ) )
7 1 2 3 ordtuni 
 |-  ( R e. TosetRel -> X = U. ( { X } u. ( A u. B ) ) )
8 dmexg 
 |-  ( R e. TosetRel -> dom R e. _V )
9 1 8 eqeltrid 
 |-  ( R e. TosetRel -> X e. _V )
10 7 9 eqeltrrd 
 |-  ( R e. TosetRel -> U. ( { X } u. ( A u. B ) ) e. _V )
11 uniexb 
 |-  ( ( { X } u. ( A u. B ) ) e. _V <-> U. ( { X } u. ( A u. B ) ) e. _V )
12 10 11 sylibr 
 |-  ( R e. TosetRel -> ( { X } u. ( A u. B ) ) e. _V )
13 ssexg 
 |-  ( ( ( A u. B ) C_ ( { X } u. ( A u. B ) ) /\ ( { X } u. ( A u. B ) ) e. _V ) -> ( A u. B ) e. _V )
14 6 12 13 sylancr 
 |-  ( R e. TosetRel -> ( A u. B ) e. _V )
15 elfiun 
 |-  ( ( { X } e. _V /\ ( A u. B ) e. _V ) -> ( z e. ( fi ` ( { X } u. ( A u. B ) ) ) <-> ( z e. ( fi ` { X } ) \/ z e. ( fi ` ( A u. B ) ) \/ E. m e. ( fi ` { X } ) E. n e. ( fi ` ( A u. B ) ) z = ( m i^i n ) ) ) )
16 5 14 15 sylancr 
 |-  ( R e. TosetRel -> ( z e. ( fi ` ( { X } u. ( A u. B ) ) ) <-> ( z e. ( fi ` { X } ) \/ z e. ( fi ` ( A u. B ) ) \/ E. m e. ( fi ` { X } ) E. n e. ( fi ` ( A u. B ) ) z = ( m i^i n ) ) ) )
17 fisn 
 |-  ( fi ` { X } ) = { X }
18 ssun1 
 |-  { X } C_ ( { X } u. ( ( A u. B ) u. C ) )
19 17 18 eqsstri 
 |-  ( fi ` { X } ) C_ ( { X } u. ( ( A u. B ) u. C ) )
20 19 sseli 
 |-  ( z e. ( fi ` { X } ) -> z e. ( { X } u. ( ( A u. B ) u. C ) ) )
21 20 a1i 
 |-  ( R e. TosetRel -> ( z e. ( fi ` { X } ) -> z e. ( { X } u. ( ( A u. B ) u. C ) ) ) )
22 1 2 3 4 ordtbas2 
 |-  ( R e. TosetRel -> ( fi ` ( A u. B ) ) = ( ( A u. B ) u. C ) )
23 ssun2 
 |-  ( ( A u. B ) u. C ) C_ ( { X } u. ( ( A u. B ) u. C ) )
24 22 23 eqsstrdi 
 |-  ( R e. TosetRel -> ( fi ` ( A u. B ) ) C_ ( { X } u. ( ( A u. B ) u. C ) ) )
25 24 sseld 
 |-  ( R e. TosetRel -> ( z e. ( fi ` ( A u. B ) ) -> z e. ( { X } u. ( ( A u. B ) u. C ) ) ) )
26 fipwuni 
 |-  ( fi ` ( A u. B ) ) C_ ~P U. ( A u. B )
27 26 sseli 
 |-  ( n e. ( fi ` ( A u. B ) ) -> n e. ~P U. ( A u. B ) )
28 27 elpwid 
 |-  ( n e. ( fi ` ( A u. B ) ) -> n C_ U. ( A u. B ) )
29 28 ad2antll 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> n C_ U. ( A u. B ) )
30 6 unissi 
 |-  U. ( A u. B ) C_ U. ( { X } u. ( A u. B ) )
31 30 7 sseqtrrid 
 |-  ( R e. TosetRel -> U. ( A u. B ) C_ X )
32 31 adantr 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> U. ( A u. B ) C_ X )
33 29 32 sstrd 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> n C_ X )
34 simprl 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> m e. ( fi ` { X } ) )
35 34 17 eleqtrdi 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> m e. { X } )
36 elsni 
 |-  ( m e. { X } -> m = X )
37 35 36 syl 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> m = X )
38 33 37 sseqtrrd 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> n C_ m )
39 sseqin2 
 |-  ( n C_ m <-> ( m i^i n ) = n )
40 38 39 sylib 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> ( m i^i n ) = n )
41 24 sselda 
 |-  ( ( R e. TosetRel /\ n e. ( fi ` ( A u. B ) ) ) -> n e. ( { X } u. ( ( A u. B ) u. C ) ) )
42 41 adantrl 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> n e. ( { X } u. ( ( A u. B ) u. C ) ) )
43 40 42 eqeltrd 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> ( m i^i n ) e. ( { X } u. ( ( A u. B ) u. C ) ) )
44 eleq1 
 |-  ( z = ( m i^i n ) -> ( z e. ( { X } u. ( ( A u. B ) u. C ) ) <-> ( m i^i n ) e. ( { X } u. ( ( A u. B ) u. C ) ) ) )
45 43 44 syl5ibrcom 
 |-  ( ( R e. TosetRel /\ ( m e. ( fi ` { X } ) /\ n e. ( fi ` ( A u. B ) ) ) ) -> ( z = ( m i^i n ) -> z e. ( { X } u. ( ( A u. B ) u. C ) ) ) )
46 45 rexlimdvva 
 |-  ( R e. TosetRel -> ( E. m e. ( fi ` { X } ) E. n e. ( fi ` ( A u. B ) ) z = ( m i^i n ) -> z e. ( { X } u. ( ( A u. B ) u. C ) ) ) )
47 21 25 46 3jaod 
 |-  ( R e. TosetRel -> ( ( z e. ( fi ` { X } ) \/ z e. ( fi ` ( A u. B ) ) \/ E. m e. ( fi ` { X } ) E. n e. ( fi ` ( A u. B ) ) z = ( m i^i n ) ) -> z e. ( { X } u. ( ( A u. B ) u. C ) ) ) )
48 16 47 sylbid 
 |-  ( R e. TosetRel -> ( z e. ( fi ` ( { X } u. ( A u. B ) ) ) -> z e. ( { X } u. ( ( A u. B ) u. C ) ) ) )
49 48 ssrdv 
 |-  ( R e. TosetRel -> ( fi ` ( { X } u. ( A u. B ) ) ) C_ ( { X } u. ( ( A u. B ) u. C ) ) )
50 ssfii 
 |-  ( ( { X } u. ( A u. B ) ) e. _V -> ( { X } u. ( A u. B ) ) C_ ( fi ` ( { X } u. ( A u. B ) ) ) )
51 12 50 syl 
 |-  ( R e. TosetRel -> ( { X } u. ( A u. B ) ) C_ ( fi ` ( { X } u. ( A u. B ) ) ) )
52 51 unssad 
 |-  ( R e. TosetRel -> { X } C_ ( fi ` ( { X } u. ( A u. B ) ) ) )
53 fiss 
 |-  ( ( ( { X } u. ( A u. B ) ) e. _V /\ ( A u. B ) C_ ( { X } u. ( A u. B ) ) ) -> ( fi ` ( A u. B ) ) C_ ( fi ` ( { X } u. ( A u. B ) ) ) )
54 12 6 53 sylancl 
 |-  ( R e. TosetRel -> ( fi ` ( A u. B ) ) C_ ( fi ` ( { X } u. ( A u. B ) ) ) )
55 22 54 eqsstrrd 
 |-  ( R e. TosetRel -> ( ( A u. B ) u. C ) C_ ( fi ` ( { X } u. ( A u. B ) ) ) )
56 52 55 unssd 
 |-  ( R e. TosetRel -> ( { X } u. ( ( A u. B ) u. C ) ) C_ ( fi ` ( { X } u. ( A u. B ) ) ) )
57 49 56 eqssd 
 |-  ( R e. TosetRel -> ( fi ` ( { X } u. ( A u. B ) ) ) = ( { X } u. ( ( A u. B ) u. C ) ) )
58 unass 
 |-  ( ( { X } u. ( A u. B ) ) u. C ) = ( { X } u. ( ( A u. B ) u. C ) )
59 57 58 eqtr4di 
 |-  ( R e. TosetRel -> ( fi ` ( { X } u. ( A u. B ) ) ) = ( ( { X } u. ( A u. B ) ) u. C ) )