Theorem ixxun

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

	Ref	Expression
Hypotheses	ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
	ixxun.2	⊢ 𝑃 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑇 𝑧 ∧ 𝑧 𝑈 𝑦 ) } )
	ixxun.3	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐵 𝑇 𝑤 ↔ ¬ 𝑤 𝑆 𝐵 ) )
	ixxun.4	⊢ 𝑄 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑈 𝑦 ) } )
	ixxun.5	⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝑤 𝑆 𝐵 ∧ 𝐵 𝑋 𝐶 ) → 𝑤 𝑈 𝐶 ) )
	ixxun.6	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑇 𝑤 ) → 𝐴 𝑅 𝑤 ) )
Assertion	ixxun	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( ( 𝐴 𝑂 𝐵 ) ∪ ( 𝐵 𝑃 𝐶 ) ) = ( 𝐴 𝑄 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		ixxun.2	⊢ 𝑃 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑇 𝑧 ∧ 𝑧 𝑈 𝑦 ) } )
3		ixxun.3	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐵 𝑇 𝑤 ↔ ¬ 𝑤 𝑆 𝐵 ) )
4		ixxun.4	⊢ 𝑄 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑈 𝑦 ) } )
5		ixxun.5	⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝑤 𝑆 𝐵 ∧ 𝐵 𝑋 𝐶 ) → 𝑤 𝑈 𝐶 ) )
6		ixxun.6	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑇 𝑤 ) → 𝐴 𝑅 𝑤 ) )
7		elun	⊢ ( 𝑤 ∈ ( ( 𝐴 𝑂 𝐵 ) ∪ ( 𝐵 𝑃 𝐶 ) ) ↔ ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∨ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) )
8		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → 𝐴 ∈ ℝ* )
9		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → 𝐵 ∈ ℝ* )
10	1	elixx1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
11	8 9 10	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) )
12	11	biimpa	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) )
13	12	simp1d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 ∈ ℝ* )
14	12	simp2d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 𝑅 𝑤 )
15	12	simp3d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 𝑆 𝐵 )
16		simplrr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐵 𝑋 𝐶 )
17	9	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐵 ∈ ℝ* )
18		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → 𝐶 ∈ ℝ* )
19	18	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐶 ∈ ℝ* )
20	13 17 19 5	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( ( 𝑤 𝑆 𝐵 ∧ 𝐵 𝑋 𝐶 ) → 𝑤 𝑈 𝐶 ) )
21	15 16 20	mp2and	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 𝑈 𝐶 )
22	13 14 21	3jca	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑈 𝐶 ) )
23	2	elixx1	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐵 𝑇 𝑤 ∧ 𝑤 𝑈 𝐶 ) ) )
24	9 18 23	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐵 𝑇 𝑤 ∧ 𝑤 𝑈 𝐶 ) ) )
25	24	biimpa	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → ( 𝑤 ∈ ℝ* ∧ 𝐵 𝑇 𝑤 ∧ 𝑤 𝑈 𝐶 ) )
26	25	simp1d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝑤 ∈ ℝ* )
27		simplrl	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐴 𝑊 𝐵 )
28	25	simp2d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐵 𝑇 𝑤 )
29	8	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐴 ∈ ℝ* )
30	9	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐵 ∈ ℝ* )
31	29 30 26 6	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → ( ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑇 𝑤 ) → 𝐴 𝑅 𝑤 ) )
32	27 28 31	mp2and	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐴 𝑅 𝑤 )
33	25	simp3d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝑤 𝑈 𝐶 )
34	26 32 33	3jca	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑈 𝐶 ) )
35	22 34	jaodan	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∨ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) ) → ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑈 𝐶 ) )
36	4	elixx1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑈 𝐶 ) ) )
37	8 18 36	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑈 𝐶 ) ) )
38	37	biimpar	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑈 𝐶 ) ) → 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) )
39	35 38	syldan	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∨ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) ) → 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) )
40		exmid	⊢ ( 𝑤 𝑆 𝐵 ∨ ¬ 𝑤 𝑆 𝐵 )
41	37	biimpa	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑈 𝐶 ) )
42	41	simp1d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → 𝑤 ∈ ℝ* )
43	41	simp2d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → 𝐴 𝑅 𝑤 )
44	42 43	jca	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ) )
45		df-3an	⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ↔ ( ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ) ∧ 𝑤 𝑆 𝐵 ) )
46	11 45	bitrdi	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ) ∧ 𝑤 𝑆 𝐵 ) ) )
47	46	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ) ∧ 𝑤 𝑆 𝐵 ) ) )
48	44 47	mpbirand	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ 𝑤 𝑆 𝐵 ) )
49		3anan12	⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 𝑇 𝑤 ∧ 𝑤 𝑈 𝐶 ) ↔ ( 𝐵 𝑇 𝑤 ∧ ( 𝑤 ∈ ℝ* ∧ 𝑤 𝑈 𝐶 ) ) )
50	24 49	bitrdi	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ↔ ( 𝐵 𝑇 𝑤 ∧ ( 𝑤 ∈ ℝ* ∧ 𝑤 𝑈 𝐶 ) ) ) )
51	50	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ↔ ( 𝐵 𝑇 𝑤 ∧ ( 𝑤 ∈ ℝ* ∧ 𝑤 𝑈 𝐶 ) ) ) )
52	41	simp3d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → 𝑤 𝑈 𝐶 )
53	42 52	jca	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( 𝑤 ∈ ℝ* ∧ 𝑤 𝑈 𝐶 ) )
54	53	biantrud	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( 𝐵 𝑇 𝑤 ↔ ( 𝐵 𝑇 𝑤 ∧ ( 𝑤 ∈ ℝ* ∧ 𝑤 𝑈 𝐶 ) ) ) )
55	9	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → 𝐵 ∈ ℝ* )
56	55 42 3	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( 𝐵 𝑇 𝑤 ↔ ¬ 𝑤 𝑆 𝐵 ) )
57	51 54 56	3bitr2d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ↔ ¬ 𝑤 𝑆 𝐵 ) )
58	48 57	orbi12d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∨ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) ↔ ( 𝑤 𝑆 𝐵 ∨ ¬ 𝑤 𝑆 𝐵 ) ) )
59	40 58	mpbiri	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) ∧ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∨ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) )
60	39 59	impbida	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ∨ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) ↔ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) )
61	7 60	syl5bb	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( 𝑤 ∈ ( ( 𝐴 𝑂 𝐵 ) ∪ ( 𝐵 𝑃 𝐶 ) ) ↔ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) )
62	61	eqrdv	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( ( 𝐴 𝑂 𝐵 ) ∪ ( 𝐵 𝑃 𝐶 ) ) = ( 𝐴 𝑄 𝐶 ) )