Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  constrsuc Structured version   Visualization version   GIF version

Theorem constrsuc 33743
Description: Membership in the successor step of the construction of constructible numbers. (Contributed by Thierry Arnoux, 25-Jun-2025.)
Hypotheses
Ref Expression
constr0.1 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})
constrsuc.1 (𝜑𝑁 ∈ On)
constrsuc.2 𝑆 = (𝐶𝑁)
Assertion
Ref Expression
constrsuc (𝜑 → (𝑋 ∈ (𝐶‘suc 𝑁) ↔ (𝑋 ∈ ℂ ∧ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓)))))))
Distinct variable groups:   𝑆,𝑎,𝑠,𝑥   𝑆,𝑏,𝑠,𝑥   𝑆,𝑐,𝑠,𝑥   𝑆,𝑑,𝑠,𝑥   𝑆,𝑒,𝑠,𝑥   𝑆,𝑓,𝑠,𝑥   𝑋,𝑎   𝑋,𝑏   𝑋,𝑐   𝑋,𝑑   𝑒,𝑋   𝑓,𝑋   𝑋,𝑟   𝑡,𝑋   𝜑,𝑠   𝑠,𝑟,𝑥   𝑡,𝑠,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑡,𝑒,𝑓,𝑟,𝑎,𝑏,𝑐,𝑑)   𝐶(𝑥,𝑡,𝑒,𝑓,𝑠,𝑟,𝑎,𝑏,𝑐,𝑑)   𝑆(𝑡,𝑟)   𝑁(𝑥,𝑡,𝑒,𝑓,𝑠,𝑟,𝑎,𝑏,𝑐,𝑑)   𝑋(𝑥,𝑠)

