Metamath Proof Explorer

Theorem comptiunov2i

Description: The composition two indexed unions is sometimes a similar indexed union. (Contributed by RP, 10-Jun-2020)

Ref Expression
Hypotheses 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 comptiunov2i 
|- ( X o. Y ) = Z

Proof

Step Hyp Ref Expression
1 comptiunov2.x 
 |-  X = ( a e. _V |-> U_ i e. I ( a .^ i ) )
2 comptiunov2.y 
 |-  Y = ( b e. _V |-> U_ j e. J ( b .^ j ) )
3 comptiunov2.z 
 |-  Z = ( c e. _V |-> U_ k e. K ( c .^ k ) )
4 comptiunov2.i 
 |-  I e. _V
5 comptiunov2.j 
 |-  J e. _V
6 comptiunov2.k 
 |-  K = ( I u. J )
7 comptiunov2.1 
 |-  U_ k e. I ( d .^ k ) C_ U_ i e. I ( U_ j e. J ( d .^ j ) .^ i )
8 comptiunov2.2 
 |-  U_ k e. J ( d .^ k ) C_ U_ i e. I ( U_ j e. J ( d .^ j ) .^ i )
9 comptiunov2.3 
 |-  U_ i e. I ( U_ j e. J ( d .^ j ) .^ i ) C_ U_ k e. ( I u. J ) ( d .^ k )
10 1 funmpt2 
 |-  Fun X
11 2 funmpt2 
 |-  Fun Y
12 funco 
 |-  ( ( Fun X /\ Fun Y ) -> Fun ( X o. Y ) )
13 10 11 12 mp2an 
 |-  Fun ( X o. Y )
14 3 funmpt2 
 |-  Fun Z
15 ssv 
 |-  ran Y C_ _V
16 ovex 
 |-  ( a .^ i ) e. _V
17 4 16 iunex 
 |-  U_ i e. I ( a .^ i ) e. _V
18 17 1 dmmpti 
 |-  dom X = _V
19 15 18 sseqtrri 
 |-  ran Y C_ dom X
20 dmcosseq 
 |-  ( ran Y C_ dom X -> dom ( X o. Y ) = dom Y )
21 19 20 ax-mp 
 |-  dom ( X o. Y ) = dom Y
22 ovex 
 |-  ( b .^ j ) e. _V
23 5 22 iunex 
 |-  U_ j e. J ( b .^ j ) e. _V
24 23 2 dmmpti 
 |-  dom Y = _V
25 21 24 eqtri 
 |-  dom ( X o. Y ) = _V
26 4 5 unex 
 |-  ( I u. J ) e. _V
27 6 26 eqeltri 
 |-  K e. _V
28 ovex 
 |-  ( c .^ k ) e. _V
29 27 28 iunex 
 |-  U_ k e. K ( c .^ k ) e. _V
30 29 3 dmmpti 
 |-  dom Z = _V
31 25 30 eqtr4i 
 |-  dom ( X o. Y ) = dom Z
32 vex 
 |-  d e. _V
33 32 24 eleqtrri 
 |-  d e. dom Y
