Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  comptiunov2i Structured version   Unicode version

Theorem comptiunov2i 35665
Description: The composition two indexed unions is sometimes a similar indexed union. (Contributed by RP, 10-Jun-2020.)
Hypotheses
Ref Expression
comptiunov2.x  |-  X  =  ( a  e.  _V  |->  U_ i  e.  I  ( a  .^  i )
)
comptiunov2.y  |-  Y  =  ( b  e.  _V  |->  U_ j  e.  J  ( b  .^  j )
)
comptiunov2.z  |-  Z  =  ( c  e.  _V  |->  U_ k  e.  K  ( c  .^  k )
)
comptiunov2.i  |-  I  e. 
_V
comptiunov2.j  |-  J  e. 
_V
comptiunov2.k  |-  K  =  ( I  u.  J
)
comptiunov2.1  |-  U_ k  e.  I  ( d  .^  k )  C_  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )
comptiunov2.2  |-  U_ k  e.  J  ( d  .^  k )  C_  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )
comptiunov2.3  |-  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )  C_  U_ k  e.  ( I  u.  J
) ( d  .^  k )
Assertion
Ref Expression
comptiunov2i  |-  ( X  o.  Y )  =  Z
Distinct variable groups:    i, a,  .^    .^ , b    .^ , c    I, a,
i    k, I    j, a, J, i    J, b   
k, J    k, c, K    X, d    Y, d    Z, d    a, d, i, j    b, d, j   
c, d, k
Allowed substitution hints:    .^ ( j, k, d)    I( j, b, c, d)    J( c, d)    K( i, j, a, b, d)    X( i, j, k, a, b, c)    Y( i, j, k, a, b, c)    Z( i, j, k, a, b, c)

