# Metamath Proof Explorer

## Theorem ixxun

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

Ref Expression
Hypotheses ixx.1 ${⊢}{O}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}\right)$
ixxun.2 ${⊢}{P}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{T}{z}\wedge {z}{U}{y}\right)\right\}\right)$
ixxun.3 ${⊢}\left({B}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left({B}{T}{w}↔¬{w}{S}{B}\right)$
ixxun.4 ${⊢}{Q}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{U}{y}\right)\right\}\right)$
ixxun.5 ${⊢}\left({w}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({w}{S}{B}\wedge {B}{X}{C}\right)\to {w}{U}{C}\right)$
ixxun.6 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\left({A}{W}{B}\wedge {B}{T}{w}\right)\to {A}{R}{w}\right)$
Assertion ixxun ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to \left({A}{O}{B}\right)\cup \left({B}{P}{C}\right)={A}{Q}{C}$

### Proof

Step Hyp Ref Expression
1 ixx.1 ${⊢}{O}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}\right)$
2 ixxun.2 ${⊢}{P}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{T}{z}\wedge {z}{U}{y}\right)\right\}\right)$
3 ixxun.3 ${⊢}\left({B}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left({B}{T}{w}↔¬{w}{S}{B}\right)$
4 ixxun.4 ${⊢}{Q}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{U}{y}\right)\right\}\right)$
5 ixxun.5 ${⊢}\left({w}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left(\left({w}{S}{B}\wedge {B}{X}{C}\right)\to {w}{U}{C}\right)$
6 ixxun.6 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\left({A}{W}{B}\wedge {B}{T}{w}\right)\to {A}{R}{w}\right)$
7 elun ${⊢}{w}\in \left(\left({A}{O}{B}\right)\cup \left({B}{P}{C}\right)\right)↔\left({w}\in \left({A}{O}{B}\right)\vee {w}\in \left({B}{P}{C}\right)\right)$
8 simpl1 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to {A}\in {ℝ}^{*}$
9 simpl2 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to {B}\in {ℝ}^{*}$
10 1 elixx1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({w}\in \left({A}{O}{B}\right)↔\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{S}{B}\right)\right)$
11 8 9 10 syl2anc ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to \left({w}\in \left({A}{O}{B}\right)↔\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{S}{B}\right)\right)$
12 11 biimpa ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to \left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{S}{B}\right)$
13 12 simp1d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {w}\in {ℝ}^{*}$
14 12 simp2d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {A}{R}{w}$
15 12 simp3d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {w}{S}{B}$
16 simplrr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {B}{X}{C}$
17 9 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {B}\in {ℝ}^{*}$
18 simpl3 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to {C}\in {ℝ}^{*}$
19 18 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {C}\in {ℝ}^{*}$
20 13 17 19 5 syl3anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to \left(\left({w}{S}{B}\wedge {B}{X}{C}\right)\to {w}{U}{C}\right)$
21 15 16 20 mp2and ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to {w}{U}{C}$
22 13 14 21 3jca ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{O}{B}\right)\right)\to \left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{U}{C}\right)$
23 2 elixx1 ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({w}\in \left({B}{P}{C}\right)↔\left({w}\in {ℝ}^{*}\wedge {B}{T}{w}\wedge {w}{U}{C}\right)\right)$
24 9 18 23 syl2anc ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to \left({w}\in \left({B}{P}{C}\right)↔\left({w}\in {ℝ}^{*}\wedge {B}{T}{w}\wedge {w}{U}{C}\right)\right)$
25 24 biimpa ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({B}{P}{C}\right)\right)\to \left({w}\in {ℝ}^{*}\wedge {B}{T}{w}\wedge {w}{U}{C}\right)$
26 25 simp1d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({B}{P}{C}\right)\right)\to {w}\in {ℝ}^{*}$
27 simplrl ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({B}{P}{C}\right)\right)\to {A}{W}{B}$
28 25 simp2d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({B}{P}{C}\right)\right)\to {B}{T}{w}$
29 8 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({B}{P}{C}\right)\right)\to {A}\in {ℝ}^{*}$
30 9 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({B}{P}{C}\right)\right)\to {B}\in {ℝ}^{*}$
31 29 30 26 6 syl3anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({B}{P}{C}\right)\right)\to \left(\left({A}{W}{B}\wedge {B}{T}{w}\right)\to {A}{R}{w}\right)$
32 27 28 31 mp2and ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({B}{P}{C}\right)\right)\to {A}{R}{w}$
33 25 simp3d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({B}{P}{C}\right)\right)\to {w}{U}{C}$
34 26 32 33 3jca ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({B}{P}{C}\right)\right)\to \left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{U}{C}\right)$
35 22 34 jaodan ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge \left({w}\in \left({A}{O}{B}\right)\vee {w}\in \left({B}{P}{C}\right)\right)\right)\to \left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{U}{C}\right)$
36 4 elixx1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({w}\in \left({A}{Q}{C}\right)↔\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{U}{C}\right)\right)$
37 8 18 36 syl2anc ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to \left({w}\in \left({A}{Q}{C}\right)↔\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{U}{C}\right)\right)$
38 37 biimpar ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge \left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{U}{C}\right)\right)\to {w}\in \left({A}{Q}{C}\right)$
39 35 38 syldan ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge \left({w}\in \left({A}{O}{B}\right)\vee {w}\in \left({B}{P}{C}\right)\right)\right)\to {w}\in \left({A}{Q}{C}\right)$
40 exmid ${⊢}\left({w}{S}{B}\vee ¬{w}{S}{B}\right)$
41 37 biimpa ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{U}{C}\right)$
42 41 simp1d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to {w}\in {ℝ}^{*}$
43 41 simp2d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to {A}{R}{w}$
44 42 43 jca ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\right)$
45 df-3an ${⊢}\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{S}{B}\right)↔\left(\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\right)\wedge {w}{S}{B}\right)$
46 11 45 syl6bb ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to \left({w}\in \left({A}{O}{B}\right)↔\left(\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\right)\wedge {w}{S}{B}\right)\right)$
47 46 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left({w}\in \left({A}{O}{B}\right)↔\left(\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\right)\wedge {w}{S}{B}\right)\right)$
48 44 47 mpbirand ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left({w}\in \left({A}{O}{B}\right)↔{w}{S}{B}\right)$
49 3anan12 ${⊢}\left({w}\in {ℝ}^{*}\wedge {B}{T}{w}\wedge {w}{U}{C}\right)↔\left({B}{T}{w}\wedge \left({w}\in {ℝ}^{*}\wedge {w}{U}{C}\right)\right)$
50 24 49 syl6bb ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to \left({w}\in \left({B}{P}{C}\right)↔\left({B}{T}{w}\wedge \left({w}\in {ℝ}^{*}\wedge {w}{U}{C}\right)\right)\right)$
51 50 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left({w}\in \left({B}{P}{C}\right)↔\left({B}{T}{w}\wedge \left({w}\in {ℝ}^{*}\wedge {w}{U}{C}\right)\right)\right)$
52 41 simp3d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to {w}{U}{C}$
53 42 52 jca ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left({w}\in {ℝ}^{*}\wedge {w}{U}{C}\right)$
54 53 biantrud ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left({B}{T}{w}↔\left({B}{T}{w}\wedge \left({w}\in {ℝ}^{*}\wedge {w}{U}{C}\right)\right)\right)$
55 9 adantr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to {B}\in {ℝ}^{*}$
56 55 42 3 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left({B}{T}{w}↔¬{w}{S}{B}\right)$
57 51 54 56 3bitr2d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left({w}\in \left({B}{P}{C}\right)↔¬{w}{S}{B}\right)$
58 48 57 orbi12d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left(\left({w}\in \left({A}{O}{B}\right)\vee {w}\in \left({B}{P}{C}\right)\right)↔\left({w}{S}{B}\vee ¬{w}{S}{B}\right)\right)$
59 40 58 mpbiri ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\wedge {w}\in \left({A}{Q}{C}\right)\right)\to \left({w}\in \left({A}{O}{B}\right)\vee {w}\in \left({B}{P}{C}\right)\right)$
60 39 59 impbida ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to \left(\left({w}\in \left({A}{O}{B}\right)\vee {w}\in \left({B}{P}{C}\right)\right)↔{w}\in \left({A}{Q}{C}\right)\right)$
61 7 60 syl5bb ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to \left({w}\in \left(\left({A}{O}{B}\right)\cup \left({B}{P}{C}\right)\right)↔{w}\in \left({A}{Q}{C}\right)\right)$
62 61 eqrdv ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{W}{B}\wedge {B}{X}{C}\right)\right)\to \left({A}{O}{B}\right)\cup \left({B}{P}{C}\right)={A}{Q}{C}$