MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ixxun Structured version   Visualization version   GIF version

Theorem ixxun 12018
Description: Split an interval into two parts. (Contributed by Mario Carneiro, 16-Jun-2014.)
Hypotheses
Ref Expression
ixx.1 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})
ixxun.2 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑈𝑦)})
ixxun.3 ((𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵))
ixxun.4 𝑄 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑈𝑦)})
ixxun.5 ((𝑤 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝑤𝑆𝐵𝐵𝑋𝐶) → 𝑤𝑈𝐶))
ixxun.6 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵𝐵𝑇𝑤) → 𝐴𝑅𝑤))
Assertion
Ref Expression
ixxun (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → ((𝐴𝑂𝐵) ∪ (𝐵𝑃𝐶)) = (𝐴𝑄𝐶))
Distinct variable groups:   𝑥,𝑤,𝑦,𝑧,𝐴   𝑤,𝐶,𝑥,𝑦,𝑧   𝑤,𝑂   𝑤,𝑄   𝑤,𝐵,𝑥,𝑦,𝑧   𝑤,𝑃   𝑥,𝑅,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧   𝑥,𝑇,𝑦,𝑧   𝑥,𝑈,𝑦,𝑧   𝑤,𝑊   𝑤,𝑋
Allowed substitution hints:   𝑃(𝑥,𝑦,𝑧)   𝑄(𝑥,𝑦,𝑧)   𝑅(𝑤)   𝑆(𝑤)   𝑇(𝑤)   𝑈(𝑤)   𝑂(𝑥,𝑦,𝑧)   𝑊(𝑥,𝑦,𝑧)   𝑋(𝑥,𝑦,𝑧)

