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

Theorem kmlem11 9585
 Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004.)
Hypothesis
Ref Expression
kmlem9.1 𝐴 = {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))}
Assertion
Ref Expression
kmlem11 (𝑧𝑥 → (𝑧 𝐴) = (𝑧 (𝑥 ∖ {𝑧})))
Distinct variable groups:   𝑥,𝑧,𝑢,𝑡   𝑧,𝐴
Allowed substitution hints:   𝐴(𝑥,𝑢,𝑡)

Proof of Theorem kmlem11
StepHypRef Expression
1 kmlem9.1 . . . . . 6 𝐴 = {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))}
21unieqi 4850 . . . . 5 𝐴 = {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))}
3 vex 3497 . . . . . . 7 𝑡 ∈ V
43difexi 5231 . . . . . 6 (𝑡 (𝑥 ∖ {𝑡})) ∈ V
54dfiun2 4957 . . . . 5 𝑡𝑥 (𝑡 (𝑥 ∖ {𝑡})) = {𝑢 ∣ ∃𝑡𝑥 𝑢 = (𝑡 (𝑥 ∖ {𝑡}))}
62, 5eqtr4i 2847 . . . 4 𝐴 = 𝑡𝑥 (𝑡 (𝑥 ∖ {𝑡}))
76ineq2i 4185 . . 3 (𝑧 𝐴) = (𝑧 𝑡𝑥 (𝑡 (𝑥 ∖ {𝑡})))
8 iunin2 4992 . . 3 𝑡𝑥 (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = (𝑧 𝑡𝑥 (𝑡 (𝑥 ∖ {𝑡})))
97, 8eqtr4i 2847 . 2 (𝑧 𝐴) = 𝑡𝑥 (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡})))
10 undif2 4424 . . . . . 6 ({𝑧} ∪ (𝑥 ∖ {𝑧})) = ({𝑧} ∪ 𝑥)
11 snssi 4740 . . . . . . 7 (𝑧𝑥 → {𝑧} ⊆ 𝑥)
12 ssequn1 4155 . . . . . . 7 ({𝑧} ⊆ 𝑥 ↔ ({𝑧} ∪ 𝑥) = 𝑥)
1311, 12sylib 220 . . . . . 6 (𝑧𝑥 → ({𝑧} ∪ 𝑥) = 𝑥)
1410, 13syl5req 2869 . . . . 5 (𝑧𝑥𝑥 = ({𝑧} ∪ (𝑥 ∖ {𝑧})))
1514iuneq1d 4945 . . . 4 (𝑧𝑥 𝑡𝑥 (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))))
16 iunxun 5015 . . . . . 6 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ( 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))))
17 vex 3497 . . . . . . . 8 𝑧 ∈ V
18 difeq1 4091 . . . . . . . . . 10 (𝑡 = 𝑧 → (𝑡 (𝑥 ∖ {𝑡})) = (𝑧 (𝑥 ∖ {𝑡})))
19 sneq 4576 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → {𝑡} = {𝑧})
2019difeq2d 4098 . . . . . . . . . . . 12 (𝑡 = 𝑧 → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {𝑧}))
2120unieqd 4851 . . . . . . . . . . 11 (𝑡 = 𝑧 (𝑥 ∖ {𝑡}) = (𝑥 ∖ {𝑧}))
2221difeq2d 4098 . . . . . . . . . 10 (𝑡 = 𝑧 → (𝑧 (𝑥 ∖ {𝑡})) = (𝑧 (𝑥 ∖ {𝑧})))
2318, 22eqtrd 2856 . . . . . . . . 9 (𝑡 = 𝑧 → (𝑡 (𝑥 ∖ {𝑡})) = (𝑧 (𝑥 ∖ {𝑧})))
2423ineq2d 4188 . . . . . . . 8 (𝑡 = 𝑧 → (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = (𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧}))))
2517, 24iunxsn 5012 . . . . . . 7 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = (𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧})))
2625uneq1i 4134 . . . . . 6 ( 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡})))) = ((𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧}))) ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))))
2716, 26eqtri 2844 . . . . 5 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧}))) ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))))
28 eldifsni 4721 . . . . . . . . . 10 (𝑡 ∈ (𝑥 ∖ {𝑧}) → 𝑡𝑧)
29 incom 4177 . . . . . . . . . . . 12 (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑧)
30 kmlem4 9578 . . . . . . . . . . . 12 ((𝑧𝑥𝑡𝑧) → ((𝑡 (𝑥 ∖ {𝑡})) ∩ 𝑧) = ∅)
3129, 30syl5eq 2868 . . . . . . . . . . 11 ((𝑧𝑥𝑡𝑧) → (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ∅)
3231ex 415 . . . . . . . . . 10 (𝑧𝑥 → (𝑡𝑧 → (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ∅))
3328, 32syl5 34 . . . . . . . . 9 (𝑧𝑥 → (𝑡 ∈ (𝑥 ∖ {𝑧}) → (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ∅))
3433ralrimiv 3181 . . . . . . . 8 (𝑧𝑥 → ∀𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ∅)
35 iuneq2 4937 . . . . . . . 8 (∀𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ∅ → 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = 𝑡 ∈ (𝑥 ∖ {𝑧})∅)
3634, 35syl 17 . . . . . . 7 (𝑧𝑥 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = 𝑡 ∈ (𝑥 ∖ {𝑧})∅)
37 iun0 4984 . . . . . . 7 𝑡 ∈ (𝑥 ∖ {𝑧})∅ = ∅
3836, 37syl6eq 2872 . . . . . 6 (𝑧𝑥 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ∅)
3938uneq2d 4138 . . . . 5 (𝑧𝑥 → ((𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧}))) ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡})))) = ((𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧}))) ∪ ∅))
4027, 39syl5eq 2868 . . . 4 (𝑧𝑥 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧}))) ∪ ∅))
4115, 40eqtrd 2856 . . 3 (𝑧𝑥 𝑡𝑥 (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧}))) ∪ ∅))
42 un0 4343 . . . 4 ((𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧}))) ∪ ∅) = (𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧})))
43 indif 4245 . . . 4 (𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧}))) = (𝑧 (𝑥 ∖ {𝑧}))
4442, 43eqtri 2844 . . 3 ((𝑧 ∩ (𝑧 (𝑥 ∖ {𝑧}))) ∪ ∅) = (𝑧 (𝑥 ∖ {𝑧}))
4541, 44syl6eq 2872 . 2 (𝑧𝑥 𝑡𝑥 (𝑧 ∩ (𝑡 (𝑥 ∖ {𝑡}))) = (𝑧 (𝑥 ∖ {𝑧})))
469, 45syl5eq 2868 1 (𝑧𝑥 → (𝑧 𝐴) = (𝑧 (𝑥 ∖ {𝑧})))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {cab 2799   ≠ wne 3016  ∀wral 3138  ∃wrex 3139   ∖ cdif 3932   ∪ cun 3933   ∩ cin 3934   ⊆ wss 3935  ∅c0 4290  {csn 4566  ∪ cuni 4837  ∪ ciun 4918 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-sn 4567  df-uni 4838  df-iun 4920 This theorem is referenced by:  kmlem12  9586
 Copyright terms: Public domain W3C validator