Theorem ixxdisj

Description: Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014)

	Ref	Expression
Hypotheses	ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
	ixxun.2	⊢ 𝑃 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑇 𝑧 ∧ 𝑧 𝑈 𝑦 ) } )
	ixxun.3	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐵 𝑇 𝑤 ↔ ¬ 𝑤 𝑆 𝐵 ) )
Assertion	ixxdisj	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐵 𝑃 𝐶 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		ixxun.2	⊢ 𝑃 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑇 𝑧 ∧ 𝑧 𝑈 𝑦 ) } )
3		ixxun.3	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐵 𝑇 𝑤 ↔ ¬ 𝑤 𝑆 𝐵 ) )
4		elin	⊢ ( 𝑤 ∈ ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐵 𝑃 𝐶 ) ) ↔ ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) )
5	1	elixx1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
6	5	3adant3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
7	6	biimpa	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) )
8	7	simp3d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 𝑆 𝐵 )
9	8	adantrr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) ) → 𝑤 𝑆 𝐵 )
10	2	elixx1	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐵 𝑇 𝑤 ∧ 𝑤 𝑈 𝐶 ) ) )
11	10	3adant1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐵 𝑇 𝑤 ∧ 𝑤 𝑈 𝐶 ) ) )
12	11	biimpa	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → ( 𝑤 ∈ ℝ* ∧ 𝐵 𝑇 𝑤 ∧ 𝑤 𝑈 𝐶 ) )
13	12	simp2d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐵 𝑇 𝑤 )
14		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐵 ∈ ℝ* )
15	12	simp1d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝑤 ∈ ℝ* )
16	14 15 3	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → ( 𝐵 𝑇 𝑤 ↔ ¬ 𝑤 𝑆 𝐵 ) )
17	13 16	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → ¬ 𝑤 𝑆 𝐵 )
18	17	adantrl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) ) → ¬ 𝑤 𝑆 𝐵 )
19	9 18	pm2.65da	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ¬ ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) )
20	19	pm2.21d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝑤 ∈ ∅ ) )
21	4 20	syl5bi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑤 ∈ ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐵 𝑃 𝐶 ) ) → 𝑤 ∈ ∅ ) )
22	21	ssrdv	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐵 𝑃 𝐶 ) ) ⊆ ∅ )
23		ss0	⊢ ( ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐵 𝑃 𝐶 ) ) ⊆ ∅ → ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐵 𝑃 𝐶 ) ) = ∅ )
24	22 23	syl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐵 𝑃 𝐶 ) ) = ∅ )