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