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

Theorem kmlem12 8866
Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 27-Mar-2004.)
Hypothesis
Ref Expression
kmlem9.1 𝐴 = {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))}
Assertion
Ref Expression
kmlem12 (∀𝑧𝑥 (𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ → (∀𝑧𝐴 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴)))))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑣,𝑢,𝑡   𝑦,𝐴,𝑧,𝑣
Allowed substitution hints:   𝐴(𝑥,𝑢,𝑡)

Proof of Theorem kmlem12
StepHypRef Expression
1 kmlem9.1 . . . . 5 𝐴 = {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))}
21raleqi 3119 . . . 4 (∀𝑧𝐴 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ∀𝑧 ∈ {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))} (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦)))
3 df-ral 2901 . . . 4 (∀𝑧 ∈ {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))} (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ∀𝑧(𝑧 ∈ {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))} → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
4 vex 3176 . . . . . . . . 9 𝑧 ∈ V
5 eqeq1 2614 . . . . . . . . . 10 (𝑢 = 𝑧 → (𝑢 = (𝑡 (𝑥 ∖ {𝑡})) ↔ 𝑧 = (𝑡 (𝑥 ∖ {𝑡}))))
65rexbidv 3034 . . . . . . . . 9 (𝑢 = 𝑧 → (∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡})) ↔ ∃𝑡𝑥 𝑧 = (𝑡 (𝑥 ∖ {𝑡}))))
74, 6elab 3319 . . . . . . . 8 (𝑧 ∈ {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))} ↔ ∃𝑡𝑥 𝑧 = (𝑡 (𝑥 ∖ {𝑡})))
87imbi1i 338 . . . . . . 7 ((𝑧 ∈ {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))} → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ (∃𝑡𝑥 𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
9 r19.23v 3005 . . . . . . 7 (∀𝑡𝑥 (𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ (∃𝑡𝑥 𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
108, 9bitr4i 266 . . . . . 6 ((𝑧 ∈ {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))} → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ ∀𝑡𝑥 (𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
1110albii 1737 . . . . 5 (∀𝑧(𝑧 ∈ {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))} → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ ∀𝑧𝑡𝑥 (𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
12 ralcom4 3197 . . . . 5 (∀𝑡𝑥𝑧(𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ ∀𝑧𝑡𝑥 (𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))))
13 vex 3176 . . . . . . . 8 𝑡 ∈ V
14 difexg 4735 . . . . . . . 8 (𝑡 ∈ V → (𝑡 (𝑥 ∖ {𝑡})) ∈ V)
1513, 14ax-mp 5 . . . . . . 7 (𝑡 (𝑥 ∖ {𝑡})) ∈ V
16 neeq1 2844 . . . . . . . 8 (𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧 ≠ ∅ ↔ (𝑡 (𝑥 ∖ {𝑡})) ≠ ∅))
17 ineq1 3769 . . . . . . . . . 10 (𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧𝑦) = ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦))
1817eleq2d 2673 . . . . . . . . 9 (𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑣 ∈ (𝑧𝑦) ↔ 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)))
1918eubidv 2478 . . . . . . . 8 (𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (∃!𝑣 𝑣 ∈ (𝑧𝑦) ↔ ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)))
2016, 19imbi12d 333 . . . . . . 7 (𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → ((𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ((𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦))))
2115, 20ceqsalv 3206 . . . . . 6 (∀𝑧(𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ ((𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)))
2221ralbii 2963 . . . . 5 (∀𝑡𝑥𝑧(𝑧 = (𝑡 (𝑥 ∖ {𝑡})) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ ∀𝑡𝑥 ((𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)))
2311, 12, 223bitr2i 287 . . . 4 (∀𝑧(𝑧 ∈ {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))} → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦))) ↔ ∀𝑡𝑥 ((𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)))
242, 3, 233bitri 285 . . 3 (∀𝑧𝐴 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦)) ↔ ∀𝑡𝑥 ((𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)))
25 ralim 2932 . . 3 (∀𝑡𝑥 ((𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)) → (∀𝑡𝑥 (𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∀𝑡𝑥 ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)))
2624, 25sylbi 206 . 2 (∀𝑧𝐴 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → (∀𝑡𝑥 (𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∀𝑡𝑥 ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)))
27 difeq1 3683 . . . . . . . 8 (𝑡 = 𝑧 → (𝑡 (𝑥 ∖ {𝑡})) = (𝑧 (𝑥 ∖ {𝑡})))
28 sneq 4135 . . . . . . . . . . 11 (𝑡 = 𝑧 → {𝑡} = {𝑧})
2928difeq2d 3690 . . . . . . . . . 10 (𝑡 = 𝑧 → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {𝑧}))
3029unieqd 4382 . . . . . . . . 9 (𝑡 = 𝑧 (𝑥 ∖ {𝑡}) = (𝑥 ∖ {𝑧}))
3130difeq2d 3690 . . . . . . . 8 (𝑡 = 𝑧 → (𝑧 (𝑥 ∖ {𝑡})) = (𝑧 (𝑥 ∖ {𝑧})))
3227, 31eqtrd 2644 . . . . . . 7 (𝑡 = 𝑧 → (𝑡 (𝑥 ∖ {𝑡})) = (𝑧 (𝑥 ∖ {𝑧})))
3332neeq1d 2841 . . . . . 6 (𝑡 = 𝑧 → ((𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ ↔ (𝑧 (𝑥 ∖ {𝑧})) ≠ ∅))
3433cbvralv 3147 . . . . 5 (∀𝑡𝑥 (𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ ↔ ∀𝑧𝑥 (𝑧 (𝑥 ∖ {𝑧})) ≠ ∅)
3532ineq1d 3775 . . . . . . . 8 (𝑡 = 𝑧 → ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦) = ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦))
3635eleq2d 2673 . . . . . . 7 (𝑡 = 𝑧 → (𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦) ↔ 𝑣 ∈ ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦)))
3736eubidv 2478 . . . . . 6 (𝑡 = 𝑧 → (∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦) ↔ ∃!𝑣 𝑣 ∈ ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦)))
3837cbvralv 3147 . . . . 5 (∀𝑡𝑥 ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦) ↔ ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦))
3934, 38imbi12i 339 . . . 4 ((∀𝑡𝑥 (𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∀𝑡𝑥 ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)) ↔ (∀𝑧𝑥 (𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ → ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦)))
40 in12 3786 . . . . . . . . . . 11 (𝑧 ∩ (𝑦 𝐴)) = (𝑦 ∩ (𝑧 𝐴))
41 incom 3767 . . . . . . . . . . 11 (𝑦 ∩ (𝑧 𝐴)) = ((𝑧 𝐴) ∩ 𝑦)
4240, 41eqtri 2632 . . . . . . . . . 10 (𝑧 ∩ (𝑦 𝐴)) = ((𝑧 𝐴) ∩ 𝑦)
431kmlem11 8865 . . . . . . . . . . 11 (𝑧𝑥 → (𝑧 𝐴) = (𝑧 (𝑥 ∖ {𝑧})))
4443ineq1d 3775 . . . . . . . . . 10 (𝑧𝑥 → ((𝑧 𝐴) ∩ 𝑦) = ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦))
4542, 44syl5req 2657 . . . . . . . . 9 (𝑧𝑥 → ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦) = (𝑧 ∩ (𝑦 𝐴)))
4645eleq2d 2673 . . . . . . . 8 (𝑧𝑥 → (𝑣 ∈ ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦) ↔ 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴))))
4746eubidv 2478 . . . . . . 7 (𝑧𝑥 → (∃!𝑣 𝑣 ∈ ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦) ↔ ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴))))
48 ax-1 6 . . . . . . 7 (∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴)) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴))))
4947, 48syl6bi 242 . . . . . 6 (𝑧𝑥 → (∃!𝑣 𝑣 ∈ ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦) → (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴)))))
5049ralimia 2934 . . . . 5 (∀𝑧𝑥 ∃!𝑣 𝑣 ∈ ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦) → ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴))))
5150imim2i 16 . . . 4 ((∀𝑧𝑥 (𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ → ∀𝑧𝑥 ∃!𝑣 𝑣 ∈ ((𝑧 (𝑥 ∖ {𝑧})) ∩ 𝑦)) → (∀𝑧𝑥 (𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ → ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴)))))
5239, 51sylbi 206 . . 3 ((∀𝑡𝑥 (𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∀𝑡𝑥 ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)) → (∀𝑧𝑥 (𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ → ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴)))))
5352com12 32 . 2 (∀𝑧𝑥 (𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ → ((∀𝑡𝑥 (𝑡 (𝑥 ∖ {𝑡})) ≠ ∅ → ∀𝑡𝑥 ∃!𝑣 𝑣 ∈ ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑦)) → ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴)))))
5426, 53syl5 33 1 (∀𝑧𝑥 (𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ → (∀𝑧𝐴 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧𝑦)) → ∀𝑧𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 𝐴)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1473   = wceq 1475  wcel 1977  ∃!weu 2458  {cab 2596  wne 2780  wral 2896  wrex 2897  Vcvv 3173  cdif 3537  cin 3539  c0 3874  {csn 4125   cuni 4372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126  df-uni 4373  df-iun 4457
This theorem is referenced by:  kmlem13  8867
  Copyright terms: Public domain W3C validator