Theorem ordtcld3

Description: A closed interval [ A , B ] is closed. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypothesis	ordttopon.3	⊢ 𝑋 = dom 𝑅
Assertion	ordtcld3	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ( 𝐴 𝑅 𝑥 ∧ 𝑥 𝑅 𝐵 ) } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordttopon.3	⊢ 𝑋 = dom 𝑅
2		inrab	⊢ ( { 𝑥 ∈ 𝑋 ∣ 𝐴 𝑅 𝑥 } ∩ { 𝑥 ∈ 𝑋 ∣ 𝑥 𝑅 𝐵 } ) = { 𝑥 ∈ 𝑋 ∣ ( 𝐴 𝑅 𝑥 ∧ 𝑥 𝑅 𝐵 ) }
3	1	ordtcld2	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ 𝐴 𝑅 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
4	3	3adant3	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ 𝐴 𝑅 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
5	1	ordtcld1	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ 𝑥 𝑅 𝐵 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
6		incld	⊢ ( ( { 𝑥 ∈ 𝑋 ∣ 𝐴 𝑅 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) ∧ { 𝑥 ∈ 𝑋 ∣ 𝑥 𝑅 𝐵 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) ) → ( { 𝑥 ∈ 𝑋 ∣ 𝐴 𝑅 𝑥 } ∩ { 𝑥 ∈ 𝑋 ∣ 𝑥 𝑅 𝐵 } ) ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
7	4 5 6	3imp3i2an	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( { 𝑥 ∈ 𝑋 ∣ 𝐴 𝑅 𝑥 } ∩ { 𝑥 ∈ 𝑋 ∣ 𝑥 𝑅 𝐵 } ) ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
8	2 7	eqeltrrid	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ( 𝐴 𝑅 𝑥 ∧ 𝑥 𝑅 𝐵 ) } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )