ixxssixx

Description: An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Hypotheses	ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
	ixx.2	⊢ 𝑃 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑇 𝑧 ∧ 𝑧 𝑈 𝑦 ) } )
	ixx.3	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝐴 𝑅 𝑤 → 𝐴 𝑇 𝑤 ) )
	ixx.4	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 𝑆 𝐵 → 𝑤 𝑈 𝐵 ) )
Assertion	ixxssixx	⊢ ( 𝐴 𝑂 𝐵 ) ⊆ ( 𝐴 𝑃 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		ixx.2	⊢ 𝑃 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑇 𝑧 ∧ 𝑧 𝑈 𝑦 ) } )
3		ixx.3	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝐴 𝑅 𝑤 → 𝐴 𝑇 𝑤 ) )
4		ixx.4	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 𝑆 𝐵 → 𝑤 𝑈 𝐵 ) )
5	1	elmpocl	⊢ ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) → ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) )
6		simp1	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) → 𝑤 ∈ ℝ^* )
7	6	a1i	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) → 𝑤 ∈ ℝ^* ) )
8		simpl	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → 𝐴 ∈ ℝ^* )
9		3simpa	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) → ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ) )
10	3	expimpd	⊢ ( 𝐴 ∈ ℝ^* → ( ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ) → 𝐴 𝑇 𝑤 ) )
11	8 9 10	syl2im	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) → 𝐴 𝑇 𝑤 ) )
12		simpr	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → 𝐵 ∈ ℝ^* )
13		3simpb	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) → ( 𝑤 ∈ ℝ^* ∧ 𝑤 𝑆 𝐵 ) )
14	4	ancoms	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝑤 𝑆 𝐵 → 𝑤 𝑈 𝐵 ) )
15	14	expimpd	⊢ ( 𝐵 ∈ ℝ^* → ( ( 𝑤 ∈ ℝ^* ∧ 𝑤 𝑆 𝐵 ) → 𝑤 𝑈 𝐵 ) )
16	12 13 15	syl2im	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) → 𝑤 𝑈 𝐵 ) )
17	7 11 16	3jcad	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) → ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑇 𝑤 ∧ 𝑤 𝑈 𝐵 ) ) )
18	1	elixx1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
19	2	elixx1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ↔ ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑇 𝑤 ∧ 𝑤 𝑈 𝐵 ) ) )
20	17 18 19	3imtr4d	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) → 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) )
21	5 20	mpcom	⊢ ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) → 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) )
22	21	ssriv	⊢ ( 𝐴 𝑂 𝐵 ) ⊆ ( 𝐴 𝑃 𝐵 )

Metamath Proof Explorer

Theorem ixxssixx

Proof