Theorem cnvordtrestixx

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)

	Ref	Expression
Hypotheses	cnvordtrestixx.1	⊢ 𝐴 ⊆ ℝ*
	cnvordtrestixx.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
Assertion	cnvordtrestixx	⊢ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) = ( ordTop ‘ ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnvordtrestixx.1	⊢ 𝐴 ⊆ ℝ*
2		cnvordtrestixx.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
3		lern	⊢ ℝ* = ran ≤
4		df-rn	⊢ ran ≤ = dom ◡ ≤
5	3 4	eqtri	⊢ ℝ* = dom ◡ ≤
6		letsr	⊢ ≤ ∈ TosetRel
7		cnvtsr	⊢ ( ≤ ∈ TosetRel → ◡ ≤ ∈ TosetRel )
8	6 7	ax-mp	⊢ ◡ ≤ ∈ TosetRel
9	8	a1i	⊢ ( ⊤ → ◡ ≤ ∈ TosetRel )
10	1	a1i	⊢ ( ⊤ → 𝐴 ⊆ ℝ* )
11		brcnvg	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ℝ* ) → ( 𝑦 ◡ ≤ 𝑧 ↔ 𝑧 ≤ 𝑦 ) )
12	11	adantlr	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ℝ* ) → ( 𝑦 ◡ ≤ 𝑧 ↔ 𝑧 ≤ 𝑦 ) )
13		simpr	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ℝ* ) → 𝑧 ∈ ℝ* )
14		simplr	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ℝ* ) → 𝑥 ∈ 𝐴 )
15		brcnvg	⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 ◡ ≤ 𝑥 ↔ 𝑥 ≤ 𝑧 ) )
16	13 14 15	syl2anc	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ℝ* ) → ( 𝑧 ◡ ≤ 𝑥 ↔ 𝑥 ≤ 𝑧 ) )
17	12 16	anbi12d	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑦 ◡ ≤ 𝑧 ∧ 𝑧 ◡ ≤ 𝑥 ) ↔ ( 𝑧 ≤ 𝑦 ∧ 𝑥 ≤ 𝑧 ) ) )
18		ancom	⊢ ( ( 𝑧 ≤ 𝑦 ∧ 𝑥 ≤ 𝑧 ) ↔ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )
19	17 18	bitrdi	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑦 ◡ ≤ 𝑧 ∧ 𝑧 ◡ ≤ 𝑥 ) ↔ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) ) )
20	19	rabbidva	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { 𝑧 ∈ ℝ* ∣ ( 𝑦 ◡ ≤ 𝑧 ∧ 𝑧 ◡ ≤ 𝑥 ) } = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
21		simpr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
22	1 21	sselid	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
23		simpl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
24	1 23	sselid	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
25		iccval	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 [,] 𝑦 ) = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
26	22 24 25	syl2anc	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 [,] 𝑦 ) = { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
27	2	ancoms	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
28	26 27	eqsstrrd	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ⊆ 𝐴 )
29	20 28	eqsstrd	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { 𝑧 ∈ ℝ* ∣ ( 𝑦 ◡ ≤ 𝑧 ∧ 𝑧 ◡ ≤ 𝑥 ) } ⊆ 𝐴 )
30	29	adantl	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → { 𝑧 ∈ ℝ* ∣ ( 𝑦 ◡ ≤ 𝑧 ∧ 𝑧 ◡ ≤ 𝑥 ) } ⊆ 𝐴 )
31	5 9 10 30	ordtrest2	⊢ ( ⊤ → ( ordTop ‘ ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( ordTop ‘ ◡ ≤ ) ↾t 𝐴 ) )
32	31	mptru	⊢ ( ordTop ‘ ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( ordTop ‘ ◡ ≤ ) ↾t 𝐴 )
33		tsrps	⊢ ( ≤ ∈ TosetRel → ≤ ∈ PosetRel )
34	6 33	ax-mp	⊢ ≤ ∈ PosetRel
35		ordtcnv	⊢ ( ≤ ∈ PosetRel → ( ordTop ‘ ◡ ≤ ) = ( ordTop ‘ ≤ ) )
36	34 35	ax-mp	⊢ ( ordTop ‘ ◡ ≤ ) = ( ordTop ‘ ≤ )
37	36	oveq1i	⊢ ( ( ordTop ‘ ◡ ≤ ) ↾t 𝐴 ) = ( ( ordTop ‘ ≤ ) ↾t 𝐴 )
38	32 37	eqtr2i	⊢ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) = ( ordTop ‘ ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) )