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

Theorem kmlem15 8930
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 1840 . . . . . . 7 𝑢 𝑣 ∈ (𝑧𝑦)
32eu1 2509 . . . . . 6 (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑣(𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)))
4 elin 3774 . . . . . . . . 9 (𝑣 ∈ (𝑧𝑦) ↔ (𝑣𝑧𝑣𝑦))
5 clelsb3 2726 . . . . . . . . . . . 12 ([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) ↔ 𝑢 ∈ (𝑧𝑦))
6 elin 3774 . . . . . . . . . . . 12 (𝑢 ∈ (𝑧𝑦) ↔ (𝑢𝑧𝑢𝑦))
75, 6bitri 264 . . . . . . . . . . 11 ([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) ↔ (𝑢𝑧𝑢𝑦))
8 equcom 1942 . . . . . . . . . . 11 (𝑣 = 𝑢𝑢 = 𝑣)
97, 8imbi12i 340 . . . . . . . . . 10 (([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢) ↔ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
109albii 1744 . . . . . . . . 9 (∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢) ↔ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
114, 10anbi12i 732 . . . . . . . 8 ((𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ((𝑣𝑧𝑣𝑦) ∧ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
12 19.28v 1906 . . . . . . . 8 (∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ((𝑣𝑧𝑣𝑦) ∧ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1311, 12bitr4i 267 . . . . . . 7 ((𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1413exbii 1771 . . . . . 6 (∃𝑣(𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
153, 14bitri 264 . . . . 5 (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1615ralbii 2974 . . . 4 (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
17 df-ral 2912 . . . . 5 (∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧(𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
18 kmlem14.2 . . . . . . . . . 10 (𝜓 ↔ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
1918albii 1744 . . . . . . . . 9 (∀𝑢𝜓 ↔ ∀𝑢(𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
20 19.21v 1865 . . . . . . . . 9 (∀𝑢(𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2119, 20bitri 264 . . . . . . . 8 (∀𝑢𝜓 ↔ (𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2221exbii 1771 . . . . . . 7 (∃𝑣𝑢𝜓 ↔ ∃𝑣(𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
23 19.37v 1907 . . . . . . 7 (∃𝑣(𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2422, 23bitri 264 . . . . . 6 (∃𝑣𝑢𝜓 ↔ (𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2524albii 1744 . . . . 5 (∀𝑧𝑣𝑢𝜓 ↔ ∀𝑧(𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2617, 25bitr4i 267 . . . 4 (∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧𝑣𝑢𝜓)
271, 16, 263bitri 286 . . 3 (𝜒 ↔ ∀𝑧𝑣𝑢𝜓)
2827anbi2i 729 . 2 ((¬ 𝑦𝑥𝜒) ↔ (¬ 𝑦𝑥 ∧ ∀𝑧𝑣𝑢𝜓))
29 19.28v 1906 . 2 (∀𝑧𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ (¬ 𝑦𝑥 ∧ ∀𝑧𝑣𝑢𝜓))
30 19.28v 1906 . . . . 5 (∀𝑢𝑦𝑥𝜓) ↔ (¬ 𝑦𝑥 ∧ ∀𝑢𝜓))
3130exbii 1771 . . . 4 (∃𝑣𝑢𝑦𝑥𝜓) ↔ ∃𝑣𝑦𝑥 ∧ ∀𝑢𝜓))
32 19.42v 1915 . . . 4 (∃𝑣𝑦𝑥 ∧ ∀𝑢𝜓) ↔ (¬ 𝑦𝑥 ∧ ∃𝑣𝑢𝜓))
3331, 32bitr2i 265 . . 3 ((¬ 𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ ∃𝑣𝑢𝑦𝑥𝜓))
3433albii 1744 . 2 (∀𝑧𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
3528, 29, 343bitr2i 288 1 ((¬ 𝑦𝑥𝜒) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wal 1478  wex 1701  [wsb 1877  wcel 1987  ∃!weu 2469  wne 2790  wral 2907  cin 3554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-v 3188  df-in 3562
This theorem is referenced by:  kmlem16  8931
  Copyright terms: Public domain W3C validator