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

Theorem kmlem15 10161
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 2604 . . . . . 6 (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑣(𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)))
4 elin 3963 . . . . . . . . 9 (𝑣 ∈ (𝑧𝑦) ↔ (𝑣𝑧𝑣𝑦))
5 clelsb1 2858 . . . . . . . . . . . 12 ([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) ↔ 𝑢 ∈ (𝑧𝑦))
6 elin 3963 . . . . . . . . . . . 12 (𝑢 ∈ (𝑧𝑦) ↔ (𝑢𝑧𝑢𝑦))
75, 6bitri 274 . . . . . . . . . . 11 ([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) ↔ (𝑢𝑧𝑢𝑦))
8 equcom 2019 . . . . . . . . . . 11 (𝑣 = 𝑢𝑢 = 𝑣)
97, 8imbi12i 349 . . . . . . . . . 10 (([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢) ↔ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
109albii 1819 . . . . . . . . 9 (∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢) ↔ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
114, 10anbi12i 625 . . . . . . . 8 ((𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ((𝑣𝑧𝑣𝑦) ∧ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
12 19.28v 1992 . . . . . . . 8 (∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ((𝑣𝑧𝑣𝑦) ∧ ∀𝑢((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1311, 12bitr4i 277 . . . . . . 7 ((𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1413exbii 1848 . . . . . 6 (∃𝑣(𝑣 ∈ (𝑧𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧𝑦) → 𝑣 = 𝑢)) ↔ ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
153, 14bitri 274 . . . . 5 (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
1615ralbii 3091 . . . 4 (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
17 df-ral 3060 . . . . 5 (∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧(𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
18 kmlem14.2 . . . . . . . . . 10 (𝜓 ↔ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
1918albii 1819 . . . . . . . . 9 (∀𝑢𝜓 ↔ ∀𝑢(𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
20 19.21v 1940 . . . . . . . . 9 (∀𝑢(𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2119, 20bitri 274 . . . . . . . 8 (∀𝑢𝜓 ↔ (𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2221exbii 1848 . . . . . . 7 (∃𝑣𝑢𝜓 ↔ ∃𝑣(𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
23 19.37v 1993 . . . . . . 7 (∃𝑣(𝑧𝑥 → ∀𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))) ↔ (𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2422, 23bitri 274 . . . . . 6 (∃𝑣𝑢𝜓 ↔ (𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2524albii 1819 . . . . 5 (∀𝑧𝑣𝑢𝜓 ↔ ∀𝑧(𝑧𝑥 → ∃𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2617, 25bitr4i 277 . . . 4 (∀𝑧𝑥𝑣𝑢((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧𝑣𝑢𝜓)
271, 16, 263bitri 296 . . 3 (𝜒 ↔ ∀𝑧𝑣𝑢𝜓)
2827anbi2i 621 . 2 ((¬ 𝑦𝑥𝜒) ↔ (¬ 𝑦𝑥 ∧ ∀𝑧𝑣𝑢𝜓))
29 19.28v 1992 . 2 (∀𝑧𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ (¬ 𝑦𝑥 ∧ ∀𝑧𝑣𝑢𝜓))
30 19.28v 1992 . . . . 5 (∀𝑢𝑦𝑥𝜓) ↔ (¬ 𝑦𝑥 ∧ ∀𝑢𝜓))
3130exbii 1848 . . . 4 (∃𝑣𝑢𝑦𝑥𝜓) ↔ ∃𝑣𝑦𝑥 ∧ ∀𝑢𝜓))
32 19.42v 1955 . . . 4 (∃𝑣𝑦𝑥 ∧ ∀𝑢𝜓) ↔ (¬ 𝑦𝑥 ∧ ∃𝑣𝑢𝜓))
3331, 32bitr2i 275 . . 3 ((¬ 𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ ∃𝑣𝑢𝑦𝑥𝜓))
3433albii 1819 . 2 (∀𝑧𝑦𝑥 ∧ ∃𝑣𝑢𝜓) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
3528, 29, 343bitr2i 298 1 ((¬ 𝑦𝑥𝜒) ↔ ∀𝑧𝑣𝑢𝑦𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wal 1537  wex 1779  [wsb 2065  wcel 2104  ∃!weu 2560  wne 2938  wral 3059  cin 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-v 3474  df-in 3954
This theorem is referenced by:  kmlem16  10162
  Copyright terms: Public domain W3C validator