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

Theorem unfi 9172
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 5364. (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 4158 . . . . 5 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ∪ ∅))
21eleq1d 2819 . . . 4 (𝑥 = ∅ → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∪ ∅) ∈ Fin))
32imbi2d 341 . . 3 (𝑥 = ∅ → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)))
4 uneq2 4158 . . . . 5 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
54eleq1d 2819 . . . 4 (𝑥 = 𝑦 → ((𝐴𝑥) ∈ Fin ↔ (𝐴𝑦) ∈ Fin))
65imbi2d 341 . . 3 (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴𝑦) ∈ Fin)))
7 uneq2 4158 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴𝑥) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
87eleq1d 2819 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
98imbi2d 341 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
10 uneq2 4158 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥) = (𝐴𝐵))
1110eleq1d 2819 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥) ∈ Fin ↔ (𝐴𝐵) ∈ Fin))
1211imbi2d 341 . . 3 (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴𝐵) ∈ Fin)))
13 un0 4391 . . . . 5 (𝐴 ∪ ∅) = 𝐴
1413eleq1i 2825 . . . 4 ((𝐴 ∪ ∅) ∈ Fin ↔ 𝐴 ∈ Fin)
1514biimpri 227 . . 3 (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)
16 snssi 4812 . . . . . . . . . . 11 (𝑧𝐴 → {𝑧} ⊆ 𝐴)
17 ssequn2 4184 . . . . . . . . . . . . . 14 ({𝑧} ⊆ 𝐴 ↔ (𝐴 ∪ {𝑧}) = 𝐴)
1817biimpi 215 . . . . . . . . . . . . 13 ({𝑧} ⊆ 𝐴 → (𝐴 ∪ {𝑧}) = 𝐴)
1918uneq2d 4164 . . . . . . . . . . . 12 ({𝑧} ⊆ 𝐴 → (𝑦 ∪ (𝐴 ∪ {𝑧})) = (𝑦𝐴))
20 un12 4168 . . . . . . . . . . . 12 (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝑦 ∪ (𝐴 ∪ {𝑧}))
21 uncom 4154 . . . . . . . . . . . 12 (𝐴𝑦) = (𝑦𝐴)
2219, 20, 213eqtr4g 2798 . . . . . . . . . . 11 ({𝑧} ⊆ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴𝑦))
2316, 22syl 17 . . . . . . . . . 10 (𝑧𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴𝑦))
2423eleq1d 2819 . . . . . . . . 9 (𝑧𝐴 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin ↔ (𝐴𝑦) ∈ Fin))
2524biimprd 247 . . . . . . . 8 (𝑧𝐴 → ((𝐴𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
2625adantld 492 . . . . . . 7 (𝑧𝐴 → ((¬ 𝑧𝑦 ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
27 isfi 8972 . . . . . . . . . . 11 ((𝐴𝑦) ∈ Fin ↔ ∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤)
2827biimpi 215 . . . . . . . . . 10 ((𝐴𝑦) ∈ Fin → ∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤)
29 r19.41v 3189 . . . . . . . . . . 11 (∃𝑤 ∈ ω ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) ↔ (∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)))
30 disjsn 4716 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝐴𝑦))
31 elun 4149 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝐴𝑦) ↔ (𝑧𝐴𝑧𝑦))
3231notbii 320 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ (𝐴𝑦) ↔ ¬ (𝑧𝐴𝑧𝑦))
33 pm4.56 988 . . . . . . . . . . . . . . . . . . 19 ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ↔ ¬ (𝑧𝐴𝑧𝑦))
3432, 33bitr4i 278 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ (𝐴𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
3530, 34sylbbr 235 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) → ((𝐴𝑦) ∩ {𝑧}) = ∅)
36 nnord 7863 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ω → Ord 𝑤)
37 orddisj 6403 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑤 → (𝑤 ∩ {𝑤}) = ∅)
3836, 37syl 17 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ω → (𝑤 ∩ {𝑤}) = ∅)
39 en2sn 9041 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑤 ∈ V) → {𝑧} ≈ {𝑤})
4039el2v 3483 . . . . . . . . . . . . . . . . . . 19 {𝑧} ≈ {𝑤}
41 unen 9046 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑦) ≈ 𝑤 ∧ {𝑧} ≈ {𝑤}) ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4240, 41mpanl2 700 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ≈ 𝑤 ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4338, 42sylanr2 682 . . . . . . . . . . . . . . . . 17 (((𝐴𝑦) ≈ 𝑤 ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ ω)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4435, 43sylanr1 681 . . . . . . . . . . . . . . . 16 (((𝐴𝑦) ≈ 𝑤 ∧ ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ ω)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
45443impb 1116 . . . . . . . . . . . . . . 15 (((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ ω) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
46453comr 1126 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
47463expb 1121 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
48 unass 4167 . . . . . . . . . . . . . 14 ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
49 df-suc 6371 . . . . . . . . . . . . . . . . 17 suc 𝑤 = (𝑤 ∪ {𝑤})
50 peano2 7881 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ω → suc 𝑤 ∈ ω)
5149, 50eqeltrrid 2839 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ω → (𝑤 ∪ {𝑤}) ∈ ω)
52 breq2 5153 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑤 ∪ {𝑤}) → (((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣 ↔ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})))
5352rspcev 3613 . . . . . . . . . . . . . . . 16 (((𝑤 ∪ {𝑤}) ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
5451, 53sylan 581 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
55 isfi 8972 . . . . . . . . . . . . . . 15 (((𝐴𝑦) ∪ {𝑧}) ∈ Fin ↔ ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
5654, 55sylibr 233 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ((𝐴𝑦) ∪ {𝑧}) ∈ Fin)
5748, 56eqeltrrid 2839 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
5847, 57syldan 592 . . . . . . . . . . . 12 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
5958rexlimiva 3148 . . . . . . . . . . 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 9165 . 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 846   = wceq 1542  wcel 2107  wrex 3071  Vcvv 3475  cun 3947  cin 3948  wss 3949  c0 4323  {csn 4629   class class class wbr 5149  Ord word 6364  suc csuc 6367  ωcom 7855  cen 8936  Fincfn 8939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-om 7856  df-en 8940  df-fin 8943
This theorem is referenced by:  ssfi  9173  imafi  9175  pwfilem  9177  cnvfi  9180  fnfi  9181  unfi2  9315  difinf  9316  xpfi  9317  xpfiOLD  9318  prfi  9322  tpfi  9323  iunfi  9340  pwfilemOLD  9346  fsuppun  9382  fsuppunfi  9383  ressuppfi  9390  fiin  9417  cantnfp1lem1  9673  ficardadju  10194  ficardun2  10197  ficardun2OLD  10198  ackbij1lem6  10220  ackbij1lem16  10230  fin23lem28  10335  fin23lem30  10337  isfin1-3  10381  axcclem  10452  hashun  14342  hashunlei  14385  hashmap  14395  hashbclem  14411  hashf1lem1OLD  14416  hashf1lem2  14417  hashf1  14418  fsumsplitsn  15690  fsummsnunz  15700  fsumsplitsnun  15701  incexclem  15782  isumltss  15794  fprodsplitsn  15933  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfunsnlem2  16577  lcmfun  16582  ramub1lem1  16959  fpwipodrs  18493  acsfiindd  18506  symgfisg  19336  gsumzunsnd  19824  gsumunsnfd  19825  dsmmacl  21296  psrbagaddclOLD  21482  mplsubg  21561  mpllss  21562  fctop  22507  uncmp  22907  bwth  22914  lfinun  23029  locfincmp  23030  comppfsc  23036  1stckgenlem  23057  ptbasin  23081  cfinfil  23397  fin1aufil  23436  alexsubALTlem3  23553  tmdgsum  23599  tsmsfbas  23632  tsmsgsum  23643  tsmsres  23648  tsmsxplem1  23657  prdsmet  23876  prdsbl  24000  icccmplem2  24339  rrxmval  24922  rrxmet  24925  rrxdstprj1  24926  ovolfiniun  25018  volfiniun  25064  fta1glem2  25684  fta1lem  25820  aannenlem2  25842  aalioulem2  25846  dchrfi  26758  usgrfilem  28584  ffsrn  31954  eulerpartlemt  33370  ballotlemgun  33523  hgt750lemb  33668  hgt750leme  33670  lindsenlbs  36483  poimirlem31  36519  poimirlem32  36520  itg2addnclem2  36540  ftc1anclem7  36567  ftc1anc  36569  prdsbnd  36661  pclfinN  38771  elrfi  41432  mzpcompact2lem  41489  eldioph2  41500  lsmfgcl  41816  fiuneneq  41939  unfid  43842  dvmptfprodlem  44660  dvnprodlem2  44663  fourierdlem50  44872  fourierdlem51  44873  fourierdlem54  44876  fourierdlem76  44898  fourierdlem80  44902  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem114  44936  sge0resplit  45122  sge0iunmptlemfi  45129  sge0xaddlem1  45149  hoiprodp1  45304  sge0hsphoire  45305  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem5  45315  hspmbllem2  45343  fsummmodsnunz  46043  mndpsuppfi  47051
  Copyright terms: Public domain W3C validator