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 43609
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 3699 . . 3 (∃!𝑏𝑉 𝜑 ↔ ∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)))
32reubii 3372 . 2 (∃!𝑎𝑉 ∃!𝑏𝑉 𝜑 ↔ ∃!𝑎𝑉𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)))
4 2reuimp.d . . . . . 6 (𝑎 = 𝑑 → (𝜑𝜒))
5 2reuimp.a . . . . . . . 8 (𝑎 = 𝑑 → (𝜃𝜏))
65imbi1d 345 . . . . . . 7 (𝑎 = 𝑑 → ((𝜃𝑏 = 𝑐) ↔ (𝜏𝑏 = 𝑐)))
76ralbidv 3187 . . . . . 6 (𝑎 = 𝑑 → (∀𝑐𝑉 (𝜃𝑏 = 𝑐) ↔ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)))
84, 7anbi12d 633 . . . . 5 (𝑎 = 𝑑 → ((𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐))))
98rexbidv 3283 . . . 4 (𝑎 = 𝑑 → (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ ∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐))))
109reu8 3699 . . 3 (∃!𝑎𝑉𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ ∃𝑎𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
11 r19.28v 3177 . . . . 5 ((∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
12 2reuimp.e . . . . . . . . . 10 (𝑏 = 𝑒 → (𝜑𝜂))
13 equequ1 2032 . . . . . . . . . . . 12 (𝑏 = 𝑒 → (𝑏 = 𝑐𝑒 = 𝑐))
1413imbi2d 344 . . . . . . . . . . 11 (𝑏 = 𝑒 → ((𝜃𝑏 = 𝑐) ↔ (𝜃𝑒 = 𝑐)))
1514ralbidv 3187 . . . . . . . . . 10 (𝑏 = 𝑒 → (∀𝑐𝑉 (𝜃𝑏 = 𝑐) ↔ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)))
1612, 15anbi12d 633 . . . . . . . . 9 (𝑏 = 𝑒 → ((𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
1716cbvrexvw 3425 . . . . . . . 8 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ↔ ∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)))
18 r19.23v 3265 . . . . . . . . 9 (∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ↔ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑))
19 r19.28v 3177 . . . . . . . . . . 11 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)))
20 ancom 464 . . . . . . . . . . . . . 14 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ ∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
21 r19.42v 3331 . . . . . . . . . . . . . 14 (∃𝑒𝑉 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))) ↔ (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ ∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
2220, 21bitr4i 281 . . . . . . . . . . . . 13 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ ∃𝑒𝑉 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))))
23 2reuimp.f . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑓 → (𝜃𝜓))
24 equequ2 2033 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑓 → (𝑒 = 𝑐𝑒 = 𝑓))
2523, 24imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑓 → ((𝜃𝑒 = 𝑐) ↔ (𝜓𝑒 = 𝑓)))
2625cbvralvw 3424 . . . . . . . . . . . . . . . 16 (∀𝑐𝑉 (𝜃𝑒 = 𝑐) ↔ ∀𝑓𝑉 (𝜓𝑒 = 𝑓))
27 r19.28v 3177 . . . . . . . . . . . . . . . . . 18 (((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ ∀𝑓𝑉 (𝜓𝑒 = 𝑓)) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
2827ex 416 . . . . . . . . . . . . . . . . 17 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → (∀𝑓𝑉 (𝜓𝑒 = 𝑓) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
2928expcom 417 . . . . . . . . . . . . . . . 16 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → (∀𝑓𝑉 (𝜓𝑒 = 𝑓) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))))
3026, 29syl7bi 258 . . . . . . . . . . . . . . 15 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → (∀𝑐𝑉 (𝜃𝑒 = 𝑐) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))))
3130imp32 422 . . . . . . . . . . . . . 14 ((((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))) → ∀𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3231reximi 3231 . . . . . . . . . . . . 13 (∃𝑒𝑉 (((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐))) → ∃𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3322, 32sylbi 220 . . . . . . . . . . . 12 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3433ralimi 3152 . . . . . . . . . . 11 (∀𝑏𝑉 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3519, 34syl 17 . . . . . . . . . 10 ((∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) ∧ ∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
3635ex 416 . . . . . . . . 9 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) → (∀𝑏𝑉 ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
3718, 36syl5bir 246 . . . . . . . 8 (∃𝑒𝑉 (𝜂 ∧ ∀𝑐𝑉 (𝜃𝑒 = 𝑐)) → ((∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
3817, 37sylbi 220 . . . . . . 7 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) → ((∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓))))
3938imp 410 . . . . . 6 ((∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4039ralimi 3152 . . . . 5 (∀𝑑𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4111, 40syl 17 . . . 4 ((∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4241reximi 3231 . . 3 (∃𝑎𝑉 (∃𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) ∧ ∀𝑑𝑉 (∃𝑏𝑉 (𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
4310, 42sylbi 220 . 2 (∃!𝑎𝑉𝑏𝑉 (𝜑 ∧ ∀𝑐𝑉 (𝜃𝑏 = 𝑐)) → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
443, 43sylbi 220 1 (∃!𝑎𝑉 ∃!𝑏𝑉 𝜑 → ∃𝑎𝑉𝑑𝑉𝑏𝑉𝑒𝑉𝑓𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐𝑉 (𝜏𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓𝑒 = 𝑓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wral 3130  wrex 3131  ∃!wreu 3132
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-10 2145  ax-11 2161  ax-12 2178
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 2070  df-mo 2622  df-eu 2653  df-clel 2894  df-ral 3135  df-rex 3136  df-reu 3137
This theorem is referenced by:  2reuimp  43610
  Copyright terms: Public domain W3C validator