ixxss12

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

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

Proof

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

Metamath Proof Explorer

Theorem ixxss12

Proof