ixxss2

Description: Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		ixxss2.2	⊢ 𝑃 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑇 𝑦 ) } )
3		ixxss2.3	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝑤 𝑇 𝐵 ∧ 𝐵 𝑊 𝐶 ) → 𝑤 𝑆 𝐶 ) )
4	2	elixx3g	⊢ ( 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) ∧ ( 𝐴 𝑅 𝑤 ∧ 𝑤 𝑇 𝐵 ) ) )
5	4	simplbi	⊢ ( 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) → ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) )
6	5	adantl	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) )
7	6	simp3d	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → 𝑤 ∈ ℝ^* )
8	4	simprbi	⊢ ( 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) → ( 𝐴 𝑅 𝑤 ∧ 𝑤 𝑇 𝐵 ) )
9	8	adantl	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → ( 𝐴 𝑅 𝑤 ∧ 𝑤 𝑇 𝐵 ) )
10	9	simpld	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → 𝐴 𝑅 𝑤 )
11	9	simprd	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → 𝑤 𝑇 𝐵 )
12		simplr	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → 𝐵 𝑊 𝐶 )
13	6	simp2d	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → 𝐵 ∈ ℝ^* )
14		simpll	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → 𝐶 ∈ ℝ^* )
15	7 13 14 3	syl3anc	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → ( ( 𝑤 𝑇 𝐵 ∧ 𝐵 𝑊 𝐶 ) → 𝑤 𝑆 𝐶 ) )
16	11 12 15	mp2and	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → 𝑤 𝑆 𝐶 )
17	6	simp1d	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → 𝐴 ∈ ℝ^* )
18	1	elixx1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐶 ) ↔ ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐶 ) ) )
19	17 14 18	syl2anc	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐶 ) ↔ ( 𝑤 ∈ ℝ^* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐶 ) ) )
20	7 10 16 19	mpbir3and	⊢ ( ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) ∧ 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) ) → 𝑤 ∈ ( 𝐴 𝑂 𝐶 ) )
21	20	ex	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) → ( 𝑤 ∈ ( 𝐴 𝑃 𝐵 ) → 𝑤 ∈ ( 𝐴 𝑂 𝐶 ) ) )
22	21	ssrdv	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 𝑊 𝐶 ) → ( 𝐴 𝑃 𝐵 ) ⊆ ( 𝐴 𝑂 𝐶 ) )

Metamath Proof Explorer

Theorem ixxss2

Proof