Proof of Theorem ixxun
StepHypRef Expression
1 elun 3714 . . 3 (𝑤 ∈ ((𝐴𝑂𝐵) ∪ (𝐵𝑃𝐶)) ↔ (𝑤 ∈ (𝐴𝑂𝐵) ∨ 𝑤 ∈ (𝐵𝑃𝐶)))
2 simpl1 1056 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → 𝐴 ∈ ℝ*)
3 simpl2 1057 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → 𝐵 ∈ ℝ*)
4 ixx.1 . . . . . . . . . . 11 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})
54elixx1 12011 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑆𝐵)))
62, 3, 5syl2anc 690 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑆𝐵)))
76biimpa 499 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑆𝐵))
87simp1d 1065 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ∈ ℝ*)
97simp2d 1066 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴𝑅𝑤)
107simp3d 1067 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤𝑆𝐵)
11 simplrr 796 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐵𝑋𝐶)
123adantr 479 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐵 ∈ ℝ*)
13 simpl3 1058 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → 𝐶 ∈ ℝ*)
1413adantr 479 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐶 ∈ ℝ*)
15 ixxun.5 . . . . . . . . 9 ((𝑤 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝑤𝑆𝐵𝐵𝑋𝐶) → 𝑤𝑈𝐶))
168, 12, 14, 15syl3anc 1317 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → ((𝑤𝑆𝐵𝐵𝑋𝐶) → 𝑤𝑈𝐶))
1710, 11, 16mp2and 710 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤𝑈𝐶)
188, 9, 173jca 1234 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑈𝐶))
19 ixxun.2 . . . . . . . . . . 11 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑈𝑦)})
2019elixx1 12011 . . . . . . . . . 10 ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → (𝑤 ∈ (𝐵𝑃𝐶) ↔ (𝑤 ∈ ℝ*𝐵𝑇𝑤𝑤𝑈𝐶)))
213, 13, 20syl2anc 690 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → (𝑤 ∈ (𝐵𝑃𝐶) ↔ (𝑤 ∈ ℝ*𝐵𝑇𝑤𝑤𝑈𝐶)))
2221biimpa 499 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → (𝑤 ∈ ℝ*𝐵𝑇𝑤𝑤𝑈𝐶))
2322simp1d 1065 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝑤 ∈ ℝ*)
24 simplrl 795 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐴𝑊𝐵)
2522simp2d 1066 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐵𝑇𝑤)
262adantr 479 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐴 ∈ ℝ*)
273adantr 479 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐵 ∈ ℝ*)
28 ixxun.6 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵𝐵𝑇𝑤) → 𝐴𝑅𝑤))
2926, 27, 23, 28syl3anc 1317 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → ((𝐴𝑊𝐵𝐵𝑇𝑤) → 𝐴𝑅𝑤))
3024, 25, 29mp2and 710 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝐴𝑅𝑤)
3122simp3d 1067 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → 𝑤𝑈𝐶)
3223, 30, 313jca 1234 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐵𝑃𝐶)) → (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑈𝐶))
3318, 32jaodan 821 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ (𝑤 ∈ (𝐴𝑂𝐵) ∨ 𝑤 ∈ (𝐵𝑃𝐶))) → (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑈𝐶))
34 ixxun.4 . . . . . . . 8 𝑄 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑈𝑦)})
3534elixx1 12011 . . . . . . 7 ((𝐴 ∈ ℝ*𝐶 ∈ ℝ*) → (𝑤 ∈ (𝐴𝑄𝐶) ↔ (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑈𝐶)))
362, 13, 35syl2anc 690 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → (𝑤 ∈ (𝐴𝑄𝐶) ↔ (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑈𝐶)))
3736biimpar 500 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑈𝐶)) → 𝑤 ∈ (𝐴𝑄𝐶))
3833, 37syldan 485 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ (𝑤 ∈ (𝐴𝑂𝐵) ∨ 𝑤 ∈ (𝐵𝑃𝐶))) → 𝑤 ∈ (𝐴𝑄𝐶))
39 exmid 429 . . . . 5 (𝑤𝑆𝐵 ∨ ¬ 𝑤𝑆𝐵)
40 df-3an 1032 . . . . . . . . 9 ((𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑆𝐵) ↔ ((𝑤 ∈ ℝ*𝐴𝑅𝑤) ∧ 𝑤𝑆𝐵))
416, 40syl6bb 274 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ ((𝑤 ∈ ℝ*𝐴𝑅𝑤) ∧ 𝑤𝑆𝐵)))
4241adantr 479 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ ((𝑤 ∈ ℝ*𝐴𝑅𝑤) ∧ 𝑤𝑆𝐵)))
4336biimpa 499 . . . . . . . . . 10 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑈𝐶))
4443simp1d 1065 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → 𝑤 ∈ ℝ*)
4543simp2d 1066 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → 𝐴𝑅𝑤)
4644, 45jca 552 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝑤 ∈ ℝ*𝐴𝑅𝑤))
4746biantrurd 527 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝑤𝑆𝐵 ↔ ((𝑤 ∈ ℝ*𝐴𝑅𝑤) ∧ 𝑤𝑆𝐵)))
4842, 47bitr4d 269 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ 𝑤𝑆𝐵))
49 3anan12 1043 . . . . . . . . 9 ((𝑤 ∈ ℝ*𝐵𝑇𝑤𝑤𝑈𝐶) ↔ (𝐵𝑇𝑤 ∧ (𝑤 ∈ ℝ*𝑤𝑈𝐶)))
5021, 49syl6bb 274 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → (𝑤 ∈ (𝐵𝑃𝐶) ↔ (𝐵𝑇𝑤 ∧ (𝑤 ∈ ℝ*𝑤𝑈𝐶))))
5150adantr 479 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝑤 ∈ (𝐵𝑃𝐶) ↔ (𝐵𝑇𝑤 ∧ (𝑤 ∈ ℝ*𝑤𝑈𝐶))))
5243simp3d 1067 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → 𝑤𝑈𝐶)
5344, 52jca 552 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝑤 ∈ ℝ*𝑤𝑈𝐶))
5453biantrud 526 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝐵𝑇𝑤 ↔ (𝐵𝑇𝑤 ∧ (𝑤 ∈ ℝ*𝑤𝑈𝐶))))
553adantr 479 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → 𝐵 ∈ ℝ*)
56 ixxun.3 . . . . . . . 8 ((𝐵 ∈ ℝ*𝑤 ∈ ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵))
5755, 44, 56syl2anc 690 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵))
5851, 54, 573bitr2d 294 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝑤 ∈ (𝐵𝑃𝐶) ↔ ¬ 𝑤𝑆𝐵))
5948, 58orbi12d 741 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → ((𝑤 ∈ (𝐴𝑂𝐵) ∨ 𝑤 ∈ (𝐵𝑃𝐶)) ↔ (𝑤𝑆𝐵 ∨ ¬ 𝑤𝑆𝐵)))
6039, 59mpbiri 246 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) ∧ 𝑤 ∈ (𝐴𝑄𝐶)) → (𝑤 ∈ (𝐴𝑂𝐵) ∨ 𝑤 ∈ (𝐵𝑃𝐶)))
6138, 60impbida 872 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → ((𝑤 ∈ (𝐴𝑂𝐵) ∨ 𝑤 ∈ (𝐵𝑃𝐶)) ↔ 𝑤 ∈ (𝐴𝑄𝐶)))
621, 61syl5bb 270 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → (𝑤 ∈ ((𝐴𝑂𝐵) ∪ (𝐵𝑃𝐶)) ↔ 𝑤 ∈ (𝐴𝑄𝐶)))
6362eqrdv 2607 1 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵𝐵𝑋𝐶)) → ((𝐴𝑂𝐵) ∪ (𝐵𝑃𝐶)) = (𝐴𝑄𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  {crab 2899  cun 3537   class class class wbr 4577  (class class class)co 6527  cmpt2 6529  *cxr 9929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-iota 5754  df-fun 5792  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-xr 9934
This theorem is referenced by:  icoun  12123  snunioo  12125  snunico  12126  snunioc  12127  ioojoin  12130  leordtval2  20768  lecldbas  20775  icopnfcld  22313  iocmnfcld  22314  ioombl  23057  ismbf3d  23144  joiniooico  28732  asindmre  32468  ioounsn  36617  snunioo2  38382  snunioo1  38389
  Copyright terms: Public domain W3C validator