Proof of Theorem comptiunov2i
StepHypRef Expression
1 comptiunov2.x . . . 4  |-  X  =  ( a  e.  _V  |->  U_ i  e.  I  ( a  .^  i )
)
21funmpt2 5605 . . 3  |-  Fun  X
3 comptiunov2.y . . . 4  |-  Y  =  ( b  e.  _V  |->  U_ j  e.  J  ( b  .^  j )
)
43funmpt2 5605 . . 3  |-  Fun  Y
5 funco 5606 . . 3  |-  ( ( Fun  X  /\  Fun  Y )  ->  Fun  ( X  o.  Y ) )
62, 4, 5mp2an 670 . 2  |-  Fun  ( X  o.  Y )
7 comptiunov2.z . . 3  |-  Z  =  ( c  e.  _V  |->  U_ k  e.  K  ( c  .^  k )
)
87funmpt2 5605 . 2  |-  Fun  Z
9 ssv 3461 . . . . . . 7  |-  ran  Y  C_ 
_V
10 comptiunov2.i . . . . . . . . 9  |-  I  e. 
_V
11 ovex 6305 . . . . . . . . 9  |-  ( a 
.^  i )  e. 
_V
1210, 11iunex 6763 . . . . . . . 8  |-  U_ i  e.  I  ( a  .^  i )  e.  _V
1312, 1dmmpti 5692 . . . . . . 7  |-  dom  X  =  _V
149, 13sseqtr4i 3474 . . . . . 6  |-  ran  Y  C_ 
dom  X
15 dmcosseq 5084 . . . . . 6  |-  ( ran 
Y  C_  dom  X  ->  dom  ( X  o.  Y
)  =  dom  Y
)
1614, 15ax-mp 5 . . . . 5  |-  dom  ( X  o.  Y )  =  dom  Y
17 comptiunov2.j . . . . . . 7  |-  J  e. 
_V
18 ovex 6305 . . . . . . 7  |-  ( b 
.^  j )  e. 
_V
1917, 18iunex 6763 . . . . . 6  |-  U_ j  e.  J  ( b  .^  j )  e.  _V
2019, 3dmmpti 5692 . . . . 5  |-  dom  Y  =  _V
2116, 20eqtri 2431 . . . 4  |-  dom  ( X  o.  Y )  =  _V
22 comptiunov2.k . . . . . . 7  |-  K  =  ( I  u.  J
)
2310, 17unex 6579 . . . . . . 7  |-  ( I  u.  J )  e. 
_V
2422, 23eqeltri 2486 . . . . . 6  |-  K  e. 
_V
25 ovex 6305 . . . . . 6  |-  ( c 
.^  k )  e. 
_V
2624, 25iunex 6763 . . . . 5  |-  U_ k  e.  K  ( c  .^  k )  e.  _V
2726, 7dmmpti 5692 . . . 4  |-  dom  Z  =  _V
2821, 27eqtr4i 2434 . . 3  |-  dom  ( X  o.  Y )  =  dom  Z
29 vex 3061 . . . . . . . . 9  |-  d  e. 
_V
3029, 20eleqtrri 2489 . . . . . . . 8  |-  d  e. 
dom  Y
31 fvco 5924 . . . . . . . 8  |-  ( ( Fun  Y  /\  d  e.  dom  Y )  -> 
( ( X  o.  Y ) `  d
)  =  ( X `
 ( Y `  d ) ) )
324, 30, 31mp2an 670 . . . . . . 7  |-  ( ( X  o.  Y ) `
 d )  =  ( X `  ( Y `  d )
)
33 oveq1 6284 . . . . . . . . . . 11  |-  ( b  =  d  ->  (
b  .^  j )  =  ( d  .^  j ) )
3433iuneq2d 4297 . . . . . . . . . 10  |-  ( b  =  d  ->  U_ j  e.  J  ( b  .^  j )  =  U_ j  e.  J  (
d  .^  j )
)
35 ovex 6305 . . . . . . . . . . 11  |-  ( d 
.^  j )  e. 
_V
3617, 35iunex 6763 . . . . . . . . . 10  |-  U_ j  e.  J  ( d  .^  j )  e.  _V
3734, 3, 36fvmpt 5931 . . . . . . . . 9  |-  ( d  e.  _V  ->  ( Y `  d )  =  U_ j  e.  J  ( d  .^  j
) )
3829, 37ax-mp 5 . . . . . . . 8  |-  ( Y `
 d )  = 
U_ j  e.  J  ( d  .^  j
)
3938fveq2i 5851 . . . . . . 7  |-  ( X `
 ( Y `  d ) )  =  ( X `  U_ j  e.  J  ( d  .^  j ) )
40 oveq1 6284 . . . . . . . . . 10  |-  ( a  =  U_ j  e.  J  ( d  .^  j )  ->  (
a  .^  i )  =  ( U_ j  e.  J  ( d  .^  j )  .^  i
) )
4140iuneq2d 4297 . . . . . . . . 9  |-  ( a  =  U_ j  e.  J  ( d  .^  j )  ->  U_ i  e.  I  ( a  .^  i )  =  U_ i  e.  I  ( U_ j  e.  J  ( d  .^  j
)  .^  i )
)
42 ovex 6305 . . . . . . . . . 10  |-  ( U_ j  e.  J  (
d  .^  j )  .^  i )  e.  _V
4310, 42iunex 6763 . . . . . . . . 9  |-  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )  e.  _V
4441, 1, 43fvmpt 5931 . . . . . . . 8  |-  ( U_ j  e.  J  (
d  .^  j )  e.  _V  ->  ( X `  U_ j  e.  J  ( d  .^  j
) )  =  U_ i  e.  I  ( U_ j  e.  J  ( d  .^  j
)  .^  i )
)
4536, 44ax-mp 5 . . . . . . 7  |-  ( X `
 U_ j  e.  J  ( d  .^  j
) )  =  U_ i  e.  I  ( U_ j  e.  J  ( d  .^  j
)  .^  i )
4632, 39, 453eqtri 2435 . . . . . 6  |-  ( ( X  o.  Y ) `
 d )  = 
