This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitrid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( 𝑤 ∈ ( ( 𝐴 𝑂 𝐵 ) ∪ ( 𝐵 𝑃 𝐶 ) ) ↔ 𝑤 ∈ ( 𝐴 𝑄 𝐶 ) ) )
62 61 eqrdv ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑋 𝐶 ) ) → ( ( 𝐴 𝑂 𝐵 ) ∪ ( 𝐵 𝑃 𝐶 ) ) = ( 𝐴 𝑄 𝐶 ) )