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

Theorem comptiunov2i 36268
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 5638 . . 3  |-  Fun  X
3 comptiunov2.y . . . 4  |-  Y  =  ( b  e.  _V  |->  U_ j  e.  J  ( b  .^  j )
)
43funmpt2 5638 . . 3  |-  Fun  Y
5 funco 5639 . . 3  |-  ( ( Fun  X  /\  Fun  Y )  ->  Fun  ( X  o.  Y ) )
62, 4, 5mp2an 676 . 2  |-  Fun  ( X  o.  Y )
7 comptiunov2.z . . 3  |-  Z  =  ( c  e.  _V  |->  U_ k  e.  K  ( c  .^  k )
)
87funmpt2 5638 . 2  |-  Fun  Z
9 ssv 3484 . . . . . . 7  |-  ran  Y  C_ 
_V
10 comptiunov2.i . . . . . . . . 9  |-  I  e. 
_V
11 ovex 6333 . . . . . . . . 9  |-  ( a 
.^  i )  e. 
_V
1210, 11iunex 6787 . . . . . . . 8  |-  U_ i  e.  I  ( a  .^  i )  e.  _V
1312, 1dmmpti 5725 . . . . . . 7  |-  dom  X  =  _V
149, 13sseqtr4i 3497 . . . . . 6  |-  ran  Y  C_ 
dom  X
15 dmcosseq 5115 . . . . . 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 6333 . . . . . . 7  |-  ( b 
.^  j )  e. 
_V
1917, 18iunex 6787 . . . . . 6  |-  U_ j  e.  J  ( b  .^  j )  e.  _V
2019, 3dmmpti 5725 . . . . 5  |-  dom  Y  =  _V
2116, 20eqtri 2451 . . . 4  |-  dom  ( X  o.  Y )  =  _V
22 comptiunov2.k . . . . . . 7  |-  K  =  ( I  u.  J
)
2310, 17unex 6603 . . . . . . 7  |-  ( I  u.  J )  e. 
_V
2422, 23eqeltri 2503 . . . . . 6  |-  K  e. 
_V
25 ovex 6333 . . . . . 6  |-  ( c 
.^  k )  e. 
_V
2624, 25iunex 6787 . . . . 5  |-  U_ k  e.  K  ( c  .^  k )  e.  _V
2726, 7dmmpti 5725 . . . 4  |-  dom  Z  =  _V
2821, 27eqtr4i 2454 . . 3  |-  dom  ( X  o.  Y )  =  dom  Z
29 vex 3083 . . . . . . . . 9  |-  d  e. 
_V
3029, 20eleqtrri 2506 . . . . . . . 8  |-  d  e. 
dom  Y
31 fvco 5957 . . . . . . . 8  |-  ( ( Fun  Y  /\  d  e.  dom  Y )  -> 
( ( X  o.  Y ) `  d
)  =  ( X `
 ( Y `  d ) ) )
324, 30, 31mp2an 676 . . . . . . 7  |-  ( ( X  o.  Y ) `
 d )  =  ( X `  ( Y `  d )
)
33 oveq1 6312 . . . . . . . . . . 11  |-  ( b  =  d  ->  (
b  .^  j )  =  ( d  .^  j ) )
3433iuneq2d 4326 . . . . . . . . . 10  |-  ( b  =  d  ->  U_ j  e.  J  ( b  .^  j )  =  U_ j  e.  J  (
d  .^  j )
)
35 ovex 6333 . . . . . . . . . . 11  |-  ( d 
.^  j )  e. 
_V
3617, 35iunex 6787 . . . . . . . . . 10  |-  U_ j  e.  J  ( d  .^  j )  e.  _V
3734, 3, 36fvmpt 5964 . . . . . . . . 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 5884 . . . . . . 7  |-  ( X `
 ( Y `  d ) )  =  ( X `  U_ j  e.  J  ( d  .^  j ) )
40 oveq1 6312 . . . . . . . . . 10  |-  ( a  =  U_ j  e.  J  ( d  .^  j )  ->  (
a  .^  i )  =  ( U_ j  e.  J  ( d  .^  j )  .^  i
) )
4140iuneq2d 4326 . . . . . . . . 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 6333 . . . . . . . . . 10  |-  ( U_ j  e.  J  (
d  .^  j )  .^  i )  e.  _V
4310, 42iunex 6787 . . . . . . . . 9  |-  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )  e.  _V
4441, 1, 43fvmpt 5964 . . . . . . . 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 2455 . . . . . 6  |-  ( ( X  o.  Y ) `
 d )  = 
U_ i  e.  I 
( U_ j  e.  J  ( d  .^  j
)  .^  i )
47 oveq1 6312 . . . . . . . . 9  |-  ( c  =  d  ->  (
c  .^  k )  =  ( d  .^  k ) )
4847iuneq2d 4326 . . . . . . . 8  |-  ( c  =  d  ->  U_ k  e.  K  ( c  .^  k )  =  U_ k  e.  K  (
d  .^  k )
)
49 ovex 6333 . . . . . . . . 9  |-  ( d 
.^  k )  e. 
_V
5024, 49iunex 6787 . . . . . . . 8  |-  U_ k  e.  K  ( d  .^  k )  e.  _V
5148, 7, 50fvmpt 5964 . . . . . . 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 2442 . . . . 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 2867 . . . 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 4384 . . . . . . . 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 3641 . . . . . . . 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 3494 . . . . . . 7  |-  U_ k  e.  ( I  u.  J
) ( d  .^  k )  C_  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )
6155, 60eqssi 3480 . . . . . 6  |-  U_ i  e.  I  ( U_ j  e.  J  (
d  .^  j )  .^  i )  =  U_ k  e.  ( I  u.  J ) ( d 
.^  k )
62 iuneq1 4313 . . . . . . 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 2454 . . . . 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 2786 . . 3  |-  A. d  e.  dom  ( X  o.  Y ) ( ( X  o.  Y ) `
 d )  =  ( Z `  d
)
67 eqfunfv 5996 . . . 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 226 . . 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 682 . 2  |-  ( ( Fun  ( X  o.  Y )  /\  Fun  Z )  ->  ( X  o.  Y )  =  Z )
706, 8, 69mp2an 676 1  |-  ( X  o.  Y )  =  Z
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2771   _Vcvv 3080    u. cun 3434    C_ wss 3436   U_ciun 4299    |-> cmpt 4482   dom cdm 4853   ran crn 4854    o. ccom 4857   Fun wfun 5595   ` cfv 5601  (class class class)co 6305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308
This theorem is referenced by:  corclrcl  36269  cotrcltrcl  36287  corcltrcl  36301  cotrclrcl  36304
  Copyright terms: Public domain W3C validator