Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2reuimp Structured version   Visualization version   GIF version

Theorem 2reuimp 43597
 Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification if the class of the quantified elements is not empty. (Contributed by AV, 13-Mar-2023.)
Hypotheses
Ref Expression
2reuimp.c (𝑏 = 𝑐 → (𝜑𝜃))
2reuimp.d (𝑎 = 𝑑 → (𝜑𝜒))
2reuimp.a (𝑎 = 𝑑 → (𝜃𝜏))
2reuimp.e (𝑏 = 𝑒 → (𝜑𝜂))
2reuimp.f (𝑐 = 𝑓 → (𝜃𝜓))
Assertion
Ref Expression
2reuimp ((𝑉 ≠ ∅ ∧ ∃!𝑎𝑉 ∃!𝑏𝑉 𝜑) → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓)))))
Distinct variable groups:   𝑉,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝜑,𝑐,𝑑,𝑒   𝜃,𝑏,𝑑,𝑒,𝑓   𝜒,𝑎,𝑒,𝑓   𝜏,𝑎,𝑒,𝑓   𝜂,𝑏,𝑓   𝜓,𝑐   𝜒,𝑐   𝜂,𝑐
Allowed substitution hints:   𝜑(𝑓,𝑎,𝑏)   𝜓(𝑒,𝑓,𝑎,𝑏,𝑑)   𝜒(𝑏,𝑑)   𝜃(𝑎,𝑐)   𝜏(𝑏,𝑐,𝑑)   𝜂(𝑒,𝑎,𝑑)

Proof of Theorem 2reuimp
StepHypRef Expression
1 r19.28zv 4429 . . . . . . . . . . . 12 (𝑉 ≠ ∅ → (∀𝑐𝑉 (𝜒 ∧ (𝜏𝑏 = 𝑐)) ↔ (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐))))
21bicomd 226 . . . . . . . . . . 11 (𝑉 ≠ ∅ → ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) ↔ ∀𝑐𝑉 (𝜒 ∧ (𝜏𝑏 = 𝑐))))
32imbi1d 345 . . . . . . . . . 10 (𝑉 ≠ ∅ → (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ↔ (∀𝑐𝑉 (𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
4 r19.36zv 4435 . . . . . . . . . . 11 (𝑉 ≠ ∅ → (∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ↔ (∀𝑐𝑉 (𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
5 r19.42v 3341 . . . . . . . . . . . . . 14 (∃𝑐𝑉 ((𝜂 ∧ (𝜓𝑒 = 𝑓)) ∧ ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ ((𝜂 ∧ (𝜓𝑒 = 𝑓)) ∧ ∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
6 pm5.31r 830 . . . . . . . . . . . . . . . 16 ((𝜂 ∧ (𝜓𝑒 = 𝑓)) → (𝜓 → (𝜂𝑒 = 𝑓)))
7 pm5.31r 830 . . . . . . . . . . . . . . . . 17 (((𝜓 → (𝜂𝑒 = 𝑓)) ∧ ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → ((𝜓 → (𝜂𝑒 = 𝑓)) ∧ 𝑎 = 𝑑)))
8 pm5.31r 830 . . . . . . . . . . . . . . . . . . 19 ((𝑎 = 𝑑 ∧ (𝜓 → (𝜂𝑒 = 𝑓))) → (𝜓 → (𝑎 = 𝑑 ∧ (𝜂𝑒 = 𝑓))))
9 an12 644 . . . . . . . . . . . . . . . . . . 19 ((𝑎 = 𝑑 ∧ (𝜂𝑒 = 𝑓)) ↔ (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓)))
108, 9syl6ib 254 . . . . . . . . . . . . . . . . . 18 ((𝑎 = 𝑑 ∧ (𝜓 → (𝜂𝑒 = 𝑓))) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))
1110ancoms 462 . . . . . . . . . . . . . . . . 17 (((𝜓 → (𝜂𝑒 = 𝑓)) ∧ 𝑎 = 𝑑) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))
127, 11syl6 35 . . . . . . . . . . . . . . . 16 (((𝜓 → (𝜂𝑒 = 𝑓)) ∧ ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓)))))
136, 12sylan 583 . . . . . . . . . . . . . . 15 (((𝜂 ∧ (𝜓𝑒 = 𝑓)) ∧ ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓)))))
1413reximi 3237 . . . . . . . . . . . . . 14 (∃𝑐𝑉 ((𝜂 ∧ (𝜓𝑒 = 𝑓)) ∧ ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓)))))
155, 14sylbir 238 . . . . . . . . . . . . 13 (((𝜂 ∧ (𝜓𝑒 = 𝑓)) ∧ ∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓)))))
1615expcom 417 . . . . . . . . . . . 12 (∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ((𝜂 ∧ (𝜓𝑒 = 𝑓)) → ∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))))
1716expd 419 . . . . . . . . . . 11 (∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → ((𝜓𝑒 = 𝑓) → ∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓)))))))
184, 17syl6bir 257 . . . . . . . . . 10 (𝑉 ≠ ∅ → ((∀𝑐𝑉 (𝜒 ∧ (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → ((𝜓𝑒 = 𝑓) → ∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))))))
193, 18sylbid 243 . . . . . . . . 9 (𝑉 ≠ ∅ → (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → ((𝜓𝑒 = 𝑓) → ∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))))))
2019com23 86 . . . . . . . 8 (𝑉 ≠ ∅ → (𝜂 → (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ((𝜓𝑒 = 𝑓) → ∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))))))
2120imp4c 427 . . . . . . 7 (𝑉 ≠ ∅ → (((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)) → ∃𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))))
2221ralimdv 3173 . . . . . 6 (𝑉 ≠ ∅ → (∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)) → ∀𝑓𝑉𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))))
2322reximdv 3265 . . . . 5 (𝑉 ≠ ∅ → (∃𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)) → ∃𝑒𝑉𝑓𝑉𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))))
2423ralimdv 3173 . . . 4 (𝑉 ≠ ∅ → (∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)) → ∀𝑏𝑉𝑒𝑉𝑓𝑉𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))))
2524ralimdv 3173 . . 3 (𝑉 ≠ ∅ → (∀𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)) → ∀𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))))
2625reximdv 3265 . 2 (𝑉 ≠ ∅ → (∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)) → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓))))))
27 2reuimp.c . . 3 (𝑏 = 𝑐 → (𝜑𝜃))
28 2reuimp.d . . 3 (𝑎 = 𝑑 → (𝜑𝜒))
29 2reuimp.a . . 3 (𝑎 = 𝑑 → (𝜃𝜏))
30 2reuimp.e . . 3 (𝑏 = 𝑒 → (𝜑𝜂))
31 2reuimp.f . . 3 (𝑐 = 𝑓 → (𝜃𝜓))
3227, 28, 29, 30, 312reuimp0 43596 . 2 (∃!𝑎𝑉 ∃!𝑏𝑉 𝜑 → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3326, 32impel 509 1 ((𝑉 ≠ ∅ ∧ ∃!𝑎𝑉 ∃!𝑏𝑉 𝜑) → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉𝑐𝑉 ((𝜒 ∧ (𝜏𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑𝑒 = 𝑓)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  ∃!wreu 3135  ∅c0 4276 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-dif 3922  df-nul 4277 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator