This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑅 ) ) )