Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cnvordtrestixx Structured version   Visualization version   GIF version

Theorem cnvordtrestixx 31999
Description: The restriction of the 'greater than' order to an interval gives the same topology as the subspace topology. (Contributed by Thierry Arnoux, 1-Apr-2017.)
Hypotheses
Ref Expression
cnvordtrestixx.1 𝐴 ⊆ ℝ*
cnvordtrestixx.2 ((𝑥𝐴𝑦𝐴) → (𝑥[,]𝑦) ⊆ 𝐴)
Assertion
Ref Expression
cnvordtrestixx ((ordTop‘ ≤ ) ↾t 𝐴) = (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))
Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem cnvordtrestixx
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 lern 18383 . . . . 5 * = ran ≤
2 df-rn 5618 . . . . 5 ran ≤ = dom
31, 2eqtri 2764 . . . 4 * = dom
4 letsr 18385 . . . . . 6 ≤ ∈ TosetRel
5 cnvtsr 18380 . . . . . 6 ( ≤ ∈ TosetRel → ≤ ∈ TosetRel )
64, 5ax-mp 5 . . . . 5 ≤ ∈ TosetRel
76a1i 11 . . . 4 (⊤ → ≤ ∈ TosetRel )
8 cnvordtrestixx.1 . . . . 5 𝐴 ⊆ ℝ*
98a1i 11 . . . 4 (⊤ → 𝐴 ⊆ ℝ*)
10 brcnvg 5808 . . . . . . . . . 10 ((𝑦𝐴𝑧 ∈ ℝ*) → (𝑦𝑧𝑧𝑦))
1110adantlr 712 . . . . . . . . 9 (((𝑦𝐴𝑥𝐴) ∧ 𝑧 ∈ ℝ*) → (𝑦𝑧𝑧𝑦))
12 simpr 485 . . . . . . . . . 10 (((𝑦𝐴𝑥𝐴) ∧ 𝑧 ∈ ℝ*) → 𝑧 ∈ ℝ*)
13 simplr 766 . . . . . . . . . 10 (((𝑦𝐴𝑥𝐴) ∧ 𝑧 ∈ ℝ*) → 𝑥𝐴)
14 brcnvg 5808 . . . . . . . . . 10 ((𝑧 ∈ ℝ*𝑥𝐴) → (𝑧𝑥𝑥𝑧))
1512, 13, 14syl2anc 584 . . . . . . . . 9 (((𝑦𝐴𝑥𝐴) ∧ 𝑧 ∈ ℝ*) → (𝑧𝑥𝑥𝑧))
1611, 15anbi12d 631 . . . . . . . 8 (((𝑦𝐴𝑥𝐴) ∧ 𝑧 ∈ ℝ*) → ((𝑦𝑧𝑧𝑥) ↔ (𝑧𝑦𝑥𝑧)))
17 ancom 461 . . . . . . . 8 ((𝑧𝑦𝑥𝑧) ↔ (𝑥𝑧𝑧𝑦))
1816, 17bitrdi 286 . . . . . . 7 (((𝑦𝐴𝑥𝐴) ∧ 𝑧 ∈ ℝ*) → ((𝑦𝑧𝑧𝑥) ↔ (𝑥𝑧𝑧𝑦)))
1918rabbidva 3410 . . . . . 6 ((𝑦𝐴𝑥𝐴) → {𝑧 ∈ ℝ* ∣ (𝑦𝑧𝑧𝑥)} = {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
20 simpr 485 . . . . . . . . 9 ((𝑦𝐴𝑥𝐴) → 𝑥𝐴)
218, 20sselid 3928 . . . . . . . 8 ((𝑦𝐴𝑥𝐴) → 𝑥 ∈ ℝ*)
22 simpl 483 . . . . . . . . 9 ((𝑦𝐴𝑥𝐴) → 𝑦𝐴)
238, 22sselid 3928 . . . . . . . 8 ((𝑦𝐴𝑥𝐴) → 𝑦 ∈ ℝ*)
24 iccval 13197 . . . . . . . 8 ((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) → (𝑥[,]𝑦) = {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
2521, 23, 24syl2anc 584 . . . . . . 7 ((𝑦𝐴𝑥𝐴) → (𝑥[,]𝑦) = {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
26 cnvordtrestixx.2 . . . . . . . 8 ((𝑥𝐴𝑦𝐴) → (𝑥[,]𝑦) ⊆ 𝐴)
2726ancoms 459 . . . . . . 7 ((𝑦𝐴𝑥𝐴) → (𝑥[,]𝑦) ⊆ 𝐴)
2825, 27eqsstrrd 3969 . . . . . 6 ((𝑦𝐴𝑥𝐴) → {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)} ⊆ 𝐴)
2919, 28eqsstrd 3968 . . . . 5 ((𝑦𝐴𝑥𝐴) → {𝑧 ∈ ℝ* ∣ (𝑦𝑧𝑧𝑥)} ⊆ 𝐴)
3029adantl 482 . . . 4 ((⊤ ∧ (𝑦𝐴𝑥𝐴)) → {𝑧 ∈ ℝ* ∣ (𝑦𝑧𝑧𝑥)} ⊆ 𝐴)
313, 7, 9, 30ordtrest2 22435 . . 3 (⊤ → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = ((ordTop‘ ≤ ) ↾t 𝐴))
3231mptru 1547 . 2 (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = ((ordTop‘ ≤ ) ↾t 𝐴)
33 tsrps 18379 . . . . 5 ( ≤ ∈ TosetRel → ≤ ∈ PosetRel)
344, 33ax-mp 5 . . . 4 ≤ ∈ PosetRel
35 ordtcnv 22432 . . . 4 ( ≤ ∈ PosetRel → (ordTop‘ ≤ ) = (ordTop‘ ≤ ))
3634, 35ax-mp 5 . . 3 (ordTop‘ ≤ ) = (ordTop‘ ≤ )
3736oveq1i 7326 . 2 ((ordTop‘ ≤ ) ↾t 𝐴) = ((ordTop‘ ≤ ) ↾t 𝐴)
3832, 37eqtr2i 2765 1 ((ordTop‘ ≤ ) ↾t 𝐴) = (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wtru 1541  wcel 2105  {crab 3403  cin 3895  wss 3896   class class class wbr 5086   × cxp 5605  ccnv 5606  dom cdm 5607  ran crn 5608  cfv 6465  (class class class)co 7316  *cxr 11087  cle 11089  [,]cicc 13161  t crest 17205  ordTopcordt 17284  PosetRelcps 18356   TosetRel ctsr 18357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5223  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-cnex 11006  ax-resscn 11007  ax-pre-lttri 11024  ax-pre-lttrn 11025
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-int 4892  df-iun 4938  df-iin 4939  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-ov 7319  df-oprab 7320  df-mpo 7321  df-om 7759  df-1st 7877  df-2nd 7878  df-1o 8345  df-er 8547  df-en 8783  df-dom 8784  df-sdom 8785  df-fin 8786  df-fi 9246  df-pnf 11090  df-mnf 11091  df-xr 11092  df-ltxr 11093  df-le 11094  df-icc 13165  df-rest 17207  df-topgen 17228  df-ordt 17286  df-ps 18358  df-tsr 18359  df-top 22123  df-topon 22140  df-bases 22176
This theorem is referenced by:  xrge0iifhmeo  32022
  Copyright terms: Public domain W3C validator