U_ i  e.  I 
( U_ j  e.  J  ( d  .^  j
)  .^  i )
47 oveq1 6284 . . . . . . . . 9  |-  ( c  =  d  ->  (
c  .^  k )  =  ( d  .^  k ) )
4847iuneq2d 4297 . . . . . . . 8  |-  ( c  =  d  ->  U_ k  e.  K  ( c  .^  k )  =  U_ k  e.  K  (
d  .^  k )
)
49 ovex 6305 . . . . . . . . 9  |-  ( d 
.^  k )  e. 
_V
5024, 49iunex 6763 . . . . . . . 8  |-  U_ k  e.  K  ( d  .^  k )  e.  _V
5148, 7, 50fvmpt 5931 . . . . . . 7  |-  ( d  e.  _V  ->  ( Z `  d )  =  U_ k  e.  K  ( d  .^  k
) )
5229, 51ax-mp 5 . . . . . 6  |-  ( Z `
 d )  = 
U_ k  e.  K  ( d  .^  k
)
5346, 52eqeq12i 2422 . . . . 5  |-  ( ( ( X  o.  Y
) `  d )  =  ( Z `  d )  <->  U_ i  e.  I  ( U_ j  e.  J  ( d  .^  j )  .^  i
)  =  U_ k  e.  K  ( d  .^  k ) )
5421, 53raleqbii 2848 . . . 4  |-  ( A. d  e.  dom  ( X  o.  Y ) ( ( X  o.  Y
) `  d )  =  ( Z `  d )  <->  A. d  e.  _V  U_ i  e.  I  ( U_ j  e.  J  ( d  .^  j )  .^  i
)  =  U_ k  e.  K  ( d  .^  k ) )
55 comptiunov2.3 . . . . . . 7  |-  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )  C_  U_ k  e.  ( I  u.  J
) ( d  .^  k )
56 iunxun 4355 . . . . . . . 8  |-  U_ k  e.  ( I  u.  J
) ( d  .^  k )  =  (
U_ k  e.  I 
( d  .^  k
)  u.  U_ k  e.  J  ( d  .^  k ) )
57 comptiunov2.1 . . . . . . . . 9  |-  U_ k  e.  I  ( d  .^  k )  C_  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )
58 comptiunov2.2 . . . . . . . . 9  |-  U_ k  e.  J  ( d  .^  k )  C_  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )
5957, 58unssi 3617 . . . . . . . 8  |-  ( U_ k  e.  I  (
d  .^  k )  u.  U_ k  e.  J  ( d  .^  k
) )  C_  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )
6056, 59eqsstri 3471 . . . . . . 7  |-  U_ k  e.  ( I  u.  J
) ( d  .^  k )  C_  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )
6155, 60eqssi 3457 . . . . . 6  |-  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )  =  U_ k  e.  ( I  u.  J ) ( d 
.^  k )
62 iuneq1 4284 . . . . . . 7  |-  ( K  =  ( I  u.  J )  ->  U_ k  e.  K  ( d  .^  k )  =  U_ k  e.  ( I  u.  J ) ( d 
.^  k ) )
6322, 62ax-mp 5 . . . . . 6  |-  U_ k  e.  K  ( d  .^  k )  =  U_ k  e.  ( I  u.  J ) ( d 
.^  k )
6461, 63eqtr4i 2434 . . . . 5  |-  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )  =  U_ k  e.  K  (
d  .^  k )
6564a1i 11 . . . 4  |-  ( d  e.  _V  ->  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )  =  U_ k  e.  K  (
d  .^  k )
)
6654, 65mprgbir 2767 . . 3  |-  A. d  e.  dom  ( X  o.  Y ) ( ( X  o.  Y ) `
 d )  =  ( Z `  d
)
67 eqfunfv 5963 . . . 4  |-  ( ( Fun  ( X  o.  Y )  /\  Fun  Z )  ->  ( ( X  o.  Y )  =  Z  <->  ( dom  ( X  o.  Y )  =  dom  Z  /\  A. d  e.  dom  ( X  o.  Y ) ( ( X  o.  Y
) `  d )  =  ( Z `  d ) ) ) )
6867biimprd 223 . . 3  |-  ( ( Fun  ( X  o.  Y )  /\  Fun  Z )  ->  ( ( dom  ( X  o.  Y
)  =  dom  Z  /\  A. d  e.  dom  ( X  o.  Y
) ( ( X  o.  Y ) `  d )  =  ( Z `  d ) )  ->  ( X  o.  Y )  =  Z ) )
6928, 66, 68mp2ani 676 . 2  |-  ( ( Fun  ( X  o.  Y )  /\  Fun  Z )  ->  ( X  o.  Y )  =  Z )
706, 8, 69mp2an 670 1  |-  ( X  o.  Y )  =  Z
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367    = wceq 1405    e. wcel 1842   A.wral 2753   _Vcvv 3058    u. cun 3411    C_ wss 3413   U_ciun 4270    |-> cmpt 4452   dom cdm 4822   ran crn 4823    o. ccom 4826   Fun wfun 5562   ` cfv 5568  (class class class)co 6277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-reu 2760  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-ov 6280
This theorem is referenced by:  corclrcl  35666  cotrcltrcl  35684  corcltrcl  35698  cotrclrcl  35701
  Copyright terms: Public domain W3C validator