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

Metamath Proof Explorer

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