Users' Mathboxes 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 43190
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 3721 . . 3 (∃!𝑏𝑉 𝜑 ↔ ∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)))
32reubii 3389 . 2 (∃!𝑎𝑉 ∃!𝑏𝑉 𝜑 ↔ ∃!𝑎𝑉𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)))
4 2reuimp.d . . . . . 6 (𝑎 = 𝑑 → (𝜑𝜒))
5 2reuimp.a . . . . . . . 8 (𝑎 = 𝑑 → (𝜃𝜏))
65imbi1d 343 . . . . . . 7 (𝑎 = 𝑑 → ((𝜃𝑏 = 𝑐) ↔ (𝜏𝑏 = 𝑐)))
76ralbidv 3194 . . . . . 6 (𝑎 = 𝑑 → (∀𝑐𝑉 (𝜃𝑏 = 𝑐) ↔ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)))
84, 7anbi12d 630 . . . . 5 (𝑎 = 𝑑 → ((𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐))))
98rexbidv 3294 . . . 4 (𝑎 = 𝑑 → (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ ∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐))))
109reu8 3721 . . 3 (∃!𝑎𝑉𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ ∃𝑎𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
11 r19.28v 3183 . . . . 5 ((∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
12 2reuimp.e . . . . . . . . . 10 (𝑏 = 𝑒 → (𝜑𝜂))
13 equequ1 2023 . . . . . . . . . . . 12 (𝑏 = 𝑒 → (𝑏 = 𝑐𝑒 = 𝑐))
1413imbi2d 342 . . . . . . . . . . 11 (𝑏 = 𝑒 → ((𝜃𝑏 = 𝑐) ↔ (𝜃𝑒 = 𝑐)))
1514ralbidv 3194 . . . . . . . . . 10 (𝑏 = 𝑒 → (∀𝑐𝑉 (𝜃𝑏 = 𝑐) ↔ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)))
1612, 15anbi12d 630 . . . . . . . . 9 (𝑏 = 𝑒 → ((𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
1716cbvrexvw 3448 . . . . . . . 8 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ ∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)))
18 r19.23v 3276 . . . . . . . . 9 (∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ↔ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑))
19 r19.28v 3183 . . . . . . . . . . 11 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
20 ancom 461 . . . . . . . . . . . . . 14 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ ∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
21 r19.42v 3347 . . . . . . . . . . . . . 14 (∃𝑒𝑉 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))) ↔ (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ ∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
2220, 21bitr4i 279 . . . . . . . . . . . . 13 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ ∃𝑒𝑉 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
23 2reuimp.f . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑓 → (𝜃𝜓))
24 equequ2 2024 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑓 → (𝑒 = 𝑐𝑒 = 𝑓))
2523, 24imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑓 → ((𝜃𝑒 = 𝑐) ↔ (𝜓𝑒 = 𝑓)))
2625cbvralvw 3447 . . . . . . . . . . . . . . . 16 (∀𝑐𝑉 (𝜃𝑒 = 𝑐) ↔ ∀𝑓𝑉 (𝜓𝑒 = 𝑓))
27 r19.28v 3183 . . . . . . . . . . . . . . . . . 18 (((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ ∀𝑓𝑉 (𝜓𝑒 = 𝑓)) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
2827ex 413 . . . . . . . . . . . . . . . . 17 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → (∀𝑓𝑉 (𝜓𝑒 = 𝑓) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
2928expcom 414 . . . . . . . . . . . . . . . 16 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → (∀𝑓𝑉 (𝜓𝑒 = 𝑓) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))))
3026, 29syl7bi 256 . . . . . . . . . . . . . . 15 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → (∀𝑐𝑉 (𝜃𝑒 = 𝑐) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))))
3130imp32 419 . . . . . . . . . . . . . 14 ((((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3231reximi 3240 . . . . . . . . . . . . 13 (∃𝑒𝑉 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))) → ∃𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3322, 32sylbi 218 . . . . . . . . . . . 12 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3433ralimi 3157 . . . . . . . . . . 11 (∀𝑏𝑉 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3519, 34syl 17 . . . . . . . . . 10 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3635ex 413 . . . . . . . . 9 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) → (∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
3718, 36syl5bir 244 . . . . . . . 8 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) → ((∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
3817, 37sylbi 218 . . . . . . 7 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) → ((∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
3938imp 407 . . . . . 6 ((∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4039ralimi 3157 . . . . 5 (∀𝑑𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4111, 40syl 17 . . . 4 ((∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4241reximi 3240 . . 3 (∃𝑎𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4310, 42sylbi 218 . 2 (∃!𝑎𝑉𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
443, 43sylbi 218 1 (∃!𝑎𝑉 ∃!𝑏𝑉 𝜑 → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wral 3135  wrex 3136  ∃!wreu 3137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-10 2136  ax-11 2151  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clel 2890  df-ral 3140  df-rex 3141  df-reu 3142
This theorem is referenced by:  2reuimp  43191
  Copyright terms: Public domain W3C validator