34 fvco 
 |-  ( ( Fun Y /\ d e. dom Y ) -> ( ( X o. Y ) ` d ) = ( X ` ( Y ` d ) ) )
35 11 33 34 mp2an 
 |-  ( ( X o. Y ) ` d ) = ( X ` ( Y ` d ) )
36 oveq1 
 |-  ( b = d -> ( b .^ j ) = ( d .^ j ) )
37 36 iuneq2d 
 |-  ( b = d -> U_ j e. J ( b .^ j ) = U_ j e. J ( d .^ j ) )
38 ovex 
 |-  ( d .^ j ) e. _V
39 5 38 iunex 
 |-  U_ j e. J ( d .^ j ) e. _V
40 37 2 39 fvmpt 
 |-  ( d e. _V -> ( Y ` d ) = U_ j e. J ( d .^ j ) )
41 40 elv 
 |-  ( Y ` d ) = U_ j e. J ( d .^ j )
42 41 fveq2i 
 |-  ( X ` ( Y ` d ) ) = ( X ` U_ j e. J ( d .^ j ) )
43 oveq1 
 |-  ( a = U_ j e. J ( d .^ j ) -> ( a .^ i ) = ( U_ j e. J ( d .^ j ) .^ i ) )
44 43 iuneq2d 
 |-  ( a = U_ j e. J ( d .^ j ) -> U_ i e. I ( a .^ i ) = U_ i e. I ( U_ j e. J ( d .^ j ) .^ i ) )
45 ovex 
 |-  ( U_ j e. J ( d .^ j ) .^ i ) e. _V
46 4 45 iunex 
 |-  U_ i e. I ( U_ j e. J ( d .^ j ) .^ i ) e. _V
47 44 1 46 fvmpt 
 |-  ( 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 ) )
48 39 47 ax-mp 
 |-  ( X ` U_ j e. J ( d .^ j ) ) = U_ i e. I ( U_ j e. J ( d .^ j ) .^ i )
49 35 42 48 3eqtri 
 |-  ( ( X o. Y ) ` d ) = U_ i e. I ( U_ j e. J ( d .^ j ) .^ i )
50 oveq1 
 |-  ( c = d -> ( c .^ k ) = ( d .^ k ) )
51 50 iuneq2d 
 |-  ( c = d -> U_ k e. K ( c .^ k ) = U_ k e. K ( d .^ k ) )
52 ovex 
 |-  ( d .^ k ) e. _V
53 27 52 iunex 
 |-  U_ k e. K ( d .^ k ) e. _V
54 51 3 53 fvmpt 
 |-  ( d e. _V -> ( Z ` d ) = U_ k e. K ( d .^ k ) )
55 54 elv 
 |-  ( Z ` d ) = U_ k e. K ( d .^ k )
56 49 55 eqeq12i 
 |-  ( ( ( X o. Y ) ` d ) = ( Z ` d ) <-> U_ i e. I ( U_ j e. J ( d .^ j ) .^ i ) = U_ k e. K ( d .^ k ) )
57 25 56 raleqbii 
 |-  ( 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 ) )
58 iunxun 
 |-  U_ k e. ( I u. J ) ( d .^ k ) = ( U_ k e. I ( d .^ k ) u. U_ k e. J ( d .^ k ) )
59 7 8 unssi 
 |-  ( 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 )
60 58 59 eqsstri 
 |-  U_ k e. ( I u. J ) ( d .^ k ) C_ U_ i e. I ( U_ j e. J ( d .^ j ) .^ i )
61 9 60 eqssi 
 |-  U_ i e. I ( U_ j e. J ( d .^ j ) .^ i ) = U_ k e. ( I u. J ) ( d .^ k )
62 iuneq1 
 |-  ( K = ( I u. J ) -> U_ k e. K ( d .^ k ) = U_ k e. ( I u. J ) ( d .^ k ) )
63 6 62 ax-mp 
 |-  U_ k e. K ( d .^ k ) = U_ k e. ( I u. J ) ( d .^ k )
64 61 63 eqtr4i 
 |-  U_ i e. I ( U_ j e. J ( d .^ j ) .^ i ) = U_ k e. K ( d .^ k )
65 64 a1i 
 |-  ( d e. _V -> U_ i e. I ( U_ j e. J ( d .^ j ) .^ i ) = U_ k e. K ( d .^ k ) )
66 57 65 mprgbir 
 |-  A. d e. dom ( X o. Y ) ( ( X o. Y ) ` d ) = ( Z ` d )
67 eqfunfv 
 |-  ( ( 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 ) ) ) )
68 67 biimprd 
 |-  ( ( 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 ) )
69 31 66 68 mp2ani 
 |-  ( ( Fun ( X o. Y ) /\ Fun Z ) -> ( X o. Y ) = Z )
70 13 14 69 mp2an 
 |-  ( X o. Y ) = Z