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

Theorem ordtrest 17258
 Description: The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.)
Assertion
Ref Expression
ordtrest ordTop ordTopt

Proof of Theorem ordtrest
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inex1g 4338 . . . 4
3 eqid 2435 . . . 4
4 eqid 2435 . . . 4
5 eqid 2435 . . . 4
63, 4, 5ordtval 17245 . . 3 ordTop
72, 6syl 16 . 2 ordTop
8 ordttop 17256 . . . 4 ordTop
9 resttop 17216 . . . 4 ordTop ordTopt
108, 9sylan 458 . . 3 ordTopt
11 eqid 2435 . . . . . . . 8
1211psssdm2 14639 . . . . . . 7
1312adantr 452 . . . . . 6
148adantr 452 . . . . . . 7 ordTop
15 simpr 448 . . . . . . 7
1611ordttopon 17249 . . . . . . . . 9 ordTop TopOn
1716adantr 452 . . . . . . . 8 ordTop TopOn
18 toponmax 16985 . . . . . . . 8 ordTop TopOn ordTop
1917, 18syl 16 . . . . . . 7 ordTop
20 elrestr 13648 . . . . . . 7 ordTop ordTop ordTopt
2114, 15, 19, 20syl3anc 1184 . . . . . 6 ordTopt
2213, 21eqeltrd 2509 . . . . 5 ordTopt
2322snssd 3935 . . . 4 ordTopt
24 rabeq 2942 . . . . . . . . 9
2513, 24syl 16 . . . . . . . 8
2613, 25mpteq12dv 4279 . . . . . . 7
2726rneqd 5089 . . . . . 6
28 inrab2 3606 . . . . . . . . . 10
29 inss2 3554 . . . . . . . . . . . . . 14
30 simpr 448 . . . . . . . . . . . . . 14
3129, 30sseldi 3338 . . . . . . . . . . . . 13
32 simpr 448 . . . . . . . . . . . . . . 15
3329, 32sseldi 3338 . . . . . . . . . . . . . 14
3433adantr 452 . . . . . . . . . . . . 13
35 brinxp 4932 . . . . . . . . . . . . 13
3631, 34, 35syl2anc 643 . . . . . . . . . . . 12
3736notbid 286 . . . . . . . . . . 11
3837rabbidva 2939 . . . . . . . . . 10
3928, 38syl5eq 2479 . . . . . . . . 9
4014adantr 452 . . . . . . . . . 10 ordTop
4115adantr 452 . . . . . . . . . 10
42 simpl 444 . . . . . . . . . . 11
43 inss1 3553 . . . . . . . . . . . 12
4443sseli 3336 . . . . . . . . . . 11
4511ordtopn1 17250 . . . . . . . . . . 11 ordTop
4642, 44, 45syl2an 464 . . . . . . . . . 10 ordTop
47 elrestr 13648 . . . . . . . . . 10 ordTop ordTop ordTopt
4840, 41, 46, 47syl3anc 1184 . . . . . . . . 9 ordTopt
4939, 48eqeltrrd 2510 . . . . . . . 8 ordTopt
50 eqid 2435 . . . . . . . 8
5149, 50fmptd 5885 . . . . . . 7 ordTopt
52 frn 5589 . . . . . . 7 ordTopt ordTopt
5351, 52syl 16 . . . . . 6 ordTopt
5427, 53eqsstrd 3374 . . . . 5 ordTopt
55 rabeq 2942 . . . . . . . . 9
5613, 55syl 16 . . . . . . . 8
5713, 56mpteq12dv 4279 . . . . . . 7
5857rneqd 5089 . . . . . 6
59 inrab2 3606 . . . . . . . . . 10
60 brinxp 4932 . . . . . . . . . . . . 13
6134, 31, 60syl2anc 643 . . . . . . . . . . . 12
6261notbid 286 . . . . . . . . . . 11
6362rabbidva 2939 . . . . . . . . . 10
6459, 63syl5eq 2479 . . . . . . . . 9
6511ordtopn2 17251 . . . . . . . . . . 11 ordTop
6642, 44, 65syl2an 464 . . . . . . . . . 10 ordTop
67 elrestr 13648 . . . . . . . . . 10 ordTop ordTop ordTopt
6840, 41, 66, 67syl3anc 1184 . . . . . . . . 9 ordTopt
6964, 68eqeltrrd 2510 . . . . . . . 8 ordTopt
70 eqid 2435 . . . . . . . 8
7169, 70fmptd 5885 . . . . . . 7 ordTopt
72 frn 5589 . . . . . . 7 ordTopt ordTopt
7371, 72syl 16 . . . . . 6 ordTopt
7458, 73eqsstrd 3374 . . . . 5 ordTopt
7554, 74unssd 3515 . . . 4 ordTopt
7623, 75unssd 3515 . . 3 ordTopt
77 tgfiss 17048 . . 3 ordTopt ordTopt ordTopt
7810, 76, 77syl2anc 643 . 2 ordTopt
797, 78eqsstrd 3374 1 ordTop ordTopt
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   wceq 1652   wcel 1725  crab 2701  cvv 2948   cun 3310   cin 3311   wss 3312  csn 3806   class class class wbr 4204   cmpt 4258   cxp 4868   cdm 4870   crn 4871  wf 5442  cfv 5446  (class class class)co 6073  cfi 7407   ↾t crest 13640  ctg 13657  ordTopcordt 13713  cps 14616  ctop 16950  TopOnctopon 16951 This theorem is referenced by:  ordtrest2  17260 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-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-fin 7105  df-fi 7408  df-rest 13642  df-topgen 13659  df-ordt 13717  df-ps 14621  df-top 16955  df-bases 16957  df-topon 16958
 Copyright terms: Public domain W3C validator