Metamath Proof Explorer


Theorem ordtcld1

Description: A downward ray ( -oo , P ] is closed. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis ordttopon.3 𝑋 = dom 𝑅
Assertion ordtcld1 ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋𝑥 𝑅 𝑃 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 ordttopon.3 𝑋 = dom 𝑅
2 ssrab2 { 𝑥𝑋𝑥 𝑅 𝑃 } ⊆ 𝑋
3 1 ordttopon ( 𝑅𝑉 → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑋 ) )
4 3 adantr ( ( 𝑅𝑉𝑃𝑋 ) → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑋 ) )
5 toponuni ( ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ( ordTop ‘ 𝑅 ) )
6 4 5 syl ( ( 𝑅𝑉𝑃𝑋 ) → 𝑋 = ( ordTop ‘ 𝑅 ) )
7 2 6 sseqtrid ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋𝑥 𝑅 𝑃 } ⊆ ( ordTop ‘ 𝑅 ) )
8 notrab ( 𝑋 ∖ { 𝑥𝑋𝑥 𝑅 𝑃 } ) = { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 }
9 6 difeq1d ( ( 𝑅𝑉𝑃𝑋 ) → ( 𝑋 ∖ { 𝑥𝑋𝑥 𝑅 𝑃 } ) = ( ( ordTop ‘ 𝑅 ) ∖ { 𝑥𝑋𝑥 𝑅 𝑃 } ) )
10 8 9 eqtr3id ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = ( ( ordTop ‘ 𝑅 ) ∖ { 𝑥𝑋𝑥 𝑅 𝑃 } ) )
11 1 ordtopn1 ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ( ordTop ‘ 𝑅 ) )
12 10 11 eqeltrrd ( ( 𝑅𝑉𝑃𝑋 ) → ( ( ordTop ‘ 𝑅 ) ∖ { 𝑥𝑋𝑥 𝑅 𝑃 } ) ∈ ( ordTop ‘ 𝑅 ) )
13 topontop ( ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ 𝑋 ) → ( ordTop ‘ 𝑅 ) ∈ Top )
14 eqid ( ordTop ‘ 𝑅 ) = ( ordTop ‘ 𝑅 )
15 14 iscld ( ( ordTop ‘ 𝑅 ) ∈ Top → ( { 𝑥𝑋𝑥 𝑅 𝑃 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) ↔ ( { 𝑥𝑋𝑥 𝑅 𝑃 } ⊆ ( ordTop ‘ 𝑅 ) ∧ ( ( ordTop ‘ 𝑅 ) ∖ { 𝑥𝑋𝑥 𝑅 𝑃 } ) ∈ ( ordTop ‘ 𝑅 ) ) ) )
16 4 13 15 3syl ( ( 𝑅𝑉𝑃𝑋 ) → ( { 𝑥𝑋𝑥 𝑅 𝑃 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) ↔ ( { 𝑥𝑋𝑥 𝑅 𝑃 } ⊆ ( ordTop ‘ 𝑅 ) ∧ ( ( ordTop ‘ 𝑅 ) ∖ { 𝑥𝑋𝑥 𝑅 𝑃 } ) ∈ ( ordTop ‘ 𝑅 ) ) ) )
17 7 12 16 mpbir2and ( ( 𝑅𝑉𝑃𝑋 ) → { 𝑥𝑋𝑥 𝑅 𝑃 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )