Metamath Proof Explorer

Theorem ordtrest2

Description: An interval-closed set A in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in RR , but in other sets like QQ there are interval-closed sets like ( _pi , +oo ) i^i QQ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses ordtrest2.1 
|- X = dom R
ordtrest2.2 
|- ( ph -> R e. TosetRel )
ordtrest2.3 
|- ( ph -> A C_ X )
ordtrest2.4 
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. X | ( x R z /\ z R y ) } C_ A )
Assertion ordtrest2 
|- ( ph -> ( ordTop ` ( R i^i ( A X. A ) ) ) = ( ( ordTop ` R ) |`t A ) )

Proof

Step Hyp Ref Expression
1 ordtrest2.1 
 |-  X = dom R
2 ordtrest2.2 
 |-  ( ph -> R e. TosetRel )
3 ordtrest2.3 
 |-  ( ph -> A C_ X )
4 ordtrest2.4 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. X | ( x R z /\ z R y ) } C_ A )
5 tsrps 
 |-  ( R e. TosetRel -> R e. PosetRel )
6 2 5 syl 
 |-  ( ph -> R e. PosetRel )
7 2 dmexd 
 |-  ( ph -> dom R e. _V )
8 1 7 eqeltrid 
 |-  ( ph -> X e. _V )
9 8 3 ssexd 
 |-  ( ph -> A e. _V )
10 ordtrest 
 |-  ( ( R e. PosetRel /\ A e. _V ) -> ( ordTop ` ( R i^i ( A X. A ) ) ) C_ ( ( ordTop ` R ) |`t A ) )
11 6 9 10 syl2anc 
 |-  ( ph -> ( ordTop ` ( R i^i ( A X. A ) ) ) C_ ( ( ordTop ` R ) |`t A ) )
12 eqid 
 |-  ran ( z e. X |-> { w e. X | -. w R z } ) = ran ( z e. X |-> { w e. X | -. w R z } )
13 eqid 
 |-  ran ( z e. X |-> { w e. X | -. z R w } ) = ran ( z e. X |-> { w e. X | -. z R w } )
14 1 12 13 ordtval 
 |-  ( R e. TosetRel -> ( ordTop ` R ) = ( topGen ` ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) ) )
15 2 14 syl 
 |-  ( ph -> ( ordTop ` R ) = ( topGen ` ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) ) )
16 15 oveq1d 
 |-  ( ph -> ( ( ordTop ` R ) |`t A ) = ( ( topGen ` ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) ) |`t A ) )
17 fibas 
 |-  ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) e. TopBases
18 tgrest 
 |-  ( ( ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) e. TopBases /\ A e. _V ) -> ( topGen ` ( ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) |`t A ) ) = ( ( topGen ` ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) ) |`t A ) )
19 17 9 18 sylancr 
 |-  ( ph -> ( topGen ` ( ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) |`t A ) ) = ( ( topGen ` ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) ) |`t A ) )
20 16 19 eqtr4d 
 |-  ( ph -> ( ( ordTop ` R ) |`t A ) = ( topGen ` ( ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) |`t A ) ) )
21 firest 
 |-  ( fi ` ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |`t A ) ) = ( ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) |`t A )
22 21 fveq2i 
 |-  ( topGen ` ( fi ` ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |`t A ) ) ) = ( topGen ` ( ( fi ` ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ) |`t A ) )
23 20 22 eqtr4di 
 |-  ( ph -> ( ( ordTop ` R ) |`t A ) = ( topGen ` ( fi ` ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |`t A ) ) ) )
24 inex1g 
 |-  ( R e. TosetRel -> ( R i^i ( A X. A ) ) e. _V )
25 2 24 syl 
 |-  ( ph -> ( R i^i ( A X. A ) ) e. _V )
26 ordttop 
 |-  ( ( R i^i ( A X. A ) ) e. _V -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. Top )
27 25 26 syl 
 |-  ( ph -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. Top )
28 1 12 13 ordtuni 
 |-  ( R e. TosetRel -> X = U. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) )
29 2 28 syl 
 |-  ( ph -> X = U. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) )
30 29 8 eqeltrrd 
 |-  ( ph -> U. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) e. _V )
31 uniexb 
 |-  ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) e. _V <-> U. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) e. _V )
32 30 31 sylibr 
 |-  ( ph -> ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) e. _V )
33 restval 
 |-  ( ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) e. _V /\ A e. _V ) -> ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |`t A ) = ran ( v e. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |-> ( v i^i A ) ) )
34 32 9 33 syl2anc 
 |-  ( ph -> ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |`t A ) = ran ( v e. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |-> ( v i^i A ) ) )
35 sseqin2 
 |-  ( A C_ X <-> ( X i^i A ) = A )
36 3 35 sylib 
 |-  ( ph -> ( X i^i A ) = A )
37 eqid 
 |-  dom ( R i^i ( A X. A ) ) = dom ( R i^i ( A X. A ) )
38 37 ordttopon 
 |-  ( ( R i^i ( A X. A ) ) e. _V -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. ( TopOn ` dom ( R i^i ( A X. A ) ) ) )
39 25 38 syl 
 |-  ( ph -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. ( TopOn ` dom ( R i^i ( A X. A ) ) ) )
40 1 psssdm 
 |-  ( ( R e. PosetRel /\ A C_ X ) -> dom ( R i^i ( A X. A ) ) = A )
41 6 3 40 syl2anc 
 |-  ( ph -> dom ( R i^i ( A X. A ) ) = A )
42 41 fveq2d 
 |-  ( ph -> ( TopOn ` dom ( R i^i ( A X. A ) ) ) = ( TopOn ` A ) )
43 39 42 eleqtrd 
 |-  ( ph -> ( ordTop ` ( R i^i ( A X. A ) ) ) e. ( TopOn ` A ) )
44 toponmax 
 |-  ( ( ordTop ` ( R i^i ( A X. A ) ) ) e. ( TopOn ` A ) -> A e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
45 43 44 syl 
 |-  ( ph -> A e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
46 36 45 eqeltrd 
 |-  ( ph -> ( X i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
47 elsni 
 |-  ( v e. { X } -> v = X )
48 47 ineq1d 
 |-  ( v e. { X } -> ( v i^i A ) = ( X i^i A ) )
49 48 eleq1d 
 |-  ( v e. { X } -> ( ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> ( X i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
50 46 49 syl5ibrcom 
 |-  ( ph -> ( v e. { X } -> ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
51 50 ralrimiv 
 |-  ( ph -> A. v e. { X } ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
52 1 2 3 4 ordtrest2lem 
 |-  ( ph -> A. v e. ran ( z e. X |-> { w e. X | -. w R z } ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
53 df-rn 
 |-  ran R = dom `' R
54 cnvtsr 
 |-  ( R e. TosetRel -> `' R e. TosetRel )
55 2 54 syl 
 |-  ( ph -> `' R e. TosetRel )
56 1 psrn 
 |-  ( R e. PosetRel -> X = ran R )
57 6 56 syl 
 |-  ( ph -> X = ran R )
58 3 57 sseqtrd 
 |-  ( ph -> A C_ ran R )
59 57 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> X = ran R )
60 59 rabeqdv 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. X | ( x R z /\ z R y ) } = { z e. ran R | ( x R z /\ z R y ) } )
61 vex 
 |-  y e. _V
62 vex 
 |-  z e. _V
63 61 62 brcnv 
 |-  ( y `' R z <-> z R y )
64 vex 
 |-  x e. _V
65 62 64 brcnv 
 |-  ( z `' R x <-> x R z )
66 63 65 anbi12ci 
 |-  ( ( y `' R z /\ z `' R x ) <-> ( x R z /\ z R y ) )
67 66 rabbii 
 |-  { z e. ran R | ( y `' R z /\ z `' R x ) } = { z e. ran R | ( x R z /\ z R y ) }
68 60 67 eqtr4di 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. X | ( x R z /\ z R y ) } = { z e. ran R | ( y `' R z /\ z `' R x ) } )
69 68 4 eqsstrrd 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. ran R | ( y `' R z /\ z `' R x ) } C_ A )
70 69 ancom2s 
 |-  ( ( ph /\ ( y e. A /\ x e. A ) ) -> { z e. ran R | ( y `' R z /\ z `' R x ) } C_ A )
71 53 55 58 70 ordtrest2lem 
 |-  ( ph -> A. v e. ran ( z e. ran R |-> { w e. ran R | -. w `' R z } ) ( v i^i A ) e. ( ordTop ` ( `' R i^i ( A X. A ) ) ) )
72 vex 
 |-  w e. _V
73 72 62 brcnv 
 |-  ( w `' R z <-> z R w )
74 73 bicomi 
 |-  ( z R w <-> w `' R z )
75 74 a1i 
 |-  ( ph -> ( z R w <-> w `' R z ) )
76 75 notbid 
 |-  ( ph -> ( -. z R w <-> -. w `' R z ) )
77 57 76 rabeqbidv 
 |-  ( ph -> { w e. X | -. z R w } = { w e. ran R | -. w `' R z } )
78 57 77 mpteq12dv 
 |-  ( ph -> ( z e. X |-> { w e. X | -. z R w } ) = ( z e. ran R |-> { w e. ran R | -. w `' R z } ) )
79 78 rneqd 
 |-  ( ph -> ran ( z e. X |-> { w e. X | -. z R w } ) = ran ( z e. ran R |-> { w e. ran R | -. w `' R z } ) )
80 cnvin 
 |-  `' ( R i^i ( A X. A ) ) = ( `' R i^i `' ( A X. A ) )
81 cnvxp 
 |-  `' ( A X. A ) = ( A X. A )
82 81 ineq2i 
 |-  ( `' R i^i `' ( A X. A ) ) = ( `' R i^i ( A X. A ) )
83 80 82 eqtri 
 |-  `' ( R i^i ( A X. A ) ) = ( `' R i^i ( A X. A ) )
84 83 fveq2i 
 |-  ( ordTop ` `' ( R i^i ( A X. A ) ) ) = ( ordTop ` ( `' R i^i ( A X. A ) ) )
85 psss 
 |-  ( R e. PosetRel -> ( R i^i ( A X. A ) ) e. PosetRel )
86 6 85 syl 
 |-  ( ph -> ( R i^i ( A X. A ) ) e. PosetRel )
87 ordtcnv 
 |-  ( ( R i^i ( A X. A ) ) e. PosetRel -> ( ordTop ` `' ( R i^i ( A X. A ) ) ) = ( ordTop ` ( R i^i ( A X. A ) ) ) )
88 86 87 syl 
 |-  ( ph -> ( ordTop ` `' ( R i^i ( A X. A ) ) ) = ( ordTop ` ( R i^i ( A X. A ) ) ) )
89 84 88 syl5reqr 
 |-  ( ph -> ( ordTop ` ( R i^i ( A X. A ) ) ) = ( ordTop ` ( `' R i^i ( A X. A ) ) ) )
90 89 eleq2d 
 |-  ( ph -> ( ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> ( v i^i A ) e. ( ordTop ` ( `' R i^i ( A X. A ) ) ) ) )
91 79 90 raleqbidv 
 |-  ( ph -> ( A. v e. ran ( z e. X |-> { w e. X | -. z R w } ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> A. v e. ran ( z e. ran R |-> { w e. ran R | -. w `' R z } ) ( v i^i A ) e. ( ordTop ` ( `' R i^i ( A X. A ) ) ) ) )
92 71 91 mpbird 
 |-  ( ph -> A. v e. ran ( z e. X |-> { w e. X | -. z R w } ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
93 ralunb 
 |-  ( A. v e. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> ( A. v e. ran ( z e. X |-> { w e. X | -. w R z } ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) /\ A. v e. ran ( z e. X |-> { w e. X | -. z R w } ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
94 52 92 93 sylanbrc 
 |-  ( ph -> A. v e. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
95 ralunb 
 |-  ( A. v e. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> ( A. v e. { X } ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) /\ A. v e. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) ) )
96 51 94 95 sylanbrc 
 |-  ( ph -> A. v e. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) )
97 eqid 
 |-  ( v e. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |-> ( v i^i A ) ) = ( v e. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |-> ( v i^i A ) )
98 97 fmpt 
 |-  ( A. v e. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) ( v i^i A ) e. ( ordTop ` ( R i^i ( A X. A ) ) ) <-> ( v e. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |-> ( v i^i A ) ) : ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) --> ( ordTop ` ( R i^i ( A X. A ) ) ) )
99 96 98 sylib 
 |-  ( ph -> ( v e. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |-> ( v i^i A ) ) : ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) --> ( ordTop ` ( R i^i ( A X. A ) ) ) )
100 99 frnd 
 |-  ( ph -> ran ( v e. ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |-> ( v i^i A ) ) C_ ( ordTop ` ( R i^i ( A X. A ) ) ) )
101 34 100 eqsstrd 
 |-  ( ph -> ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |`t A ) C_ ( ordTop ` ( R i^i ( A X. A ) ) ) )
102 tgfiss 
 |-  ( ( ( ordTop ` ( R i^i ( A X. A ) ) ) e. Top /\ ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |`t A ) C_ ( ordTop ` ( R i^i ( A X. A ) ) ) ) -> ( topGen ` ( fi ` ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |`t A ) ) ) C_ ( ordTop ` ( R i^i ( A X. A ) ) ) )
103 27 101 102 syl2anc 
 |-  ( ph -> ( topGen ` ( fi ` ( ( { X } u. ( ran ( z e. X |-> { w e. X | -. w R z } ) u. ran ( z e. X |-> { w e. X | -. z R w } ) ) ) |`t A ) ) ) C_ ( ordTop ` ( R i^i ( A X. A ) ) ) )
104 23 103 eqsstrd 
 |-  ( ph -> ( ( ordTop ` R ) |`t A ) C_ ( ordTop ` ( R i^i ( A X. A ) ) ) )
105 11 104 eqssd 
 |-  ( ph -> ( ordTop ` ( R i^i ( A X. A ) ) ) = ( ( ordTop ` R ) |`t A ) )