Theorem ordtcld2

Description: An upward ray [ P , +oo ) is closed. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypothesis	ordttopon.3	⊢ 𝑋 = dom 𝑅
Assertion	ordtcld2	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ 𝑃 𝑅 𝑥 } ∈ ( 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	ordtopn2	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ∈ ( 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 ‘ 𝑅 ) ) )