Proof of Theorem constrsuc
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 constr0.1 . . . . . 6 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})
21fveq1i 6908 . . . . 5 (𝐶‘suc 𝑁) = (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})‘suc 𝑁)
3 constrsuc.1 . . . . . 6 (𝜑𝑁 ∈ On)
4 rdgsuc 8463 . . . . . 6 (𝑁 ∈ On → (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})‘suc 𝑁) = ((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})‘(rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})‘𝑁)))
53, 4syl 17 . . . . 5 (𝜑 → (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})‘suc 𝑁) = ((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})‘(rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})‘𝑁)))
62, 5eqtrid 2787 . . . 4 (𝜑 → (𝐶‘suc 𝑁) = ((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})‘(rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})‘𝑁)))
7 constrsuc.2 . . . . . 6 𝑆 = (𝐶𝑁)
81fveq1i 6908 . . . . . 6 (𝐶𝑁) = (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})‘𝑁)
97, 8eqtri 2763 . . . . 5 𝑆 = (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})‘𝑁)
109fveq2i 6910 . . . 4 ((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})‘𝑆) = ((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})‘(rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})‘𝑁))
116, 10eqtr4di 2793 . . 3 (𝜑 → (𝐶‘suc 𝑁) = ((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})‘𝑆))
1211eleq2d 2825 . 2 (𝜑 → (𝑋 ∈ (𝐶‘suc 𝑁) ↔ 𝑋 ∈ ((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})‘𝑆)))
13 eqid 2735 . . . 4 (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}) = (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})
14 id 22 . . . . . . . 8 (𝑠 = 𝑆𝑠 = 𝑆)
15 rexeq 3320 . . . . . . . . . 10 (𝑠 = 𝑆 → (∃𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ ∃𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
1614, 15rexeqbidv 3345 . . . . . . . . 9 (𝑠 = 𝑆 → (∃𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ ∃𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
1714, 16rexeqbidv 3345 . . . . . . . 8 (𝑠 = 𝑆 → (∃𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ ∃𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
1814, 17rexeqbidv 3345 . . . . . . 7 (𝑠 = 𝑆 → (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
19 rexeq 3320 . . . . . . . . . . 11 (𝑠 = 𝑆 → (∃𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))))
2014, 19rexeqbidv 3345 . . . . . . . . . 10 (𝑠 = 𝑆 → (∃𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))))
2114, 20rexeqbidv 3345 . . . . . . . . 9 (𝑠 = 𝑆 → (∃𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))))
2214, 21rexeqbidv 3345 . . . . . . . 8 (𝑠 = 𝑆 → (∃𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))))
2314, 22rexeqbidvv 3334 . . . . . . 7 (𝑠 = 𝑆 → (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))))
24 rexeq 3320 . . . . . . . . . . . 12 (𝑠 = 𝑆 → (∃𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))))
2514, 24rexeqbidv 3345 . . . . . . . . . . 11 (𝑠 = 𝑆 → (∃𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))))
2614, 25rexeqbidv 3345 . . . . . . . . . 10 (𝑠 = 𝑆 → (∃𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))))
2714, 26rexeqbidv 3345 . . . . . . . . 9 (𝑠 = 𝑆 → (∃𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))))
2814, 27rexeqbidv 3345 . . . . . . . 8 (𝑠 = 𝑆 → (∃𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))))
2914, 28rexeqbidvv 3334 . . . . . . 7 (𝑠 = 𝑆 → (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))))
3018, 23, 293orbi123d 1434 . . . . . 6 (𝑠 = 𝑆 → ((∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))) ↔ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))))
3130rabbidv 3441 . . . . 5 (𝑠 = 𝑆 → {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))} = {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})
3231adantl 481 . . . 4 ((𝜑𝑠 = 𝑆) → {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))} = {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})
337fvexi 6921 . . . . 5 𝑆 ∈ V
3433a1i 11 . . . 4 (𝜑𝑆 ∈ V)
35 cnex 11234 . . . . . 6 ℂ ∈ V
36 ssrab2 4090 . . . . . 6 {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))} ⊆ ℂ
3735, 36ssexi 5328 . . . . 5 {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))} ∈ V
3837a1i 11 . . . 4 (𝜑 → {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))} ∈ V)
3913, 32, 34, 38fvmptd2 7024 . . 3 (𝜑 → ((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})‘𝑆) = {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})
4039eleq2d 2825 . 2 (𝜑 → (𝑋 ∈ ((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})‘𝑆) ↔ 𝑋 ∈ {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}))
41 eqeq1 2739 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ↔ 𝑦 = (𝑎 + (𝑡 · (𝑏𝑎)))))
42 eqeq1 2739 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ↔ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐)))))
4341, 423anbi12d 1436 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
44432rexbidv 3220 . . . . . . . . 9 (𝑥 = 𝑦 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
45442rexbidv 3220 . . . . . . . 8 (𝑥 = 𝑦 → (∃𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ ∃𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
46452rexbidv 3220 . . . . . . 7 (𝑥 = 𝑦 → (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
47 fvoveq1 7454 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (abs‘(𝑥𝑐)) = (abs‘(𝑦𝑐)))
4847eqeq1d 2737 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)) ↔ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓))))
4941, 48anbi12d 632 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ↔ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓)))))
50492rexbidv 3220 . . . . . . . . 9 (𝑥 = 𝑦 → (∃𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓)))))
51502rexbidv 3220 . . . . . . . 8 (𝑥 = 𝑦 → (∃𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓)))))
52512rexbidv 3220 . . . . . . 7 (𝑥 = 𝑦 → (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓)))))
53 fvoveq1 7454 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (abs‘(𝑥𝑎)) = (abs‘(𝑦𝑎)))
5453eqeq1d 2737 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ↔ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐))))
55 fvoveq1 7454 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (abs‘(𝑥𝑑)) = (abs‘(𝑦𝑑)))
5655eqeq1d 2737 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)) ↔ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓))))
5754, 563anbi23d 1438 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))) ↔ (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓)))))
58572rexbidv 3220 . . . . . . . . 9 (𝑥 = 𝑦 → (∃𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓)))))
59582rexbidv 3220 . . . . . . . 8 (𝑥 = 𝑦 → (∃𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓)))))
60592rexbidv 3220 . . . . . . 7 (𝑥 = 𝑦 → (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓)))))
6146, 52, 603orbi123d 1434 . . . . . 6 (𝑥 = 𝑦 → ((∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))) ↔ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓))))))
6261cbvrabv 3444 . . . . 5 {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))} = {𝑦 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓))))}
6362eleq2i 2831 . . . 4 (𝑋 ∈ {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))} ↔ 𝑋 ∈ {𝑦 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓))))})
64 eqeq1 2739 . . . . . . . . . 10 (𝑦 = 𝑋 → (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ↔ 𝑋 = (𝑎 + (𝑡 · (𝑏𝑎)))))
65 eqeq1 2739 . . . . . . . . . 10 (𝑦 = 𝑋 → (𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ↔ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐)))))
6664, 653anbi12d 1436 . . . . . . . . 9 (𝑦 = 𝑋 → ((𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
67662rexbidv 3220 . . . . . . . 8 (𝑦 = 𝑋 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
68672rexbidv 3220 . . . . . . 7 (𝑦 = 𝑋 → (∃𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ ∃𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
69682rexbidv 3220 . . . . . 6 (𝑦 = 𝑋 → (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ↔ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)))
70 fvoveq1 7454 . . . . . . . . . . 11 (𝑦 = 𝑋 → (abs‘(𝑦𝑐)) = (abs‘(𝑋𝑐)))
7170eqeq1d 2737 . . . . . . . . . 10 (𝑦 = 𝑋 → ((abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓)) ↔ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓))))
7264, 71anbi12d 632 . . . . . . . . 9 (𝑦 = 𝑋 → ((𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓))) ↔ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓)))))
73722rexbidv 3220 . . . . . . . 8 (𝑦 = 𝑋 → (∃𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑓𝑆𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓)))))
74732rexbidv 3220 . . . . . . 7 (𝑦 = 𝑋 → (∃𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓)))))
75742rexbidv 3220 . . . . . 6 (𝑦 = 𝑋 → (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓))) ↔ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓)))))
76 fvoveq1 7454 . . . . . . . . . . 11 (𝑦 = 𝑋 → (abs‘(𝑦𝑎)) = (abs‘(𝑋𝑎)))
7776eqeq1d 2737 . . . . . . . . . 10 (𝑦 = 𝑋 → ((abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ↔ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐))))
78 fvoveq1 7454 . . . . . . . . . . 11 (𝑦 = 𝑋 → (abs‘(𝑦𝑑)) = (abs‘(𝑋𝑑)))
7978eqeq1d 2737 . . . . . . . . . 10 (𝑦 = 𝑋 → ((abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓)) ↔ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓))))
8077, 793anbi23d 1438 . . . . . . . . 9 (𝑦 = 𝑋 → ((𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓))) ↔ (𝑎𝑑 ∧ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓)))))
81802rexbidv 3220 . . . . . . . 8 (𝑦 = 𝑋 → (∃𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓)))))
82812rexbidv 3220 . . . . . . 7 (𝑦 = 𝑋 → (∃𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓)))))
83822rexbidv 3220 . . . . . 6 (𝑦 = 𝑋 → (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓))) ↔ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓)))))
8469, 75, 833orbi123d 1434 . . . . 5 (𝑦 = 𝑋 → ((∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓)))) ↔ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓))))))
8584elrab 3695 . . . 4 (𝑋 ∈ {𝑦 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑦𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑦𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑦𝑑)) = (abs‘(𝑒𝑓))))} ↔ (𝑋 ∈ ℂ ∧ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓))))))
8663, 85bitri 275 . . 3 (𝑋 ∈ {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))} ↔ (𝑋 ∈ ℂ ∧ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓))))))
8786a1i 11 . 2 (𝜑 → (𝑋 ∈ {𝑥 ∈ ℂ ∣ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))} ↔ (𝑋 ∈ ℂ ∧ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓)))))))
8812, 40, 873bitrd 305 1 (𝜑 → (𝑋 ∈ (𝐶‘suc 𝑁) ↔ (𝑋 ∈ ℂ ∧ (∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑒𝑆𝑓𝑆𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑋𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑆𝑏𝑆𝑐𝑆𝑑𝑆𝑒𝑆𝑓𝑆 (𝑎𝑑 ∧ (abs‘(𝑋𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑋𝑑)) = (abs‘(𝑒𝑓)))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3o 1085  w3a 1086   = wceq 1537  wcel 2106  wne 2938  wrex 3068  {crab 3433  Vcvv 3478  {cpr 4633  cmpt 5231  Oncon0 6386  suc csuc 6388  cfv 6563  (class class class)co 7431  reccrdg 8448  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156   · cmul 11158  cmin 11490  ccj 15132  cim 15134  abscabs 15270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754  ax-cnex 11209
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449
This theorem is referenced by:  constrsscn  33745  constrsslem  33746  constrconj  33750  constrfin  33751  constrelextdg2  33752
  Copyright terms: Public domain W3C validator