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

Theorem iunfi 8115
Description: The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 8116. Note that 𝐵 depends on 𝑥, i.e. can be thought of as 𝐵(𝑥). (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
iunfi ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵 ∈ Fin) → 𝑥𝐴 𝐵 ∈ Fin)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem iunfi
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 3115 . . . 4 (𝑤 = ∅ → (∀𝑥𝑤 𝐵 ∈ Fin ↔ ∀𝑥 ∈ ∅ 𝐵 ∈ Fin))
2 iuneq1 4465 . . . . . 6 (𝑤 = ∅ → 𝑥𝑤 𝐵 = 𝑥 ∈ ∅ 𝐵)
3 0iun 4508 . . . . . 6 𝑥 ∈ ∅ 𝐵 = ∅
42, 3syl6eq 2660 . . . . 5 (𝑤 = ∅ → 𝑥𝑤 𝐵 = ∅)
54eleq1d 2672 . . . 4 (𝑤 = ∅ → ( 𝑥𝑤 𝐵 ∈ Fin ↔ ∅ ∈ Fin))
61, 5imbi12d 333 . . 3 (𝑤 = ∅ → ((∀𝑥𝑤 𝐵 ∈ Fin → 𝑥𝑤 𝐵 ∈ Fin) ↔ (∀𝑥 ∈ ∅ 𝐵 ∈ Fin → ∅ ∈ Fin)))
7 raleq 3115 . . . 4 (𝑤 = 𝑦 → (∀𝑥𝑤 𝐵 ∈ Fin ↔ ∀𝑥𝑦 𝐵 ∈ Fin))
8 iuneq1 4465 . . . . 5 (𝑤 = 𝑦 𝑥𝑤 𝐵 = 𝑥𝑦 𝐵)
98eleq1d 2672 . . . 4 (𝑤 = 𝑦 → ( 𝑥𝑤 𝐵 ∈ Fin ↔ 𝑥𝑦 𝐵 ∈ Fin))
107, 9imbi12d 333 . . 3 (𝑤 = 𝑦 → ((∀𝑥𝑤 𝐵 ∈ Fin → 𝑥𝑤 𝐵 ∈ Fin) ↔ (∀𝑥𝑦 𝐵 ∈ Fin → 𝑥𝑦 𝐵 ∈ Fin)))
11 raleq 3115 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥𝑤 𝐵 ∈ Fin ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin))
12 iuneq1 4465 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → 𝑥𝑤 𝐵 = 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵)
1312eleq1d 2672 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → ( 𝑥𝑤 𝐵 ∈ Fin ↔ 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin))
1411, 13imbi12d 333 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → ((∀𝑥𝑤 𝐵 ∈ Fin → 𝑥𝑤 𝐵 ∈ Fin) ↔ (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin)))
15 raleq 3115 . . . 4 (𝑤 = 𝐴 → (∀𝑥𝑤 𝐵 ∈ Fin ↔ ∀𝑥𝐴 𝐵 ∈ Fin))
16 iuneq1 4465 . . . . 5 (𝑤 = 𝐴 𝑥𝑤 𝐵 = 𝑥𝐴 𝐵)
1716eleq1d 2672 . . . 4 (𝑤 = 𝐴 → ( 𝑥𝑤 𝐵 ∈ Fin ↔ 𝑥𝐴 𝐵 ∈ Fin))
1815, 17imbi12d 333 . . 3 (𝑤 = 𝐴 → ((∀𝑥𝑤 𝐵 ∈ Fin → 𝑥𝑤 𝐵 ∈ Fin) ↔ (∀𝑥𝐴 𝐵 ∈ Fin → 𝑥𝐴 𝐵 ∈ Fin)))
19 0fin 8051 . . . 4 ∅ ∈ Fin
2019a1i 11 . . 3 (∀𝑥 ∈ ∅ 𝐵 ∈ Fin → ∅ ∈ Fin)
21 ssun1 3738 . . . . . . 7 𝑦 ⊆ (𝑦 ∪ {𝑧})
22 ssralv 3629 . . . . . . 7 (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∀𝑥𝑦 𝐵 ∈ Fin))
2321, 22ax-mp 5 . . . . . 6 (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ∀𝑥𝑦 𝐵 ∈ Fin)
2423imim1i 61 . . . . 5 ((∀𝑥𝑦 𝐵 ∈ Fin → 𝑥𝑦 𝐵 ∈ Fin) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → 𝑥𝑦 𝐵 ∈ Fin))
25 iunxun 4536 . . . . . . 7 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 = ( 𝑥𝑦 𝐵 𝑥 ∈ {𝑧}𝐵)
26 nfcv 2751 . . . . . . . . . . 11 𝑦𝐵
27 nfcsb1v 3515 . . . . . . . . . . 11 𝑥𝑦 / 𝑥𝐵
28 csbeq1a 3508 . . . . . . . . . . 11 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
2926, 27, 28cbviun 4488 . . . . . . . . . 10 𝑥 ∈ {𝑧}𝐵 = 𝑦 ∈ {𝑧}𝑦 / 𝑥𝐵
30 vex 3176 . . . . . . . . . . 11 𝑧 ∈ V
31 csbeq1 3502 . . . . . . . . . . 11 (𝑦 = 𝑧𝑦 / 𝑥𝐵 = 𝑧 / 𝑥𝐵)
3230, 31iunxsn 4534 . . . . . . . . . 10 𝑦 ∈ {𝑧}𝑦 / 𝑥𝐵 = 𝑧 / 𝑥𝐵
3329, 32eqtri 2632 . . . . . . . . 9 𝑥 ∈ {𝑧}𝐵 = 𝑧 / 𝑥𝐵
34 ssun2 3739 . . . . . . . . . . 11 {𝑧} ⊆ (𝑦 ∪ {𝑧})
35 vsnid 4156 . . . . . . . . . . 11 𝑧 ∈ {𝑧}
3634, 35sselii 3565 . . . . . . . . . 10 𝑧 ∈ (𝑦 ∪ {𝑧})
37 nfcsb1v 3515 . . . . . . . . . . . 12 𝑥𝑧 / 𝑥𝐵
3837nfel1 2765 . . . . . . . . . . 11 𝑥𝑧 / 𝑥𝐵 ∈ Fin
39 csbeq1a 3508 . . . . . . . . . . . 12 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
4039eleq1d 2672 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝐵 ∈ Fin ↔ 𝑧 / 𝑥𝐵 ∈ Fin))
4138, 40rspc 3276 . . . . . . . . . 10 (𝑧 ∈ (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → 𝑧 / 𝑥𝐵 ∈ Fin))
4236, 41ax-mp 5 . . . . . . . . 9 (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → 𝑧 / 𝑥𝐵 ∈ Fin)
4333, 42syl5eqel 2692 . . . . . . . 8 (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → 𝑥 ∈ {𝑧}𝐵 ∈ Fin)
44 unfi 8090 . . . . . . . 8 (( 𝑥𝑦 𝐵 ∈ Fin ∧ 𝑥 ∈ {𝑧}𝐵 ∈ Fin) → ( 𝑥𝑦 𝐵 𝑥 ∈ {𝑧}𝐵) ∈ Fin)
4543, 44sylan2 490 . . . . . . 7 (( 𝑥𝑦 𝐵 ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin) → ( 𝑥𝑦 𝐵 𝑥 ∈ {𝑧}𝐵) ∈ Fin)
4625, 45syl5eqel 2692 . . . . . 6 (( 𝑥𝑦 𝐵 ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin) → 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin)
4746expcom 450 . . . . 5 (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → ( 𝑥𝑦 𝐵 ∈ Fin → 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin))
4824, 47sylcom 30 . . . 4 ((∀𝑥𝑦 𝐵 ∈ Fin → 𝑥𝑦 𝐵 ∈ Fin) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin))
4948a1i 11 . . 3 (𝑦 ∈ Fin → ((∀𝑥𝑦 𝐵 ∈ Fin → 𝑥𝑦 𝐵 ∈ Fin) → (∀𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin → 𝑥 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ Fin)))
506, 10, 14, 18, 20, 49findcard2 8063 . 2 (𝐴 ∈ Fin → (∀𝑥𝐴 𝐵 ∈ Fin → 𝑥𝐴 𝐵 ∈ Fin))
5150imp 444 1 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵 ∈ Fin) → 𝑥𝐴 𝐵 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  wral 2896  csb 3499  cun 3538  wss 3540  c0 3874  {csn 4125   ciun 4450  Fincfn 7819
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-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-int 4406  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-oadd 7429  df-er 7607  df-en 7820  df-fin 7823
This theorem is referenced by:  unifi  8116  infssuni  8118  ixpfi  8124  ackbij1lem9  8911  ackbij1lem10  8912  fsuppmapnn0fiublem  12609  fsuppmapnn0fiub  12610  fsuppmapnn0fiubOLD  12611  fsum2dlem  14292  fsumcom2  14296  fsumcom2OLD  14297  fsumiun  14343  hashiun  14344  ackbijnn  14348  fprod2dlem  14498  fprodcom2  14502  fprodcom2OLD  14503  ablfaclem3  18258  pmatcoe1fsupp  20273  locfincmp  21087  txcmplem2  21203  alexsubALTlem3  21611  aannenlem1  23832  fsumvma  24683  frghash2spot  26384  usgreghash2spotv  26387  poimirlem30  32403  fiphp3d  36195  hbt  36513  frgrhash2wsp  41489  fusgreghash2wspv  41491
  Copyright terms: Public domain W3C validator