Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtrest2 Structured version   Unicode version

Theorem ordtrest2 17258
 Description: An interval-closed set 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 , but in other sets like there are interval-closed sets like that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.)
Hypotheses
Ref Expression
ordtrest2.1
ordtrest2.2
ordtrest2.3
ordtrest2.4
Assertion
Ref Expression
ordtrest2 ordTop ordTopt
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,

Proof of Theorem ordtrest2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordtrest2.2 . . . 4
2 tsrps 14643 . . . 4
31, 2syl 16 . . 3
4 ordtrest2.1 . . . . 5
5 dmexg 5122 . . . . . 6
61, 5syl 16 . . . . 5
74, 6syl5eqel 2519 . . . 4
8 ordtrest2.3 . . . 4
97, 8ssexd 4342 . . 3
10 ordtrest 17256 . . 3 ordTop ordTopt
113, 9, 10syl2anc 643 . 2 ordTop ordTopt
12 eqid 2435 . . . . . . . 8
13 eqid 2435 . . . . . . . 8
144, 12, 13ordtval 17243 . . . . . . 7 ordTop
151, 14syl 16 . . . . . 6 ordTop
1615oveq1d 6088 . . . . 5 ordTopt t
17 fibas 17032 . . . . . 6
18 tgrest 17213 . . . . . 6 t t
1917, 9, 18sylancr 645 . . . . 5 t t
2016, 19eqtr4d 2470 . . . 4 ordTopt t
21 firest 13650 . . . . 5 t t
2221fveq2i 5723 . . . 4 t t
2320, 22syl6eqr 2485 . . 3 ordTopt t
24 inex1g 4338 . . . . . 6
251, 24syl 16 . . . . 5
26 ordttop 17254 . . . . 5 ordTop
2725, 26syl 16 . . . 4 ordTop
284, 12, 13ordtuni 17244 . . . . . . . . 9
291, 28syl 16 . . . . . . . 8
3029, 7eqeltrrd 2510 . . . . . . 7
31 uniexb 4744 . . . . . . 7
3230, 31sylibr 204 . . . . . 6
33 restval 13644 . . . . . 6 t
3432, 9, 33syl2anc 643 . . . . 5 t
35 dfss1 3537 . . . . . . . . . . . 12
368, 35sylib 189 . . . . . . . . . . 11
37 eqid 2435 . . . . . . . . . . . . . . 15
3837ordttopon 17247 . . . . . . . . . . . . . 14 ordTop TopOn
3925, 38syl 16 . . . . . . . . . . . . 13 ordTop TopOn
404psssdm 14638 . . . . . . . . . . . . . . 15
413, 8, 40syl2anc 643 . . . . . . . . . . . . . 14
4241fveq2d 5724 . . . . . . . . . . . . 13 TopOn TopOn
4339, 42eleqtrd 2511 . . . . . . . . . . . 12 ordTop TopOn
44 toponmax 16983 . . . . . . . . . . . 12 ordTop TopOn ordTop
4543, 44syl 16 . . . . . . . . . . 11 ordTop
4636, 45eqeltrd 2509 . . . . . . . . . 10 ordTop
47 elsni 3830 . . . . . . . . . . . 12
4847ineq1d 3533 . . . . . . . . . . 11
4948eleq1d 2501 . . . . . . . . . 10 ordTop ordTop
5046, 49syl5ibrcom 214 . . . . . . . . 9 ordTop
5150ralrimiv 2780 . . . . . . . 8 ordTop
52 ordtrest2.4 . . . . . . . . . 10
534, 1, 8, 52ordtrest2lem 17257 . . . . . . . . 9 ordTop
54 df-rn 4881 . . . . . . . . . . 11
55 cnvtsr 14644 . . . . . . . . . . . 12
561, 55syl 16 . . . . . . . . . . 11
574psrn 14631 . . . . . . . . . . . . 13
583, 57syl 16 . . . . . . . . . . . 12
598, 58sseqtrd 3376 . . . . . . . . . . 11
6058adantr 452 . . . . . . . . . . . . . . 15
61 rabeq 2942 . . . . . . . . . . . . . . 15
6260, 61syl 16 . . . . . . . . . . . . . 14
63 vex 2951 . . . . . . . . . . . . . . . . . 18
64 vex 2951 . . . . . . . . . . . . . . . . . 18
6563, 64brcnv 5047 . . . . . . . . . . . . . . . . 17
66 vex 2951 . . . . . . . . . . . . . . . . . 18
6764, 66brcnv 5047 . . . . . . . . . . . . . . . . 17
6865, 67anbi12ci 680 . . . . . . . . . . . . . . . 16
6968a1i 11 . . . . . . . . . . . . . . 15
7069rabbiia 2938 . . . . . . . . . . . . . 14
7162, 70syl6eqr 2485 . . . . . . . . . . . . 13
7271, 52eqsstr3d 3375 . . . . . . . . . . . 12
7372ancom2s 778 . . . . . . . . . . 11
7454, 56, 59, 73ordtrest2lem 17257 . . . . . . . . . 10 ordTop
75 vex 2951 . . . . . . . . . . . . . . . . . 18
7675, 64brcnv 5047 . . . . . . . . . . . . . . . . 17
7776bicomi 194 . . . . . . . . . . . . . . . 16
7877a1i 11 . . . . . . . . . . . . . . 15
7978notbid 286 . . . . . . . . . . . . . 14
8058, 79rabeqbidv 2943 . . . . . . . . . . . . 13
8158, 80mpteq12dv 4279 . . . . . . . . . . . 12
8281rneqd 5089 . . . . . . . . . . 11
83 cnvin 5271 . . . . . . . . . . . . . . 15
84 cnvxp 5282 . . . . . . . . . . . . . . . 16
8584ineq2i 3531 . . . . . . . . . . . . . . 15
8683, 85eqtri 2455 . . . . . . . . . . . . . 14
8786fveq2i 5723 . . . . . . . . . . . . 13 ordTop ordTop
88 psss 14636 . . . . . . . . . . . . . . 15
893, 88syl 16 . . . . . . . . . . . . . 14
90 ordtcnv 17255 . . . . . . . . . . . . . 14 ordTop ordTop
9189, 90syl 16 . . . . . . . . . . . . 13 ordTop ordTop
9287, 91syl5reqr 2482 . . . . . . . . . . . 12 ordTop ordTop
9392eleq2d 2502 . . . . . . . . . . 11 ordTop ordTop
9482, 93raleqbidv 2908 . . . . . . . . . 10 ordTop ordTop
9574, 94mpbird 224 . . . . . . . . 9 ordTop
96 ralunb 3520 . . . . . . . . 9 ordTop ordTop ordTop
9753, 95, 96sylanbrc 646 . . . . . . . 8 ordTop
98 ralunb 3520 . . . . . . . 8 ordTop ordTop ordTop
9951, 97, 98sylanbrc 646 . . . . . . 7 ordTop
100 eqid 2435 . . . . . . . 8
101100fmpt 5882 . . . . . . 7 ordTop ordTop
10299, 101sylib 189 . . . . . 6 ordTop
103 frn 5589 . . . . . 6 ordTop ordTop
104102, 103syl 16 . . . . 5 ordTop
10534, 104eqsstrd 3374 . . . 4 t ordTop
106 tgfiss 17046 . . . 4 ordTop t ordTop t ordTop
10727, 105, 106syl2anc 643 . . 3 t ordTop
10823, 107eqsstrd 3374 . 2 ordTopt ordTop
10911, 108eqssd 3357 1 ordTop ordTopt
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   wceq 1652   wcel 1725  wral 2697  crab 2701  cvv 2948   cun 3310   cin 3311   wss 3312  csn 3806  cuni 4007   class class class wbr 4204   cmpt 4258   cxp 4868  ccnv 4869   cdm 4870   crn 4871  wf 5442  cfv 5446  (class class class)co 6073  cfi 7407   ↾t crest 13638  ctg 13655  ordTopcordt 13711  cps 14614   ctsr 14615  ctop 16948  TopOnctopon 16949  ctb 16952 This theorem is referenced by:  ordtrestixx  17276  cnvordtrestixx  24301 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-iin 4088  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-recs 6625  df-rdg 6660  df-1o 6716  df-oadd 6720  df-er 6897  df-en 7102  df-dom 7103  df-fin 7105  df-fi 7408  df-rest 13640  df-topgen 13657  df-ordt 13715  df-ps 14619  df-tsr 14620  df-top 16953  df-bases 16955  df-topon 16956
 Copyright terms: Public domain W3C validator