Theorem carsgclctunlem3 28447

Description: Lemma for carsgclctun 28448. (Contributed by Thierry Arnoux, 24-May-2020.)

Hypotheses

Ref	Expression
carsgval.1	|- ( ph -> O e. V )
carsgval.2	|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
carsgsiga.1	|- ( ph -> ( M ` (/) ) = 0 )
carsgsiga.2	|- ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )
carsgsiga.3	|- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
carsgclctun.1	|- ( ph -> A ~<_ om )
carsgclctun.2	|- ( ph -> A C_ (toCaraSiga ` M ) )
carsgclctunlem3.1	|- ( ph -> E e. ~P O )

Assertion

Ref	Expression
carsgclctunlem3	|- ( ph -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )

Distinct variable groups:   x, A, y   x, E, y   x, M, y   x, O, y   ph, x, y

Allowed substitution hints:   V( x, y)

Proof of Theorem carsgclctunlem3

Dummy variables e f k n z g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iccssxr 11528	. . . . . . 7 |- ( 0 [,] +oo ) C_ RR*
2		carsgval.2	. . . . . . . 8 |- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3		carsgclctunlem3.1	. . . . . . . . 9 |- ( ph -> E e. ~P O )
4	3	elpwincl1 27539	. . . . . . . 8 |- ( ph -> ( E i^i U. A ) e. ~P O )
5	2, 4	ffvelrnd 5934	. . . . . . 7 |- ( ph -> ( M ` ( E i^i U. A ) ) e. ( 0 [,] +oo ) )
6	1, 5	sseldi 3415	. . . . . 6 |- ( ph -> ( M ` ( E i^i U. A ) ) e. RR* )
7	3	elpwdifcl 27540	. . . . . . . 8 |- ( ph -> ( E \ U. A ) e. ~P O )
8	2, 7	ffvelrnd 5934	. . . . . . 7 |- ( ph -> ( M ` ( E \ U. A ) ) e. ( 0 [,] +oo ) )
9	1, 8	sseldi 3415	. . . . . 6 |- ( ph -> ( M ` ( E \ U. A ) ) e. RR* )
10	6, 9	xaddcld 11414	. . . . 5 |- ( ph -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) e. RR* )
11	10	adantr 463	. . . 4 |- ( ( ph /\ ( M ` E ) = +oo ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) e. RR* )
12		pnfge 11260	. . . 4 |- ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) e. RR* -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ +oo )
13	11, 12	syl 16	. . 3 |- ( ( ph /\ ( M ` E ) = +oo ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ +oo )
14		simpr 459	. . 3 |- ( ( ph /\ ( M ` E ) = +oo ) -> ( M ` E ) = +oo )
15	13, 14	breqtrrd 4393	. 2 |- ( ( ph /\ ( M ` E ) = +oo ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
16		unieq 4171	. . . . . . . . . . . . 13 |- ( A = (/) -> U. A = U. (/) )
17		uni0 4190	. . . . . . . . . . . . 13 |- U. (/) = (/)
18	16, 17	syl6eq 2439	. . . . . . . . . . . 12 |- ( A = (/) -> U. A = (/) )
19	18	ineq2d 3614	. . . . . . . . . . 11 |- ( A = (/) -> ( E i^i U. A ) = ( E i^i (/) ) )
20		in0 3738	. . . . . . . . . . 11 |- ( E i^i (/) ) = (/)
21	19, 20	syl6eq 2439	. . . . . . . . . 10 |- ( A = (/) -> ( E i^i U. A ) = (/) )
22	21	fveq2d 5778	. . . . . . . . 9 |- ( A = (/) -> ( M ` ( E i^i U. A ) ) = ( M ` (/) ) )
23	18	difeq2d 3536	. . . . . . . . . . 11 |- ( A = (/) -> ( E \ U. A ) = ( E \ (/) ) )
24		dif0 3814	. . . . . . . . . . 11 |- ( E \ (/) ) = E
25	23, 24	syl6eq 2439	. . . . . . . . . 10 |- ( A = (/) -> ( E \ U. A ) = E )
26	25	fveq2d 5778	. . . . . . . . 9 |- ( A = (/) -> ( M ` ( E \ U. A ) ) = ( M ` E ) )
27	22, 26	oveq12d 6214	. . . . . . . 8 |- ( A = (/) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) = ( ( M ` (/) ) +e ( M ` E ) ) )
28	27	adantl 464	. . . . . . 7 |- ( ( ph /\ A = (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) = ( ( M ` (/) ) +e ( M ` E ) ) )
29		carsgsiga.1	. . . . . . . . 9 |- ( ph -> ( M ` (/) ) = 0 )
30	29	adantr 463	. . . . . . . 8 |- ( ( ph /\ A = (/) ) -> ( M ` (/) ) = 0 )
31	30	oveq1d 6211	. . . . . . 7 |- ( ( ph /\ A = (/) ) -> ( ( M ` (/) ) +e ( M ` E ) ) = ( 0 +e ( M ` E ) ) )
32	2, 3	ffvelrnd 5934	. . . . . . . . . 10 |- ( ph -> ( M ` E ) e. ( 0 [,] +oo ) )
33	1, 32	sseldi 3415	. . . . . . . . 9 |- ( ph -> ( M ` E ) e. RR* )
34	33	adantr 463	. . . . . . . 8 |- ( ( ph /\ A = (/) ) -> ( M ` E ) e. RR* )
35		xaddid2 11360	. . . . . . . 8 |- ( ( M ` E ) e. RR* -> ( 0 +e ( M ` E ) ) = ( M ` E ) )
36	34, 35	syl 16	. . . . . . 7 |- ( ( ph /\ A = (/) ) -> ( 0 +e ( M ` E ) ) = ( M ` E ) )
37	28, 31, 36	3eqtrd 2427	. . . . . 6 |- ( ( ph /\ A = (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) = ( M ` E ) )
38	37, 34	eqeltrd 2470	. . . . . . 7 |- ( ( ph /\ A = (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) e. RR* )
39		xeqlelt 27740	. . . . . . 7 |- ( ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) e. RR* /\ ( M ` E ) e. RR* ) -> ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) = ( M ` E ) <-> ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) /\ -. ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) < ( M ` E ) ) ) )
40	38, 34, 39	syl2anc 659	. . . . . 6 |- ( ( ph /\ A = (/) ) -> ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) = ( M ` E ) <-> ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) /\ -. ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) < ( M ` E ) ) ) )
41	37, 40	mpbid 210	. . . . 5 |- ( ( ph /\ A = (/) ) -> ( ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) /\ -. ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) < ( M ` E ) ) )
42	41	simpld 457	. . . 4 |- ( ( ph /\ A = (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
43	42	adantlr 712	. . 3 |- ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A = (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
44		carsgclctun.2	. . . . . . . 8 |- ( ph -> A C_ (toCaraSiga ` M ) )
45		fvex 5784	. . . . . . . . 9 |- (toCaraSiga ` M ) e. _V
46		ssexg 4511	. . . . . . . . 9 |- ( ( A C_ (toCaraSiga ` M ) /\ (toCaraSiga ` M ) e. _V ) -> A e. _V )
47	45, 46	mpan2 669	. . . . . . . 8 |- ( A C_ (toCaraSiga ` M ) -> A e. _V )
48		0sdomg 7565	. . . . . . . 8 |- ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
49	44, 47, 48	3syl 20	. . . . . . 7 |- ( ph -> ( (/) ~< A <-> A =/= (/) ) )
50	49	biimpar 483	. . . . . 6 |- ( ( ph /\ A =/= (/) ) -> (/) ~< A )
51	50	adantlr 712	. . . . 5 |- ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) -> (/) ~< A )
52		carsgclctun.1	. . . . . . 7 |- ( ph -> A ~<_ om )
53		nnenom 11993	. . . . . . . 8 |- NN ~~ om
54		ensymb 7482	. . . . . . . 8 |- ( NN ~~ om <-> om ~~ NN )
55	53, 54	mpbi 208	. . . . . . 7 |- om ~~ NN
56		domentr 7493	. . . . . . 7 |- ( ( A ~<_ om /\ om ~~ NN ) -> A ~<_ NN )
57	52, 55, 56	sylancl 660	. . . . . 6 |- ( ph -> A ~<_ NN )
58	57	ad2antrr 723	. . . . 5 |- ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) -> A ~<_ NN )
59		fodomr 7587	. . . . 5 |- ( ( (/) ~< A /\ A ~<_ NN ) -> E. f f : NN -onto-> A )
60	51, 58, 59	syl2anc 659	. . . 4 |- ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) -> E. f f : NN -onto-> A )
61		fveq2 5774	. . . . . . . . . 10 |- ( n = k -> ( f ` n ) = ( f ` k ) )
62	61	iundisj 22043	. . . . . . . . 9 |- U_ n e. NN ( f ` n ) = U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) )
63		fofn 5705	. . . . . . . . . . . 12 |- ( f : NN -onto-> A -> f Fn NN )
64		fniunfv 6060	. . . . . . . . . . . 12 |- ( f Fn NN -> U_ n e. NN ( f ` n ) = U. ran f )
65	63, 64	syl 16	. . . . . . . . . . 11 |- ( f : NN -onto-> A -> U_ n e. NN ( f ` n ) = U. ran f )
66		forn 5706	. . . . . . . . . . . 12 |- ( f : NN -onto-> A -> ran f = A )
67	66	unieqd 4173	. . . . . . . . . . 11 |- ( f : NN -onto-> A -> U. ran f = U. A )
68	65, 67	eqtrd 2423	. . . . . . . . . 10 |- ( f : NN -onto-> A -> U_ n e. NN ( f ` n ) = U. A )
69	68	adantl 464	. . . . . . . . 9 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> U_ n e. NN ( f ` n ) = U. A )
70	62, 69	syl5eqr 2437	. . . . . . . 8 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) = U. A )
71	70	ineq2d 3614	. . . . . . 7 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( E i^i U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) ) = ( E i^i U. A ) )
72	71	fveq2d 5778	. . . . . 6 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( M ` ( E i^i U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) ) ) = ( M ` ( E i^i U. A ) ) )
73	70	difeq2d 3536	. . . . . . 7 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( E \ U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) ) = ( E \ U. A ) )
74	73	fveq2d 5778	. . . . . 6 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( M ` ( E \ U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) ) ) = ( M ` ( E \ U. A ) ) )
75	72, 74	oveq12d 6214	. . . . 5 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( ( M ` ( E i^i U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) ) ) +e ( M ` ( E \ U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) ) ) ) = ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) )
76		carsgval.1	. . . . . . 7 |- ( ph -> O e. V )
77	76	ad3antrrr 727	. . . . . 6 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> O e. V )
78	2	ad3antrrr 727	. . . . . 6 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> M : ~P O --> ( 0 [,] +oo ) )
79	29	ad3antrrr 727	. . . . . 6 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( M ` (/) ) = 0 )
80		carsgsiga.2	. . . . . . . . 9 |- ( ( ph /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )
81	80	3adant1r 1219	. . . . . . . 8 |- ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )
82	81	3adant1r 1219	. . . . . . 7 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )
83	82	3adant1r 1219	. . . . . 6 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )
84		carsgsiga.3	. . . . . . . . 9 |- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
85	84	3adant1r 1219	. . . . . . . 8 |- ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
86	85	3adant1r 1219	. . . . . . 7 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
87	86	3adant1r 1219	. . . . . 6 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
88	61	iundisj2 22044	. . . . . . 7 |- Disj n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) )
89	88	a1i 11	. . . . . 6 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> Disj n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) )
90	77	adantr 463	. . . . . . 7 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> O e. V )
91	78	adantr 463	. . . . . . 7 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> M : ~P O --> ( 0 [,] +oo ) )
92	44	ad4antr 729	. . . . . . . 8 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> A C_ (toCaraSiga ` M ) )
93		fof 5703	. . . . . . . . . 10 |- ( f : NN -onto-> A -> f : NN --> A )
94	93	ad2antlr 724	. . . . . . . . 9 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> f : NN --> A )
95		simpr 459	. . . . . . . . 9 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> n e. NN )
96	94, 95	ffvelrnd 5934	. . . . . . . 8 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ( f ` n ) e. A )
97	92, 96	sseldd 3418	. . . . . . 7 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ( f ` n ) e. (toCaraSiga ` M ) )
98	79	adantr 463	. . . . . . . 8 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ( M ` (/) ) = 0 )
99	83	3adant1r 1219	. . . . . . . 8 |- ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ x ~<_ om /\ x C_ ~P O ) -> ( M ` U. x ) <_ Σ* y e. x ( M ` y ) )
100	90, 91, 98, 99	carsgsigalem 28442	. . . . . . 7 |- ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ e e. ~P O /\ g e. ~P O ) -> ( M ` ( e u. g ) ) <_ ( ( M ` e ) +e ( M ` g ) ) )
101	93	ad3antlr 728	. . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ k e. ( 1..^ n ) ) -> f : NN --> A )
102		fzossnn 11765	. . . . . . . . . . . . 13 |- ( 1..^ n ) C_ NN
103	102	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ( 1..^ n ) C_ NN )
104	103	sselda 3417	. . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ k e. ( 1..^ n ) ) -> k e. NN )
105	101, 104	ffvelrnd 5934	. . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ k e. ( 1..^ n ) ) -> ( f ` k ) e. A )
106	105	ralrimiva 2796	. . . . . . . . 9 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> A. k e. ( 1..^ n ) ( f ` k ) e. A )
107		dfiun2g 4275	. . . . . . . . 9 |- ( A. k e. ( 1..^ n ) ( f ` k ) e. A -> U_ k e. ( 1..^ n ) ( f ` k ) = U. { z | E. k e. ( 1..^ n ) z = ( f ` k ) } )
108	106, 107	syl 16	. . . . . . . 8 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> U_ k e. ( 1..^ n ) ( f ` k ) = U. { z | E. k e. ( 1..^ n ) z = ( f ` k ) } )
109		eqid 2382	. . . . . . . . . . . 12 |- ( k e. ( 1..^ n ) |-> ( f ` k ) ) = ( k e. ( 1..^ n ) |-> ( f ` k ) )
110	109	rnmpt 5161	. . . . . . . . . . 11 |- ran ( k e. ( 1..^ n ) |-> ( f ` k ) ) = { z | E. k e. ( 1..^ n ) z = ( f ` k ) }
111		fzofi 11987	. . . . . . . . . . . 12 |- ( 1..^ n ) e. Fin
112		mptfi 7734	. . . . . . . . . . . 12 |- ( ( 1..^ n ) e. Fin -> ( k e. ( 1..^ n ) |-> ( f ` k ) ) e. Fin )
113		rnfi 7720	. . . . . . . . . . . 12 |- ( ( k e. ( 1..^ n ) |-> ( f ` k ) ) e. Fin -> ran ( k e. ( 1..^ n ) |-> ( f ` k ) ) e. Fin )
114	111, 112, 113	mp2b 10	. . . . . . . . . . 11 |- ran ( k e. ( 1..^ n ) |-> ( f ` k ) ) e. Fin
115	110, 114	eqeltrri 2467	. . . . . . . . . 10 |- { z | E. k e. ( 1..^ n ) z = ( f ` k ) } e. Fin
116	115	a1i 11	. . . . . . . . 9 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> { z | E. k e. ( 1..^ n ) z = ( f ` k ) } e. Fin )
117	92	adantr 463	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ k e. ( 1..^ n ) ) -> A C_ (toCaraSiga ` M ) )
118	117, 105	sseldd 3418	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) /\ k e. ( 1..^ n ) ) -> ( f ` k ) e. (toCaraSiga ` M ) )
119	118	ralrimiva 2796	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> A. k e. ( 1..^ n ) ( f ` k ) e. (toCaraSiga ` M ) )
120	109	rnmptss 5962	. . . . . . . . . . 11 |- ( A. k e. ( 1..^ n ) ( f ` k ) e. (toCaraSiga ` M ) -> ran ( k e. ( 1..^ n ) |-> ( f ` k ) ) C_ (toCaraSiga ` M ) )
121	119, 120	syl 16	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ran ( k e. ( 1..^ n ) |-> ( f ` k ) ) C_ (toCaraSiga ` M ) )
122	110, 121	syl5eqssr 3462	. . . . . . . . 9 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> { z | E. k e. ( 1..^ n ) z = ( f ` k ) } C_ (toCaraSiga ` M ) )
123	90, 91, 98, 99, 116, 122	fiunelcarsg 28443	. . . . . . . 8 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> U. { z | E. k e. ( 1..^ n ) z = ( f ` k ) } e. (toCaraSiga ` M ) )
124	108, 123	eqeltrd 2470	. . . . . . 7 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> U_ k e. ( 1..^ n ) ( f ` k ) e. (toCaraSiga ` M ) )
125	90, 91, 97, 100, 124	difelcarsg2 28440	. . . . . 6 |- ( ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) /\ n e. NN ) -> ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) e. (toCaraSiga ` M ) )
126	3	ad3antrrr 727	. . . . . 6 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> E e. ~P O )
127		simpllr 758	. . . . . 6 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( M ` E ) =/= +oo )
128	77, 78, 79, 83, 87, 89, 125, 126, 127	carsgclctunlem2 28446	. . . . 5 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( ( M ` ( E i^i U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) ) ) +e ( M ` ( E \ U_ n e. NN ( ( f ` n ) \ U_ k e. ( 1..^ n ) ( f ` k ) ) ) ) ) <_ ( M ` E ) )
129	75, 128	eqbrtrrd 4389	. . . 4 |- ( ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) /\ f : NN -onto-> A ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
130	60, 129	exlimddv 1734	. . 3 |- ( ( ( ph /\ ( M ` E ) =/= +oo ) /\ A =/= (/) ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
131	43, 130	pm2.61dane 2700	. 2 |- ( ( ph /\ ( M ` E ) =/= +oo ) -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )
132	15, 131	pm2.61dane 2700	1 |- ( ph -> ( ( M ` ( E i^i U. A ) ) +e ( M ` ( E \ U. A ) ) ) <_ ( M ` E ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   /\ w3a 971   = wceq 1399   E.wex 1620   e. wcel 1826   {cab 2367   =/= wne 2577   A.wral 2732   E.wrex 2733   _Vcvv 3034   \ cdif 3386   i^i cin 3388   C_ wss 3389   (/)c0 3711   ~Pcpw 3927   U.cuni 4163   U_ciun 4243  Disj wdisj 4338   class class class wbr 4367   |-> cmpt 4425   ran crn 4914   Fn wfn 5491   -->wf 5492   -onto->wfo 5494   ` cfv 5496  (class class class)co 6196   omcom 6599   ~~ cen 7432   ~<_ cdom 7433   ~< csdm 7434   Fincfn 7435   0cc0 9403   1c1 9404   +oocpnf 9536   RR*cxr 9538   < clt 9539   <_ cle 9540   NNcn 10452   +ecxad 11237   [,]cicc 11453  ..^cfzo 11717  Σ^*cesum 28175  toCaraSigaccarsg 28428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-inf2 7972  ax-ac2 8756  ax-cnex 9459  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479  ax-pre-mulgt0 9480  ax-pre-sup 9481  ax-addf 9482  ax-mulf 9483

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-fal 1405  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-iin 4246  df-disj 4339  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-se 4753  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-isom 5505  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-of 6439  df-om 6600  df-1st 6699  df-2nd 6700  df-supp 6818  df-recs 6960  df-rdg 6994  df-1o 7048  df-2o 7049  df-oadd 7052  df-er 7229  df-map 7340  df-pm 7341  df-ixp 7389  df-en 7436  df-dom 7437  df-sdom 7438  df-fin 7439  df-fsupp 7745  df-fi 7786  df-sup 7816  df-oi 7850  df-card 8233  df-acn 8236  df-ac 8410  df-cda 8461  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-sub 9720  df-neg 9721  df-div 10124  df-nn 10453  df-2 10511  df-3 10512  df-4 10513  df-5 10514  df-6 10515  df-7 10516  df-8 10517  df-9 10518  df-10 10519  df-n0 10713  df-z 10782  df-dec 10896  df-uz 11002  df-q 11102  df-rp 11140  df-xneg 11239  df-xadd 11240  df-xmul 11241  df-ioo 11454  df-ioc 11455  df-ico 11456  df-icc 11457  df-fz 11594  df-fzo 11718  df-fl 11828  df-mod 11897  df-seq 12011  df-exp 12070  df-fac 12256  df-bc 12283  df-hash 12308  df-shft 12902  df-cj 12934  df-re 12935  df-im 12936  df-sqrt 13070  df-abs 13071  df-limsup 13296  df-clim 13313  df-rlim 13314  df-sum 13511  df-ef 13805  df-sin 13807  df-cos 13808  df-pi 13810  df-struct 14636  df-ndx 14637  df-slot 14638  df-base 14639  df-sets 14640  df-ress 14641  df-plusg 14715  df-mulr 14716  df-starv 14717  df-sca 14718  df-vsca 14719  df-ip 14720  df-tset 14721  df-ple 14722  df-ds 14724  df-unif 14725  df-hom 14726  df-cco 14727  df-rest 14830  df-topn 14831  df-0g 14849  df-gsum 14850  df-topgen 14851  df-pt 14852  df-prds 14855  df-ordt 14908  df-xrs 14909  df-qtop 14914  df-imas 14915  df-xps 14917  df-mre 14993  df-mrc 14994  df-acs 14996  df-ps 15947  df-tsr 15948  df-plusf 15988  df-mgm 15989  df-sgrp 16028  df-mnd 16038  df-mhm 16083  df-submnd 16084  df-grp 16174  df-minusg 16175  df-sbg 16176  df-mulg 16177  df-subg 16315  df-cntz 16472  df-cmn 16917  df-abl 16918  df-mgp 17255  df-ur 17267  df-ring 17313  df-cring 17314  df-subrg 17540  df-abv 17579  df-lmod 17627  df-scaf 17628  df-sra 17931  df-rgmod 17932  df-psmet 18524  df-xmet 18525  df-met 18526  df-bl 18527  df-mopn 18528  df-fbas 18529  df-fg 18530  df-cnfld 18534  df-top 19484  df-bases 19486  df-topon 19487  df-topsp 19488  df-cld 19605  df-ntr 19606  df-cls 19607  df-nei 19685  df-lp 19723  df-perf 19724  df-cn 19814  df-cnp 19815  df-haus 19902  df-tx 20148  df-hmeo 20341  df-fil 20432  df-fm 20524  df-flim 20525  df-flf 20526  df-tmd 20656  df-tgp 20657  df-tsms 20710  df-trg 20747  df-xms 20908  df-ms 20909  df-tms 20910  df-nm 21188  df-ngp 21189  df-nrg 21191  df-nlm 21192  df-ii 21466  df-cncf 21467  df-limc 22355  df-dv 22356  df-log 23029  df-esum 28176  df-carsg 28429

This theorem is referenced by:  carsgclctun  28448