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

Theorem kmlem15 9564
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 1915 . . . . . . 7 𝑢 𝑣 ∈ (𝑧𝑦)
32eu1 2693 . . . . . 6 (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑣(𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)))
4 elin 3925 . . . . . . . . 9 (𝑣 ∈ (𝑧𝑦) ↔ (𝑣𝑧𝑣𝑦))
5 clelsb3 2938 . . . . . . . . . . . 12 ([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) ↔ 𝑢 ∈ (𝑧𝑦))
6 elin 3925 . . . . . . . . . . . 12 (𝑢 ∈ (𝑧𝑦) ↔ (𝑢𝑧𝑢𝑦))
75, 6bitri 277 . . . . . . . . . . 11 ([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) ↔ (𝑢𝑧𝑢𝑦))
8 equcom 2025 . . . . . . . . . . 11 (𝑣 = 𝑢𝑢 = 𝑣)
97, 8imbi12i 353 . . . . . . . . . 10 (([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢) ↔ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
109albii 1820 . . . . . . . . 9 (∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢) ↔ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
114, 10anbi12i 628 . . . . . . . 8 ((𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ((𝑣𝑧𝑣𝑦) ∧ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
12 19.28v 1997 . . . . . . . 8 (∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ((𝑣𝑧𝑣𝑦) ∧ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1311, 12bitr4i 280 . . . . . . 7 ((𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1413exbii 1848 . . . . . 6 (∃𝑣(𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
153, 14bitri 277 . . . . 5 (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1615ralbii 3152 . . . 4 (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
17 df-ral 3130 . . . . 5 (∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧(𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
18 kmlem14.2 . . . . . . . . . 10 (𝜓 ↔ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
1918albii 1820 . . . . . . . . 9 (∀𝑢𝜓 ↔ ∀𝑢(𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
20 19.21v 1940 . . . . . . . . 9 (∀𝑢(𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2119, 20bitri 277 . . . . . . . 8 (∀𝑢𝜓 ↔ (𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2221exbii 1848 . . . . . . 7 (∃𝑣𝑢𝜓 ↔ ∃𝑣(𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
23 19.37v 1998 . . . . . . 7 (∃𝑣(𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2422, 23bitri 277 . . . . . 6 (∃𝑣𝑢𝜓 ↔ (𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2524albii 1820 . . . . 5 (∀𝑧𝑣𝑢𝜓 ↔ ∀𝑧(𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2617, 25bitr4i 280 . . . 4 (∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧𝑣𝑢𝜓)
271, 16, 263bitri 299 . . 3 (𝜒 ↔ ∀𝑧𝑣𝑢𝜓)
2827anbi2i 624 . 2 ((¬ 𝑦𝑥𝜒) ↔ (¬ 𝑦𝑥 ∧ ∀𝑧𝑣𝑢𝜓))
29 19.28v 1997 . 2 (∀𝑧𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ (¬ 𝑦𝑥 ∧ ∀𝑧𝑣𝑢𝜓))
30 19.28v 1997 . . . . 5 (∀𝑢𝑦𝑥𝜓) ↔ (¬ 𝑦𝑥 ∧ ∀𝑢𝜓))
3130exbii 1848 . . . 4 (∃𝑣𝑢𝑦𝑥𝜓) ↔ ∃𝑣𝑦𝑥 ∧ ∀𝑢𝜓))
32 19.42v 1954 . . . 4 (∃𝑣𝑦𝑥 ∧ ∀𝑢𝜓) ↔ (¬ 𝑦𝑥 ∧ ∃𝑣𝑢𝜓))
3331, 32bitr2i 278 . . 3 ((¬ 𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ ∃𝑣𝑢𝑦𝑥𝜓))
3433albii 1820 . 2 (∀𝑧𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
3528, 29, 343bitr2i 301 1 ((¬ 𝑦𝑥𝜒) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wal 1535  wex 1780  [wsb 2069  wcel 2114  ∃!weu 2652  wne 3006  wral 3125  cin 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-ral 3130  df-v 3472  df-in 3916
This theorem is referenced by:  kmlem16  9565
  Copyright terms: Public domain W3C validator