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

Theorem 2reuimp0 42665
 Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification. The involved wffs depend on the setvar variables as follows: ph(a,b), th(a,c), ch(d,b), ta(d,c), et(a,e), ps(a,f) (Contributed by AV, 13-Mar-2023.)
Hypotheses
Ref Expression
2reuimp.c (𝑏 = 𝑐 → (𝜑𝜃))
2reuimp.d (𝑎 = 𝑑 → (𝜑𝜒))
2reuimp.a (𝑎 = 𝑑 → (𝜃𝜏))
2reuimp.e (𝑏 = 𝑒 → (𝜑𝜂))
2reuimp.f (𝑐 = 𝑓 → (𝜃𝜓))
Assertion
Ref Expression
2reuimp0 (∃!𝑎𝑉 ∃!𝑏𝑉 𝜑 → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
Distinct variable groups:   𝑉,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝜑,𝑐,𝑑,𝑒   𝜃,𝑏,𝑑,𝑒,𝑓   𝜒,𝑎,𝑒,𝑓   𝜏,𝑎,𝑒,𝑓   𝜂,𝑏,𝑓   𝜓,𝑐
Allowed substitution hints:   𝜑(𝑓,𝑎,𝑏)   𝜓(𝑒,𝑓,𝑎,𝑏,𝑑)   𝜒(𝑏,𝑐,𝑑)   𝜃(𝑎,𝑐)   𝜏(𝑏,𝑐,𝑑)   𝜂(𝑒,𝑎,𝑐,𝑑)

Proof of Theorem 2reuimp0
StepHypRef Expression
1 2reuimp.c . . . 4 (𝑏 = 𝑐 → (𝜑𝜃))
21reu8 3632 . . 3 (∃!𝑏𝑉 𝜑 ↔ ∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)))
32reubii 3325 . 2 (∃!𝑎𝑉 ∃!𝑏𝑉 𝜑 ↔ ∃!𝑎𝑉𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)))
4 2reuimp.d . . . . . 6 (𝑎 = 𝑑 → (𝜑𝜒))
5 2reuimp.a . . . . . . . 8 (𝑎 = 𝑑 → (𝜃𝜏))
65imbi1d 334 . . . . . . 7 (𝑎 = 𝑑 → ((𝜃𝑏 = 𝑐) ↔ (𝜏𝑏 = 𝑐)))
76ralbidv 3141 . . . . . 6 (𝑎 = 𝑑 → (∀𝑐𝑉 (𝜃𝑏 = 𝑐) ↔ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)))
84, 7anbi12d 621 . . . . 5 (𝑎 = 𝑑 → ((𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐))))
98rexbidv 3236 . . . 4 (𝑎 = 𝑑 → (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ ∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐))))
109reu8 3632 . . 3 (∃!𝑎𝑉𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ ∃𝑎𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
11 r19.28v 3130 . . . . 5 ((∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
12 2reuimp.e . . . . . . . . . 10 (𝑏 = 𝑒 → (𝜑𝜂))
13 equequ1 1981 . . . . . . . . . . . 12 (𝑏 = 𝑒 → (𝑏 = 𝑐𝑒 = 𝑐))
1413imbi2d 333 . . . . . . . . . . 11 (𝑏 = 𝑒 → ((𝜃𝑏 = 𝑐) ↔ (𝜃𝑒 = 𝑐)))
1514ralbidv 3141 . . . . . . . . . 10 (𝑏 = 𝑒 → (∀𝑐𝑉 (𝜃𝑏 = 𝑐) ↔ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)))
1612, 15anbi12d 621 . . . . . . . . 9 (𝑏 = 𝑒 → ((𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
1716cbvrexv 3378 . . . . . . . 8 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ ∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)))
18 r19.23v 3218 . . . . . . . . 9 (∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ↔ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑))
19 r19.28v 3130 . . . . . . . . . . 11 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
20 ancom 453 . . . . . . . . . . . . . 14 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ ∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
21 r19.42v 3285 . . . . . . . . . . . . . 14 (∃𝑒𝑉 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))) ↔ (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ ∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
2220, 21bitr4i 270 . . . . . . . . . . . . 13 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ ∃𝑒𝑉 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
23 2reuimp.f . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑓 → (𝜃𝜓))
24 equequ2 1982 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑓 → (𝑒 = 𝑐𝑒 = 𝑓))
2523, 24imbi12d 337 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑓 → ((𝜃𝑒 = 𝑐) ↔ (𝜓𝑒 = 𝑓)))
2625cbvralv 3377 . . . . . . . . . . . . . . . 16 (∀𝑐𝑉 (𝜃𝑒 = 𝑐) ↔ ∀𝑓𝑉 (𝜓𝑒 = 𝑓))
27 r19.28v 3130 . . . . . . . . . . . . . . . . . 18 (((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ ∀𝑓𝑉 (𝜓𝑒 = 𝑓)) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
2827ex 405 . . . . . . . . . . . . . . . . 17 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → (∀𝑓𝑉 (𝜓𝑒 = 𝑓) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
2928expcom 406 . . . . . . . . . . . . . . . 16 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → (∀𝑓𝑉 (𝜓𝑒 = 𝑓) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))))
3026, 29syl7bi 247 . . . . . . . . . . . . . . 15 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → (∀𝑐𝑉 (𝜃𝑒 = 𝑐) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))))
3130imp32 411 . . . . . . . . . . . . . 14 ((((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3231reximi 3184 . . . . . . . . . . . . 13 (∃𝑒𝑉 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))) → ∃𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3322, 32sylbi 209 . . . . . . . . . . . 12 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3433ralimi 3104 . . . . . . . . . . 11 (∀𝑏𝑉 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3519, 34syl 17 . . . . . . . . . 10 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3635ex 405 . . . . . . . . 9 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) → (∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
3718, 36syl5bir 235 . . . . . . . 8 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) → ((∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
3817, 37sylbi 209 . . . . . . 7 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) → ((∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
3938imp 398 . . . . . 6 ((∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4039ralimi 3104 . . . . 5 (∀𝑑𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4111, 40syl 17 . . . 4 ((∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4241reximi 3184 . . 3 (∃𝑎𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4310, 42sylbi 209 . 2 (∃!𝑎𝑉𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
443, 43sylbi 209 1 (∃!𝑎𝑉 ∃!𝑏𝑉 𝜑 → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387  ∀wral 3082  ∃wrex 3083  ∃!wreu 3084 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-reu 3089 This theorem is referenced by:  2reuimp  42666
 Copyright terms: Public domain W3C validator