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 psss
 |-  ( R e. PosetRel -> ( R i^i ( A X. A ) ) e. PosetRel )
81 6 80 syl
 |-  ( ph -> ( R i^i ( A X. A ) ) e. PosetRel )
82 ordtcnv
 |-  ( ( R i^i ( A X. A ) ) e. PosetRel -> ( ordTop ` `' ( R i^i ( A X. A ) ) ) = ( ordTop ` ( R i^i ( A X. A ) ) ) )
83 81 82 syl
 |-  ( ph -> ( ordTop ` `' ( R i^i ( A X. A ) ) ) = ( ordTop ` ( R i^i ( A X. A ) ) ) )
84 cnvin
 |-  `' ( R i^i ( A X. A ) ) = ( `' R i^i `' ( A X. A ) )
85 cnvxp
 |-  `' ( A X. A ) = ( A X. A )
86 85 ineq2i
 |-  ( `' R i^i `' ( A X. A ) ) = ( `' R i^i ( A X. A ) )
87 84 86 eqtri
 |-  `' ( R i^i ( A X. A ) ) = ( `' R i^i ( A X. A ) )
88 87 fveq2i
 |-  ( ordTop ` `' ( R i^i ( A X. A ) ) ) = ( ordTop ` ( `' R i^i ( A X. A ) ) )
89 83 88 eqtr3di
 |-  ( 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 ) )