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

Theorem kmlem15 9920
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 1917 . . . . . . 7 𝑢 𝑣 ∈ (𝑧𝑦)
32eu1 2612 . . . . . 6 (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑣(𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)))
4 elin 3903 . . . . . . . . 9 (𝑣 ∈ (𝑧𝑦) ↔ (𝑣𝑧𝑣𝑦))
5 clelsb1 2866 . . . . . . . . . . . 12 ([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) ↔ 𝑢 ∈ (𝑧𝑦))
6 elin 3903 . . . . . . . . . . . 12 (𝑢 ∈ (𝑧𝑦) ↔ (𝑢𝑧𝑢𝑦))
75, 6bitri 274 . . . . . . . . . . 11 ([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) ↔ (𝑢𝑧𝑢𝑦))
8 equcom 2021 . . . . . . . . . . 11 (𝑣 = 𝑢𝑢 = 𝑣)
97, 8imbi12i 351 . . . . . . . . . 10 (([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢) ↔ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
109albii 1822 . . . . . . . . 9 (∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢) ↔ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
114, 10anbi12i 627 . . . . . . . 8 ((𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ((𝑣𝑧𝑣𝑦) ∧ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
12 19.28v 1994 . . . . . . . 8 (∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ((𝑣𝑧𝑣𝑦) ∧ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1311, 12bitr4i 277 . . . . . . 7 ((𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1413exbii 1850 . . . . . 6 (∃𝑣(𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
153, 14bitri 274 . . . . 5 (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1615ralbii 3092 . . . 4 (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
17 df-ral 3069 . . . . 5 (∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧(𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
18 kmlem14.2 . . . . . . . . . 10 (𝜓 ↔ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
1918albii 1822 . . . . . . . . 9 (∀𝑢𝜓 ↔ ∀𝑢(𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
20 19.21v 1942 . . . . . . . . 9 (∀𝑢(𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2119, 20bitri 274 . . . . . . . 8 (∀𝑢𝜓 ↔ (𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2221exbii 1850 . . . . . . 7 (∃𝑣𝑢𝜓 ↔ ∃𝑣(𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
23 19.37v 1995 . . . . . . 7 (∃𝑣(𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2422, 23bitri 274 . . . . . 6 (∃𝑣𝑢𝜓 ↔ (𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2524albii 1822 . . . . 5 (∀𝑧𝑣𝑢𝜓 ↔ ∀𝑧(𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2617, 25bitr4i 277 . . . 4 (∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧𝑣𝑢𝜓)
271, 16, 263bitri 297 . . 3 (𝜒 ↔ ∀𝑧𝑣𝑢𝜓)
2827anbi2i 623 . 2 ((¬ 𝑦𝑥𝜒) ↔ (¬ 𝑦𝑥 ∧ ∀𝑧𝑣𝑢𝜓))
29 19.28v 1994 . 2 (∀𝑧𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ (¬ 𝑦𝑥 ∧ ∀𝑧𝑣𝑢𝜓))
30 19.28v 1994 . . . . 5 (∀𝑢𝑦𝑥𝜓) ↔ (¬ 𝑦𝑥 ∧ ∀𝑢𝜓))
3130exbii 1850 . . . 4 (∃𝑣𝑢𝑦𝑥𝜓) ↔ ∃𝑣𝑦𝑥 ∧ ∀𝑢𝜓))
32 19.42v 1957 . . . 4 (∃𝑣𝑦𝑥 ∧ ∀𝑢𝜓) ↔ (¬ 𝑦𝑥 ∧ ∃𝑣𝑢𝜓))
3331, 32bitr2i 275 . . 3 ((¬ 𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ ∃𝑣𝑢𝑦𝑥𝜓))
3433albii 1822 . 2 (∀𝑧𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
3528, 29, 343bitr2i 299 1 ((¬ 𝑦𝑥𝜒) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wal 1537  wex 1782  [wsb 2067  wcel 2106  ∃!weu 2568  wne 2943  wral 3064  cin 3886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-in 3894
This theorem is referenced by:  kmlem16  9921
  Copyright terms: Public domain W3C validator