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

Theorem unfi 9046
Description: The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 16-Nov-2002.) Avoid ax-pow 5315. (Revised by BTernaryTau, 7-Aug-2024.)
Assertion
Ref Expression
unfi ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴𝐵) ∈ Fin)

Proof of Theorem unfi
Dummy variables 𝑥 𝑦 𝑧 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uneq2 4112 . . . . 5 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ∪ ∅))
21eleq1d 2822 . . . 4 (𝑥 = ∅ → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∪ ∅) ∈ Fin))
32imbi2d 341 . . 3 (𝑥 = ∅ → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)))
4 uneq2 4112 . . . . 5 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
54eleq1d 2822 . . . 4 (𝑥 = 𝑦 → ((𝐴𝑥) ∈ Fin ↔ (𝐴𝑦) ∈ Fin))
65imbi2d 341 . . 3 (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴𝑦) ∈ Fin)))
7 uneq2 4112 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴𝑥) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
87eleq1d 2822 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
98imbi2d 341 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
10 uneq2 4112 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥) = (𝐴𝐵))
1110eleq1d 2822 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥) ∈ Fin ↔ (𝐴𝐵) ∈ Fin))
1211imbi2d 341 . . 3 (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴𝐵) ∈ Fin)))
13 un0 4345 . . . . 5 (𝐴 ∪ ∅) = 𝐴
1413eleq1i 2828 . . . 4 ((𝐴 ∪ ∅) ∈ Fin ↔ 𝐴 ∈ Fin)
1514biimpri 227 . . 3 (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)
16 snssi 4763 . . . . . . . . . . 11 (𝑧𝐴 → {𝑧} ⊆ 𝐴)
17 ssequn2 4138 . . . . . . . . . . . . . 14 ({𝑧} ⊆ 𝐴 ↔ (𝐴 ∪ {𝑧}) = 𝐴)
1817biimpi 215 . . . . . . . . . . . . 13 ({𝑧} ⊆ 𝐴 → (𝐴 ∪ {𝑧}) = 𝐴)
1918uneq2d 4118 . . . . . . . . . . . 12 ({𝑧} ⊆ 𝐴 → (𝑦 ∪ (𝐴 ∪ {𝑧})) = (𝑦𝐴))
20 un12 4122 . . . . . . . . . . . 12 (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝑦 ∪ (𝐴 ∪ {𝑧}))
21 uncom 4108 . . . . . . . . . . . 12 (𝐴𝑦) = (𝑦𝐴)
2219, 20, 213eqtr4g 2802 . . . . . . . . . . 11 ({𝑧} ⊆ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴𝑦))
2316, 22syl 17 . . . . . . . . . 10 (𝑧𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴𝑦))
2423eleq1d 2822 . . . . . . . . 9 (𝑧𝐴 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin ↔ (𝐴𝑦) ∈ Fin))
2524biimprd 248 . . . . . . . 8 (𝑧𝐴 → ((𝐴𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
2625adantld 492 . . . . . . 7 (𝑧𝐴 → ((¬ 𝑧𝑦 ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
27 isfi 8846 . . . . . . . . . . 11 ((𝐴𝑦) ∈ Fin ↔ ∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤)
2827biimpi 215 . . . . . . . . . 10 ((𝐴𝑦) ∈ Fin → ∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤)
29 r19.41v 3183 . . . . . . . . . . 11 (∃𝑤 ∈ ω ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) ↔ (∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)))
30 disjsn 4667 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝐴𝑦))
31 elun 4103 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝐴𝑦) ↔ (𝑧𝐴𝑧𝑦))
3231notbii 320 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ (𝐴𝑦) ↔ ¬ (𝑧𝐴𝑧𝑦))
33 pm4.56 987 . . . . . . . . . . . . . . . . . . 19 ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ↔ ¬ (𝑧𝐴𝑧𝑦))
3432, 33bitr4i 278 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ (𝐴𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
3530, 34sylbbr 235 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) → ((𝐴𝑦) ∩ {𝑧}) = ∅)
36 nnord 7797 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ω → Ord 𝑤)
37 orddisj 6348 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑤 → (𝑤 ∩ {𝑤}) = ∅)
3836, 37syl 17 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ω → (𝑤 ∩ {𝑤}) = ∅)
39 en2sn 8915 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑤 ∈ V) → {𝑧} ≈ {𝑤})
4039el2v 3451 . . . . . . . . . . . . . . . . . . 19 {𝑧} ≈ {𝑤}
41 unen 8920 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑦) ≈ 𝑤 ∧ {𝑧} ≈ {𝑤}) ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4240, 41mpanl2 699 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ≈ 𝑤 ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4338, 42sylanr2 681 . . . . . . . . . . . . . . . . 17 (((𝐴𝑦) ≈ 𝑤 ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ ω)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4435, 43sylanr1 680 . . . . . . . . . . . . . . . 16 (((𝐴𝑦) ≈ 𝑤 ∧ ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ ω)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
45443impb 1115 . . . . . . . . . . . . . . 15 (((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ ω) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
46453comr 1125 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
47463expb 1120 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
48 unass 4121 . . . . . . . . . . . . . 14 ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
49 df-suc 6316 . . . . . . . . . . . . . . . . 17 suc 𝑤 = (𝑤 ∪ {𝑤})
50 peano2 7814 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ω → suc 𝑤 ∈ ω)
5149, 50eqeltrrid 2843 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ω → (𝑤 ∪ {𝑤}) ∈ ω)
52 breq2 5104 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑤 ∪ {𝑤}) → (((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣 ↔ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})))
5352rspcev 3576 . . . . . . . . . . . . . . . 16 (((𝑤 ∪ {𝑤}) ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
5451, 53sylan 581 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
55 isfi 8846 . . . . . . . . . . . . . . 15 (((𝐴𝑦) ∪ {𝑧}) ∈ Fin ↔ ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
5654, 55sylibr 233 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ((𝐴𝑦) ∪ {𝑧}) ∈ Fin)
5748, 56eqeltrrid 2843 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
5847, 57syldan 592 . . . . . . . . . . . 12 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
5958rexlimiva 3142 . . . . . . . . . . 11 (∃𝑤 ∈ ω ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6029, 59sylbir 234 . . . . . . . . . 10 ((∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6128, 60sylan 581 . . . . . . . . 9 (((𝐴𝑦) ∈ Fin ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6261ancoms 460 . . . . . . . 8 (((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6362expl 459 . . . . . . 7 𝑧𝐴 → ((¬ 𝑧𝑦 ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
6426, 63pm2.61i 182 . . . . . 6 ((¬ 𝑧𝑦 ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6564ex 414 . . . . 5 𝑧𝑦 → ((𝐴𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
6665imim2d 57 . . . 4 𝑧𝑦 → ((𝐴 ∈ Fin → (𝐴𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
6766adantl 483 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝐴 ∈ Fin → (𝐴𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
683, 6, 9, 12, 15, 67findcard2s 9039 . 2 (𝐵 ∈ Fin → (𝐴 ∈ Fin → (𝐴𝐵) ∈ Fin))
6968impcom 409 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴𝐵) ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wo 845   = wceq 1541  wcel 2106  wrex 3071  Vcvv 3443  cun 3903  cin 3904  wss 3905  c0 4277  {csn 4581   class class class wbr 5100  Ord word 6309  suc csuc 6312  ωcom 7789  cen 8810  Fincfn 8813
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5251  ax-nul 5258  ax-pr 5379  ax-un 7659
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3735  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3924  df-nul 4278  df-if 4482  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-br 5101  df-opab 5163  df-tr 5218  df-id 5525  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5582  df-we 5584  df-xp 5633  df-rel 5634  df-cnv 5635  df-co 5636  df-dm 5637  df-rn 5638  df-res 5639  df-ima 5640  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6440  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-om 7790  df-en 8814  df-fin 8817
This theorem is referenced by:  ssfi  9047  imafi  9049  pwfilem  9051  cnvfi  9054  fnfi  9055  unfi2  9189  difinf  9190  xpfi  9191  xpfiOLD  9192  prfi  9196  tpfi  9197  iunfi  9214  pwfilemOLD  9220  fsuppun  9254  fsuppunfi  9255  ressuppfi  9261  fiin  9288  cantnfp1lem1  9544  ficardadju  10065  ficardun2  10068  ficardun2OLD  10069  ackbij1lem6  10091  ackbij1lem16  10101  fin23lem28  10206  fin23lem30  10208  isfin1-3  10252  axcclem  10323  hashun  14206  hashunlei  14249  hashmap  14259  hashbclem  14273  hashf1lem1OLD  14278  hashf1lem2  14279  hashf1  14280  fsumsplitsn  15560  fsummsnunz  15570  fsumsplitsnun  15571  incexclem  15652  isumltss  15664  fprodsplitsn  15803  lcmfunsnlem2lem1  16445  lcmfunsnlem2lem2  16446  lcmfunsnlem2  16447  lcmfun  16452  ramub1lem1  16829  fpwipodrs  18360  acsfiindd  18373  symgfisg  19177  gsumzunsnd  19656  gsumunsnfd  19657  dsmmacl  21058  psrbagaddclOLD  21242  mplsubg  21318  mpllss  21319  fctop  22264  uncmp  22664  bwth  22671  lfinun  22786  locfincmp  22787  comppfsc  22793  1stckgenlem  22814  ptbasin  22838  cfinfil  23154  fin1aufil  23193  alexsubALTlem3  23310  tmdgsum  23356  tsmsfbas  23389  tsmsgsum  23400  tsmsres  23405  tsmsxplem1  23414  prdsmet  23633  prdsbl  23757  icccmplem2  24096  rrxmval  24679  rrxmet  24682  rrxdstprj1  24683  ovolfiniun  24775  volfiniun  24821  fta1glem2  25441  fta1lem  25577  aannenlem2  25599  aalioulem2  25603  dchrfi  26513  usgrfilem  28049  ffsrn  31415  eulerpartlemt  32702  ballotlemgun  32855  hgt750lemb  33000  hgt750leme  33002  lindsenlbs  35928  poimirlem31  35964  poimirlem32  35965  itg2addnclem2  35985  ftc1anclem7  36012  ftc1anc  36014  prdsbnd  36107  pclfinN  38219  elrfi  40829  mzpcompact2lem  40886  eldioph2  40897  lsmfgcl  41213  fiuneneq  41336  unfid  43075  dvmptfprodlem  43873  dvnprodlem2  43876  fourierdlem50  44085  fourierdlem51  44086  fourierdlem54  44089  fourierdlem76  44111  fourierdlem80  44115  fourierdlem102  44137  fourierdlem103  44138  fourierdlem104  44139  fourierdlem114  44149  sge0resplit  44333  sge0iunmptlemfi  44340  sge0xaddlem1  44360  hoiprodp1  44515  sge0hsphoire  44516  hoidmvlelem1  44522  hoidmvlelem2  44523  hoidmvlelem5  44526  hspmbllem2  44554  fsummmodsnunz  45245  mndpsuppfi  46129
  Copyright terms: Public domain W3C validator