ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2reuswapdc GIF version

Theorem 2reuswapdc 2765
Description: A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by NM, 16-Jun-2017.)
Assertion
Ref Expression
2reuswapdc (DECID𝑥𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → (∀𝑥𝐴 ∃*𝑦𝐵 𝜑 → (∃!𝑥𝐴𝑦𝐵 𝜑 → ∃!𝑦𝐵𝑥𝐴 𝜑)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐵(𝑦)

Proof of Theorem 2reuswapdc
StepHypRef Expression
1 df-rmo 2331 . . 3 (∃*𝑦𝐵 𝜑 ↔ ∃*𝑦(𝑦𝐵𝜑))
21ralbii 2347 . 2 (∀𝑥𝐴 ∃*𝑦𝐵 𝜑 ↔ ∀𝑥𝐴 ∃*𝑦(𝑦𝐵𝜑))
3 df-ral 2328 . . . 4 (∀𝑥𝐴 ∃*𝑦(𝑦𝐵𝜑) ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦(𝑦𝐵𝜑)))
4 moanimv 1991 . . . . 5 (∃*𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) ↔ (𝑥𝐴 → ∃*𝑦(𝑦𝐵𝜑)))
54albii 1375 . . . 4 (∀𝑥∃*𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦(𝑦𝐵𝜑)))
63, 5bitr4i 180 . . 3 (∀𝑥𝐴 ∃*𝑦(𝑦𝐵𝜑) ↔ ∀𝑥∃*𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)))
7 df-reu 2330 . . . . . 6 (∃!𝑥𝐴𝑦𝐵 𝜑 ↔ ∃!𝑥(𝑥𝐴 ∧ ∃𝑦𝐵 𝜑))
8 r19.42v 2484 . . . . . . . . 9 (∃𝑦𝐵 (𝑥𝐴𝜑) ↔ (𝑥𝐴 ∧ ∃𝑦𝐵 𝜑))
9 df-rex 2329 . . . . . . . . 9 (∃𝑦𝐵 (𝑥𝐴𝜑) ↔ ∃𝑦(𝑦𝐵 ∧ (𝑥𝐴𝜑)))
108, 9bitr3i 179 . . . . . . . 8 ((𝑥𝐴 ∧ ∃𝑦𝐵 𝜑) ↔ ∃𝑦(𝑦𝐵 ∧ (𝑥𝐴𝜑)))
11 an12 503 . . . . . . . . 9 ((𝑦𝐵 ∧ (𝑥𝐴𝜑)) ↔ (𝑥𝐴 ∧ (𝑦𝐵𝜑)))
1211exbii 1512 . . . . . . . 8 (∃𝑦(𝑦𝐵 ∧ (𝑥𝐴𝜑)) ↔ ∃𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)))
1310, 12bitri 177 . . . . . . 7 ((𝑥𝐴 ∧ ∃𝑦𝐵 𝜑) ↔ ∃𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)))
1413eubii 1925 . . . . . 6 (∃!𝑥(𝑥𝐴 ∧ ∃𝑦𝐵 𝜑) ↔ ∃!𝑥𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)))
157, 14bitri 177 . . . . 5 (∃!𝑥𝐴𝑦𝐵 𝜑 ↔ ∃!𝑥𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)))
16 2euswapdc 2007 . . . . 5 (DECID𝑥𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → (∀𝑥∃*𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → (∃!𝑥𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → ∃!𝑦𝑥(𝑥𝐴 ∧ (𝑦𝐵𝜑)))))
1715, 16syl7bi 158 . . . 4 (DECID𝑥𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → (∀𝑥∃*𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → (∃!𝑥𝐴𝑦𝐵 𝜑 → ∃!𝑦𝑥(𝑥𝐴 ∧ (𝑦𝐵𝜑)))))
18 df-reu 2330 . . . . . 6 (∃!𝑦𝐵𝑥𝐴 𝜑 ↔ ∃!𝑦(𝑦𝐵 ∧ ∃𝑥𝐴 𝜑))
19 r19.42v 2484 . . . . . . . 8 (∃𝑥𝐴 (𝑦𝐵𝜑) ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝜑))
20 df-rex 2329 . . . . . . . 8 (∃𝑥𝐴 (𝑦𝐵𝜑) ↔ ∃𝑥(𝑥𝐴 ∧ (𝑦𝐵𝜑)))
2119, 20bitr3i 179 . . . . . . 7 ((𝑦𝐵 ∧ ∃𝑥𝐴 𝜑) ↔ ∃𝑥(𝑥𝐴 ∧ (𝑦𝐵𝜑)))
2221eubii 1925 . . . . . 6 (∃!𝑦(𝑦𝐵 ∧ ∃𝑥𝐴 𝜑) ↔ ∃!𝑦𝑥(𝑥𝐴 ∧ (𝑦𝐵𝜑)))
2318, 22bitri 177 . . . . 5 (∃!𝑦𝐵𝑥𝐴 𝜑 ↔ ∃!𝑦𝑥(𝑥𝐴 ∧ (𝑦𝐵𝜑)))
2423imbi2i 219 . . . 4 ((∃!𝑥𝐴𝑦𝐵 𝜑 → ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ (∃!𝑥𝐴𝑦𝐵 𝜑 → ∃!𝑦𝑥(𝑥𝐴 ∧ (𝑦𝐵𝜑))))
2517, 24syl6ibr 155 . . 3 (DECID𝑥𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → (∀𝑥∃*𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → (∃!𝑥𝐴𝑦𝐵 𝜑 → ∃!𝑦𝐵𝑥𝐴 𝜑)))
266, 25syl5bi 145 . 2 (DECID𝑥𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → (∀𝑥𝐴 ∃*𝑦(𝑦𝐵𝜑) → (∃!𝑥𝐴𝑦𝐵 𝜑 → ∃!𝑦𝐵𝑥𝐴 𝜑)))
272, 26syl5bi 145 1 (DECID𝑥𝑦(𝑥𝐴 ∧ (𝑦𝐵𝜑)) → (∀𝑥𝐴 ∃*𝑦𝐵 𝜑 → (∃!𝑥𝐴𝑦𝐵 𝜑 → ∃!𝑦𝐵𝑥𝐴 𝜑)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  DECID wdc 753  wal 1257  wex 1397  wcel 1409  ∃!weu 1916  ∃*wmo 1917  wral 2323  wrex 2324  ∃!wreu 2325  ∃*wrmo 2326
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444
This theorem depends on definitions:  df-bi 114  df-dc 754  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-ral 2328  df-rex 2329  df-reu 2330  df-rmo 2331
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator