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

Theorem iunfi 7357
Description: The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 7358. Note that  B depends on  x, i.e. can be thought of as  B ( x ). (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
iunfi  |-  ( ( A  e.  Fin  /\  A. x  e.  A  B  e.  Fin )  ->  U_ x  e.  A  B  e.  Fin )
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem iunfi
Dummy variables  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 2868 . . . 4  |-  ( w  =  (/)  ->  ( A. x  e.  w  B  e.  Fin  <->  A. x  e.  (/)  B  e.  Fin ) )
2 iuneq1 4070 . . . . . 6  |-  ( w  =  (/)  ->  U_ x  e.  w  B  =  U_ x  e.  (/)  B )
3 0iun 4112 . . . . . 6  |-  U_ x  e.  (/)  B  =  (/)
42, 3syl6eq 2456 . . . . 5  |-  ( w  =  (/)  ->  U_ x  e.  w  B  =  (/) )
54eleq1d 2474 . . . 4  |-  ( w  =  (/)  ->  ( U_ x  e.  w  B  e.  Fin  <->  (/)  e.  Fin )
)
61, 5imbi12d 312 . . 3  |-  ( w  =  (/)  ->  ( ( A. x  e.  w  B  e.  Fin  ->  U_ x  e.  w  B  e.  Fin )  <->  ( A. x  e.  (/)  B  e.  Fin  -> 
(/)  e.  Fin )
) )
7 raleq 2868 . . . 4  |-  ( w  =  y  ->  ( A. x  e.  w  B  e.  Fin  <->  A. x  e.  y  B  e.  Fin ) )
8 iuneq1 4070 . . . . 5  |-  ( w  =  y  ->  U_ x  e.  w  B  =  U_ x  e.  y  B )
98eleq1d 2474 . . . 4  |-  ( w  =  y  ->  ( U_ x  e.  w  B  e.  Fin  <->  U_ x  e.  y  B  e.  Fin ) )
107, 9imbi12d 312 . . 3  |-  ( w  =  y  ->  (
( A. x  e.  w  B  e.  Fin  ->  U_ x  e.  w  B  e.  Fin )  <->  ( A. x  e.  y  B  e.  Fin  ->  U_ x  e.  y  B  e.  Fin ) ) )
11 raleq 2868 . . . 4  |-  ( w  =  ( y  u. 
{ z } )  ->  ( A. x  e.  w  B  e.  Fin 
<-> 
A. x  e.  ( y  u.  { z } ) B  e. 
Fin ) )
12 iuneq1 4070 . . . . 5  |-  ( w  =  ( y  u. 
{ z } )  ->  U_ x  e.  w  B  =  U_ x  e.  ( y  u.  {
z } ) B )
1312eleq1d 2474 . . . 4  |-  ( w  =  ( y  u. 
{ z } )  ->  ( U_ x  e.  w  B  e.  Fin 
<-> 
U_ x  e.  ( y  u.  { z } ) B  e. 
Fin ) )
1411, 13imbi12d 312 . . 3  |-  ( w  =  ( y  u. 
{ z } )  ->  ( ( A. x  e.  w  B  e.  Fin  ->  U_ x  e.  w  B  e.  Fin ) 
<->  ( A. x  e.  ( y  u.  {
z } ) B  e.  Fin  ->  U_ x  e.  ( y  u.  {
z } ) B  e.  Fin ) ) )
15 raleq 2868 . . . 4  |-  ( w  =  A  ->  ( A. x  e.  w  B  e.  Fin  <->  A. x  e.  A  B  e.  Fin ) )
16 iuneq1 4070 . . . . 5  |-  ( w  =  A  ->  U_ x  e.  w  B  =  U_ x  e.  A  B
)
1716eleq1d 2474 . . . 4  |-  ( w  =  A  ->  ( U_ x  e.  w  B  e.  Fin  <->  U_ x  e.  A  B  e.  Fin ) )
1815, 17imbi12d 312 . . 3  |-  ( w  =  A  ->  (
( A. x  e.  w  B  e.  Fin  ->  U_ x  e.  w  B  e.  Fin )  <->  ( A. x  e.  A  B  e.  Fin  ->  U_ x  e.  A  B  e.  Fin ) ) )
19 0fin 7299 . . . 4  |-  (/)  e.  Fin
2019a1i 11 . . 3  |-  ( A. x  e.  (/)  B  e. 
Fin  ->  (/)  e.  Fin )
21 ssun1 3474 . . . . . . 7  |-  y  C_  ( y  u.  {
z } )
22 ssralv 3371 . . . . . . 7  |-  ( y 
C_  ( y  u. 
{ z } )  ->  ( A. x  e.  ( y  u.  {
z } ) B  e.  Fin  ->  A. x  e.  y  B  e.  Fin ) )
2321, 22ax-mp 8 . . . . . 6  |-  ( A. x  e.  ( y  u.  { z } ) B  e.  Fin  ->  A. x  e.  y  B  e.  Fin )
2423imim1i 56 . . . . 5  |-  ( ( A. x  e.  y  B  e.  Fin  ->  U_ x  e.  y  B  e.  Fin )  -> 
( A. x  e.  ( y  u.  {
z } ) B  e.  Fin  ->  U_ x  e.  y  B  e.  Fin ) )
25 iunxun 4136 . . . . . . 7  |-  U_ x  e.  ( y  u.  {
z } ) B  =  ( U_ x  e.  y  B  u.  U_ x  e.  { z } B )
26 nfcv 2544 . . . . . . . . . . 11  |-  F/_ y B
27 nfcsb1v 3247 . . . . . . . . . . 11  |-  F/_ x [_ y  /  x ]_ B
28 csbeq1a 3223 . . . . . . . . . . 11  |-  ( x  =  y  ->  B  =  [_ y  /  x ]_ B )
2926, 27, 28cbviun 4092 . . . . . . . . . 10  |-  U_ x  e.  { z } B  =  U_ y  e.  {
z } [_ y  /  x ]_ B
30 vex 2923 . . . . . . . . . . 11  |-  z  e. 
_V
31 csbeq1 3218 . . . . . . . . . . 11  |-  ( y  =  z  ->  [_ y  /  x ]_ B  = 
[_ z  /  x ]_ B )
3230, 31iunxsn 4134 . . . . . . . . . 10  |-  U_ y  e.  { z } [_ y  /  x ]_ B  =  [_ z  /  x ]_ B
3329, 32eqtri 2428 . . . . . . . . 9  |-  U_ x  e.  { z } B  =  [_ z  /  x ]_ B
34 ssun2 3475 . . . . . . . . . . 11  |-  { z }  C_  ( y  u.  { z } )
3530snid 3805 . . . . . . . . . . 11  |-  z  e. 
{ z }
3634, 35sselii 3309 . . . . . . . . . 10  |-  z  e.  ( y  u.  {
z } )
37 nfcsb1v 3247 . . . . . . . . . . . 12  |-  F/_ x [_ z  /  x ]_ B
3837nfel1 2554 . . . . . . . . . . 11  |-  F/ x [_ z  /  x ]_ B  e.  Fin
39 csbeq1a 3223 . . . . . . . . . . . 12  |-  ( x  =  z  ->  B  =  [_ z  /  x ]_ B )
4039eleq1d 2474 . . . . . . . . . . 11  |-  ( x  =  z  ->  ( B  e.  Fin  <->  [_ z  /  x ]_ B  e.  Fin ) )
4138, 40rspc 3010 . . . . . . . . . 10  |-  ( z  e.  ( y  u. 
{ z } )  ->  ( A. x  e.  ( y  u.  {
z } ) B  e.  Fin  ->  [_ z  /  x ]_ B  e. 
Fin ) )
4236, 41ax-mp 8 . . . . . . . . 9  |-  ( A. x  e.  ( y  u.  { z } ) B  e.  Fin  ->  [_ z  /  x ]_ B  e.  Fin )
4333, 42syl5eqel 2492 . . . . . . . 8  |-  ( A. x  e.  ( y  u.  { z } ) B  e.  Fin  ->  U_ x  e.  { z } B  e.  Fin )
44 unfi 7337 . . . . . . . 8  |-  ( (
U_ x  e.  y  B  e.  Fin  /\  U_ x  e.  { z } B  e.  Fin )  ->  ( U_ x  e.  y  B  u.  U_ x  e.  { z } B )  e. 
Fin )
4543, 44sylan2 461 . . . . . . 7  |-  ( (
U_ x  e.  y  B  e.  Fin  /\  A. x  e.  ( y  u.  { z } ) B  e.  Fin )  ->  ( U_ x  e.  y  B  u.  U_ x  e.  { z } B )  e. 
Fin )
4625, 45syl5eqel 2492 . . . . . 6  |-  ( (
U_ x  e.  y  B  e.  Fin  /\  A. x  e.  ( y  u.  { z } ) B  e.  Fin )  ->  U_ x  e.  ( y  u.  { z } ) B  e. 
Fin )
4746expcom 425 . . . . 5  |-  ( A. x  e.  ( y  u.  { z } ) B  e.  Fin  ->  (
U_ x  e.  y  B  e.  Fin  ->  U_ x  e.  ( y  u.  { z } ) B  e.  Fin ) )
4824, 47sylcom 27 . . . 4  |-  ( ( A. x  e.  y  B  e.  Fin  ->  U_ x  e.  y  B  e.  Fin )  -> 
( A. x  e.  ( y  u.  {
z } ) B  e.  Fin  ->  U_ x  e.  ( y  u.  {
z } ) B  e.  Fin ) )
4948a1i 11 . . 3  |-  ( y  e.  Fin  ->  (
( A. x  e.  y  B  e.  Fin  ->  U_ x  e.  y  B  e.  Fin )  ->  ( A. x  e.  ( y  u.  {
z } ) B  e.  Fin  ->  U_ x  e.  ( y  u.  {
z } ) B  e.  Fin ) ) )
506, 10, 14, 18, 20, 49findcard2 7311 . 2  |-  ( A  e.  Fin  ->  ( A. x  e.  A  B  e.  Fin  ->  U_ x  e.  A  B  e.  Fin ) )
5150imp 419 1  |-  ( ( A  e.  Fin  /\  A. x  e.  A  B  e.  Fin )  ->  U_ x  e.  A  B  e.  Fin )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   A.wral 2670   [_csb 3215    u. cun 3282    C_ wss 3284   (/)c0 3592   {csn 3778   U_ciun 4057   Fincfn 7072
This theorem is referenced by:  unifi  7358  ixpfi  7366  ackbij1lem9  8068  ackbij1lem10  8069  fsum2dlem  12513  fsumcom2  12517  fsumiun  12559  hashiun  12560  ackbijnn  12566  ablfaclem3  15604  txcmplem2  17631  alexsubALTlem3  18037  aannenlem1  20202  fsumvma  20954  fprod2dlem  25261  fprodcom2  25265  locfincmp  26278  fiphp3d  26774  hbt  27206  frghash2spot  28170  usgreghash2spotv  28173
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-reu 2677  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-pss 3300  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-tp 3786  df-op 3787  df-uni 3980  df-int 4015  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-tr 4267  df-eprel 4458  df-id 4462  df-po 4467  df-so 4468  df-fr 4505  df-we 4507  df-ord 4548  df-on 4549  df-lim 4550  df-suc 4551  df-om 4809  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-recs 6596  df-rdg 6631  df-1o 6687  df-oadd 6691  df-er 6868  df-en 7073  df-fin 7076
  Copyright terms: Public domain W3C validator