Theorem comptiunov2i 37998

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

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

Syntax hints:   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   u. cun 3572   C_ wss 3574   U_ciun 4520   |-> cmpt 4729   dom cdm 5114   ran crn 5115   o. ccom 5118   Fun wfun 5882   ` cfv 5888  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653

This theorem is referenced by:  corclrcl  37999  cotrcltrcl  38017  corcltrcl  38031  cotrclrcl  38034