MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  kmlem15 Structured version   Visualization version   GIF version

Theorem kmlem15 9667
Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.)
Hypotheses
Ref Expression
kmlem14.1 (𝜑 ↔ (𝑧𝑦 → ((𝑣𝑥𝑦𝑣) ∧ 𝑧𝑣)))
kmlem14.2 (𝜓 ↔ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
kmlem14.3 (𝜒 ↔ ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦))
Assertion
Ref Expression
kmlem15 ((¬ 𝑦𝑥𝜒) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑣,𝑢   𝜑,𝑢
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑣)   𝜓(𝑥,𝑦,𝑧,𝑣,𝑢)   𝜒(𝑥,𝑦,𝑧,𝑣,𝑢)

Proof of Theorem kmlem15
StepHypRef Expression
1 kmlem14.3 . . . 4 (𝜒 ↔ ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦))
2 nfv 1921 . . . . . . 7 𝑢 𝑣 ∈ (𝑧𝑦)
32eu1 2614 . . . . . 6 (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑣(𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)))
4 elin 3860 . . . . . . . . 9 (𝑣 ∈ (𝑧𝑦) ↔ (𝑣𝑧𝑣𝑦))
5 clelsb3 2861 . . . . . . . . . . . 12 ([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) ↔ 𝑢 ∈ (𝑧𝑦))
6 elin 3860 . . . . . . . . . . . 12 (𝑢 ∈ (𝑧𝑦) ↔ (𝑢𝑧𝑢𝑦))
75, 6bitri 278 . . . . . . . . . . 11 ([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) ↔ (𝑢𝑧𝑢𝑦))
8 equcom 2030 . . . . . . . . . . 11 (𝑣 = 𝑢𝑢 = 𝑣)
97, 8imbi12i 354 . . . . . . . . . 10 (([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢) ↔ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
109albii 1826 . . . . . . . . 9 (∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢) ↔ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
114, 10anbi12i 630 . . . . . . . 8 ((𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ((𝑣𝑧𝑣𝑦) ∧ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
12 19.28v 2002 . . . . . . . 8 (∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ((𝑣𝑧𝑣𝑦) ∧ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1311, 12bitr4i 281 . . . . . . 7 ((𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1413exbii 1854 . . . . . 6 (∃𝑣(𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
153, 14bitri 278 . . . . 5 (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1615ralbii 3081 . . . 4 (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
17 df-ral 3059 . . . . 5 (∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧(𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
18 kmlem14.2 . . . . . . . . . 10 (𝜓 ↔ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
1918albii 1826 . . . . . . . . 9 (∀𝑢𝜓 ↔ ∀𝑢(𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
20 19.21v 1946 . . . . . . . . 9 (∀𝑢(𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2119, 20bitri 278 . . . . . . . 8 (∀𝑢𝜓 ↔ (𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2221exbii 1854 . . . . . . 7 (∃𝑣𝑢𝜓 ↔ ∃𝑣(𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
23 19.37v 2003 . . . . . . 7 (∃𝑣(𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2422, 23bitri 278 . . . . . 6 (∃𝑣𝑢𝜓 ↔ (𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2524albii 1826 . . . . 5 (∀𝑧𝑣𝑢𝜓 ↔ ∀𝑧(𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2617, 25bitr4i 281 . . . 4 (∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧𝑣𝑢𝜓)
271, 16, 263bitri 300 . . 3 (𝜒 ↔ ∀𝑧𝑣𝑢𝜓)
2827anbi2i 626 . 2 ((¬ 𝑦𝑥𝜒) ↔ (¬ 𝑦𝑥 ∧ ∀𝑧𝑣𝑢𝜓))
29 19.28v 2002 . 2 (∀𝑧𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ (¬ 𝑦𝑥 ∧ ∀𝑧𝑣𝑢𝜓))
30 19.28v 2002 . . . . 5 (∀𝑢𝑦𝑥𝜓) ↔ (¬ 𝑦𝑥 ∧ ∀𝑢𝜓))
3130exbii 1854 . . . 4 (∃𝑣𝑢𝑦𝑥𝜓) ↔ ∃𝑣𝑦𝑥 ∧ ∀𝑢𝜓))
32 19.42v 1961 . . . 4 (∃𝑣𝑦𝑥 ∧ ∀𝑢𝜓) ↔ (¬ 𝑦𝑥 ∧ ∃𝑣𝑢𝜓))
3331, 32bitr2i 279 . . 3 ((¬ 𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ ∃𝑣𝑢𝑦𝑥𝜓))
3433albii 1826 . 2 (∀𝑧𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
3528, 29, 343bitr2i 302 1 ((¬ 𝑦𝑥𝜒) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1540  wex 1786  [wsb 2074  wcel 2114  ∃!weu 2570  wne 2935  wral 3054  cin 3843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-v 3401  df-in 3851
This theorem is referenced by:  kmlem16  9668
  Copyright terms: Public domain W3C validator