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

Theorem iunfi 7146
Description: The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 7147. 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 2738 . . . 4  |-  ( w  =  (/)  ->  ( A. x  e.  w  B  e.  Fin  <->  A. x  e.  (/)  B  e.  Fin ) )
2 iuneq1 3920 . . . . . 6  |-  ( w  =  (/)  ->  U_ x  e.  w  B  =  U_ x  e.  (/)  B )
3 0iun 3961 . . . . . 6  |-  U_ x  e.  (/)  B  =  (/)
42, 3syl6eq 2333 . . . . 5  |-  ( w  =  (/)  ->  U_ x  e.  w  B  =  (/) )
54eleq1d 2351 . . . 4  |-  ( w  =  (/)  ->  ( U_ x  e.  w  B  e.  Fin  <->  (/)  e.  Fin )
)
61, 5imbi12d 311 . . 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 2738 . . . 4  |-  ( w  =  y  ->  ( A. x  e.  w  B  e.  Fin  <->  A. x  e.  y  B  e.  Fin ) )
8 iuneq1 3920 . . . . 5  |-  ( w  =  y  ->  U_ x  e.  w  B  =  U_ x  e.  y  B )
98eleq1d 2351 . . . 4  |-  ( w  =  y  ->  ( U_ x  e.  w  B  e.  Fin  <->  U_ x  e.  y  B  e.  Fin ) )
107, 9imbi12d 311 . . 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 2738 . . . 4  |-  ( w  =  ( y  u. 
{ z } )  ->  ( A. x  e.  w  B  e.  Fin 
<-> 
A. x  e.  ( y  u.  { z } ) B  e. 
Fin ) )
12 iuneq1 3920 . . . . 5  |-  ( w  =  ( y  u. 
{ z } )  ->  U_ x  e.  w  B  =  U_ x  e.  ( y  u.  {
z } ) B )
1312eleq1d 2351 . . . 4  |-  ( w  =  ( y  u. 
{ z } )  ->  ( U_ x  e.  w  B  e.  Fin 
<-> 
U_ x  e.  ( y  u.  { z } ) B  e. 
Fin ) )
1411, 13imbi12d 311 . . 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 2738 . . . 4  |-  ( w  =  A  ->  ( A. x  e.  w  B  e.  Fin  <->  A. x  e.  A  B  e.  Fin ) )
16 iuneq1 3920 . . . . 5  |-  ( w  =  A  ->  U_ x  e.  w  B  =  U_ x  e.  A  B
)
1716eleq1d 2351 . . . 4  |-  ( w  =  A  ->  ( U_ x  e.  w  B  e.  Fin  <->  U_ x  e.  A  B  e.  Fin ) )
1815, 17imbi12d 311 . . 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 7089 . . . 4  |-  (/)  e.  Fin
2019a1i 10 . . 3  |-  ( A. x  e.  (/)  B  e. 
Fin  ->  (/)  e.  Fin )
21 ssun1 3340 . . . . . . 7  |-  y  C_  ( y  u.  {
z } )
22 ssralv 3239 . . . . . . 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 54 . . . . 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 3985 . . . . . . 7  |-  U_ x  e.  ( y  u.  {
z } ) B  =  ( U_ x  e.  y  B  u.  U_ x  e.  { z } B )
26 nfcv 2421 . . . . . . . . . . 11  |-  F/_ y B
27 nfcsb1v 3115 . . . . . . . . . . 11  |-  F/_ x [_ y  /  x ]_ B
28 csbeq1a 3091 . . . . . . . . . . 11  |-  ( x  =  y  ->  B  =  [_ y  /  x ]_ B )
2926, 27, 28cbviun 3941 . . . . . . . . . 10  |-  U_ x  e.  { z } B  =  U_ y  e.  {
z } [_ y  /  x ]_ B
30 vex 2793 . . . . . . . . . . 11  |-  z  e. 
_V
31 csbeq1 3086 . . . . . . . . . . 11  |-  ( y  =  z  ->  [_ y  /  x ]_ B  = 
[_ z  /  x ]_ B )
3230, 31iunxsn 3983 . . . . . . . . . 10  |-  U_ y  e.  { z } [_ y  /  x ]_ B  =  [_ z  /  x ]_ B
3329, 32eqtri 2305 . . . . . . . . 9  |-  U_ x  e.  { z } B  =  [_ z  /  x ]_ B
34 ssun2 3341 . . . . . . . . . . 11  |-  { z }  C_  ( y  u.  { z } )
3530snid 3669 . . . . . . . . . . 11  |-  z  e. 
{ z }
3634, 35sselii 3179 . . . . . . . . . 10  |-  z  e.  ( y  u.  {
z } )
37 nfcsb1v 3115 . . . . . . . . . . . 12  |-  F/_ x [_ z  /  x ]_ B
3837nfel1 2431 . . . . . . . . . . 11  |-  F/ x [_ z  /  x ]_ B  e.  Fin
39 csbeq1a 3091 . . . . . . . . . . . 12  |-  ( x  =  z  ->  B  =  [_ z  /  x ]_ B )
4039eleq1d 2351 . . . . . . . . . . 11  |-  ( x  =  z  ->  ( B  e.  Fin  <->  [_ z  /  x ]_ B  e.  Fin ) )
4138, 40rspc 2880 . . . . . . . . . 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 2369 . . . . . . . 8  |-  ( A. x  e.  ( y  u.  { z } ) B  e.  Fin  ->  U_ x  e.  { z } B  e.  Fin )
44 unfi 7126 . . . . . . . 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 460 . . . . . . 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 2369 . . . . . 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 424 . . . . 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 25 . . . 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 10 . . 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 7100 . 2  |-  ( A  e.  Fin  ->  ( A. x  e.  A  B  e.  Fin  ->  U_ x  e.  A  B  e.  Fin ) )
5150imp 418 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 358    = wceq 1625    e. wcel 1686   A.wral 2545   [_csb 3083    u. cun 3152    C_ wss 3154   (/)c0 3457   {csn 3642   U_ciun 3907   Fincfn 6865
This theorem is referenced by:  unifi  7147  ixpfi  7155  marypha2  7194  ackbij1lem9  7856  ackbij1lem10  7857  fsum2dlem  12235  fsumcom2  12239  fsumiun  12281  hashiun  12282  ackbijnn  12288  ablfaclem3  15324  txcmplem2  17338  alexsubALTlem3  17745  aannenlem1  19710  fsumvma  20454  isunscov  25085  locfincmp  26315  fiphp3d  26913  hbt  27345
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-recs 6390  df-rdg 6425  df-1o 6481  df-oadd 6485  df-er 6662  df-en 6866  df-fin 6869
  Copyright terms: Public domain W3C validator