Theorem ulmss 24151

Description: A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.)

Hypotheses

Ref	Expression
ulmss.z	|- Z = ( ZZ>= ` M )
ulmss.t	|- ( ph -> T C_ S )
ulmss.a	|- ( ( ph /\ x e. Z ) -> A e. W )
ulmss.u	|- ( ph -> ( x e. Z |-> A ) ( ~~> u ` S ) G )

Assertion

Ref	Expression
ulmss	|- ( ph -> ( x e. Z |-> ( A |` T ) ) ( ~~> u ` T ) ( G |` T ) )

Distinct variable groups:   x, T   ph, x   x, S   x, Z

Allowed substitution hints:   A( x)   G( x)   M( x)   W( x)

Proof of Theorem ulmss

Dummy variables j k m r z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ulmss.u	. 2 |- ( ph -> ( x e. Z |-> A ) ( ~~> u ` S ) G )
2		ulmss.z	. . . . . . . . 9 |- Z = ( ZZ>= ` M )
3	2	uztrn2 11705	. . . . . . . 8 |- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
4		ulmss.t	. . . . . . . . . . 11 |- ( ph -> T C_ S )
5	4	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ k e. Z ) -> T C_ S )
6		ssralv 3666	. . . . . . . . . 10 |- ( T C_ S -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
7	5, 6	syl 17	. . . . . . . . 9 |- ( ( ph /\ k e. Z ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
8		fvres 6207	. . . . . . . . . . . . . . 15 |- ( z e. T -> ( ( A |` T ) ` z ) = ( A ` z ) )
9	8	ad2antll 765	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( A |` T ) ` z ) = ( A ` z ) )
10		simprl 794	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> x e. Z )
11		ulmss.a	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. Z ) -> A e. W )
12	11	adantrr 753	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> A e. W )
13		resexg 5442	. . . . . . . . . . . . . . . . 17 |- ( A e. W -> ( A |` T ) e. _V )
14	12, 13	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( A |` T ) e. _V )
15		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( x e. Z |-> ( A |` T ) ) = ( x e. Z |-> ( A |` T ) )
16	15	fvmpt2 6291	. . . . . . . . . . . . . . . 16 |- ( ( x e. Z /\ ( A |` T ) e. _V ) -> ( ( x e. Z |-> ( A |` T ) ) ` x ) = ( A |` T ) )
17	10, 14, 16	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( x e. Z |-> ( A |` T ) ) ` x ) = ( A |` T ) )
18	17	fveq1d 6193	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( A |` T ) ` z ) )
19		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( x e. Z |-> A ) = ( x e. Z |-> A )
20	19	fvmpt2 6291	. . . . . . . . . . . . . . . 16 |- ( ( x e. Z /\ A e. W ) -> ( ( x e. Z |-> A ) ` x ) = A )
21	10, 12, 20	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( x e. Z |-> A ) ` x ) = A )
22	21	fveq1d 6193	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> A ) ` x ) ` z ) = ( A ` z ) )
23	9, 18, 22	3eqtr4d 2666	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) )
24	23	ralrimivva 2971	. . . . . . . . . . . 12 |- ( ph -> A. x e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) )
25		nfv 1843	. . . . . . . . . . . . 13 |- F/ k A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z )
26		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ x T
27		nffvmpt1 6199	. . . . . . . . . . . . . . . 16 |- F/_ x ( ( x e. Z |-> ( A |` T ) ) ` k )
28		nfcv 2764	. . . . . . . . . . . . . . . 16 |- F/_ x z
29	27, 28	nffv 6198	. . . . . . . . . . . . . . 15 |- F/_ x ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z )
30		nffvmpt1 6199	. . . . . . . . . . . . . . . 16 |- F/_ x ( ( x e. Z |-> A ) ` k )
31	30, 28	nffv 6198	. . . . . . . . . . . . . . 15 |- F/_ x ( ( ( x e. Z |-> A ) ` k ) ` z )
32	29, 31	nfeq 2776	. . . . . . . . . . . . . 14 |- F/ x ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z )
33	26, 32	nfral 2945	. . . . . . . . . . . . 13 |- F/ x A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z )
34		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( x = k -> ( ( x e. Z |-> ( A |` T ) ) ` x ) = ( ( x e. Z |-> ( A |` T ) ) ` k ) )
35	34	fveq1d 6193	. . . . . . . . . . . . . . 15 |- ( x = k -> ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) )
36		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( x = k -> ( ( x e. Z |-> A ) ` x ) = ( ( x e. Z |-> A ) ` k ) )
37	36	fveq1d 6193	. . . . . . . . . . . . . . 15 |- ( x = k -> ( ( ( x e. Z |-> A ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) )
38	35, 37	eqeq12d 2637	. . . . . . . . . . . . . 14 |- ( x = k -> ( ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) <-> ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) )
39	38	ralbidv 2986	. . . . . . . . . . . . 13 |- ( x = k -> ( A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) <-> A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) )
40	25, 33, 39	cbvral 3167	. . . . . . . . . . . 12 |- ( A. x e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) <-> A. k e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) )
41	24, 40	sylib 208	. . . . . . . . . . 11 |- ( ph -> A. k e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) )
42	41	r19.21bi 2932	. . . . . . . . . 10 |- ( ( ph /\ k e. Z ) -> A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) )
43		oveq1 6657	. . . . . . . . . . . . 13 |- ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) -> ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) = ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) )
44	43	fveq2d 6195	. . . . . . . . . . . 12 |- ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) -> ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) = ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) )
45	44	breq1d 4663	. . . . . . . . . . 11 |- ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) -> ( ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
46	45	ralimi 2952	. . . . . . . . . 10 |- ( A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) -> A. z e. T ( ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
47		ralbi 3068	. . . . . . . . . 10 |- ( A. z e. T ( ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) -> ( A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
48	42, 46, 47	3syl 18	. . . . . . . . 9 |- ( ( ph /\ k e. Z ) -> ( A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
49	7, 48	sylibrd 249	. . . . . . . 8 |- ( ( ph /\ k e. Z ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
50	3, 49	sylan2 491	. . . . . . 7 |- ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
51	50	anassrs 680	. . . . . 6 |- ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
52	51	ralimdva 2962	. . . . 5 |- ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
53	52	reximdva 3017	. . . 4 |- ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
54	53	ralimdv 2963	. . 3 |- ( ph -> ( A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
55		ulmf 24136	. . . . . 6 |- ( ( x e. Z |-> A ) ( ~~> u ` S ) G -> E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) )
56	1, 55	syl 17	. . . . 5 |- ( ph -> E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) )
57		fdm 6051	. . . . . . . 8 |- ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> dom ( x e. Z |-> A ) = ( ZZ>= ` m ) )
58	19	dmmptss 5631	. . . . . . . 8 |- dom ( x e. Z |-> A ) C_ Z
59	57, 58	syl6eqssr 3656	. . . . . . 7 |- ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> ( ZZ>= ` m ) C_ Z )
60		uzid 11702	. . . . . . . . 9 |- ( m e. ZZ -> m e. ( ZZ>= ` m ) )
61	60	adantl 482	. . . . . . . 8 |- ( ( ph /\ m e. ZZ ) -> m e. ( ZZ>= ` m ) )
62		ssel 3597	. . . . . . . . 9 |- ( ( ZZ>= ` m ) C_ Z -> ( m e. ( ZZ>= ` m ) -> m e. Z ) )
63		eluzel2 11692	. . . . . . . . . 10 |- ( m e. ( ZZ>= ` M ) -> M e. ZZ )
64	63, 2	eleq2s 2719	. . . . . . . . 9 |- ( m e. Z -> M e. ZZ )
65	62, 64	syl6 35	. . . . . . . 8 |- ( ( ZZ>= ` m ) C_ Z -> ( m e. ( ZZ>= ` m ) -> M e. ZZ ) )
66	61, 65	syl5com 31	. . . . . . 7 |- ( ( ph /\ m e. ZZ ) -> ( ( ZZ>= ` m ) C_ Z -> M e. ZZ ) )
67	59, 66	syl5 34	. . . . . 6 |- ( ( ph /\ m e. ZZ ) -> ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> M e. ZZ ) )
68	67	rexlimdva 3031	. . . . 5 |- ( ph -> ( E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> M e. ZZ ) )
69	56, 68	mpd 15	. . . 4 |- ( ph -> M e. ZZ )
70	11	ralrimiva 2966	. . . . . 6 |- ( ph -> A. x e. Z A e. W )
71	19	fnmpt 6020	. . . . . 6 |- ( A. x e. Z A e. W -> ( x e. Z |-> A ) Fn Z )
72	70, 71	syl 17	. . . . 5 |- ( ph -> ( x e. Z |-> A ) Fn Z )
73		frn 6053	. . . . . . 7 |- ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> ran ( x e. Z |-> A ) C_ ( CC ^m S ) )
74	73	rexlimivw 3029	. . . . . 6 |- ( E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> ran ( x e. Z |-> A ) C_ ( CC ^m S ) )
75	56, 74	syl 17	. . . . 5 |- ( ph -> ran ( x e. Z |-> A ) C_ ( CC ^m S ) )
76		df-f 5892	. . . . 5 |- ( ( x e. Z |-> A ) : Z --> ( CC ^m S ) <-> ( ( x e. Z |-> A ) Fn Z /\ ran ( x e. Z |-> A ) C_ ( CC ^m S ) ) )
77	72, 75, 76	sylanbrc 698	. . . 4 |- ( ph -> ( x e. Z |-> A ) : Z --> ( CC ^m S ) )
78		eqidd 2623	. . . 4 |- ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( ( x e. Z |-> A ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) )
79		eqidd 2623	. . . 4 |- ( ( ph /\ z e. S ) -> ( G ` z ) = ( G ` z ) )
80		ulmcl 24135	. . . . 5 |- ( ( x e. Z |-> A ) ( ~~> u ` S ) G -> G : S --> CC )
81	1, 80	syl 17	. . . 4 |- ( ph -> G : S --> CC )
82		ulmscl 24133	. . . . 5 |- ( ( x e. Z |-> A ) ( ~~> u ` S ) G -> S e. _V )
83	1, 82	syl 17	. . . 4 |- ( ph -> S e. _V )
84	2, 69, 77, 78, 79, 81, 83	ulm2 24139	. . 3 |- ( ph -> ( ( x e. Z |-> A ) ( ~~> u ` S ) G <-> A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
85	19	fmpt 6381	. . . . . . . . . 10 |- ( A. x e. Z A e. ( CC ^m S ) <-> ( x e. Z |-> A ) : Z --> ( CC ^m S ) )
86	77, 85	sylibr 224	. . . . . . . . 9 |- ( ph -> A. x e. Z A e. ( CC ^m S ) )
87	86	r19.21bi 2932	. . . . . . . 8 |- ( ( ph /\ x e. Z ) -> A e. ( CC ^m S ) )
88		elmapi 7879	. . . . . . . 8 |- ( A e. ( CC ^m S ) -> A : S --> CC )
89	87, 88	syl 17	. . . . . . 7 |- ( ( ph /\ x e. Z ) -> A : S --> CC )
90	4	adantr 481	. . . . . . 7 |- ( ( ph /\ x e. Z ) -> T C_ S )
91	89, 90	fssresd 6071	. . . . . 6 |- ( ( ph /\ x e. Z ) -> ( A |` T ) : T --> CC )
92		cnex 10017	. . . . . . 7 |- CC e. _V
93	83, 4	ssexd 4805	. . . . . . . 8 |- ( ph -> T e. _V )
94	93	adantr 481	. . . . . . 7 |- ( ( ph /\ x e. Z ) -> T e. _V )
95		elmapg 7870	. . . . . . 7 |- ( ( CC e. _V /\ T e. _V ) -> ( ( A |` T ) e. ( CC ^m T ) <-> ( A |` T ) : T --> CC ) )
96	92, 94, 95	sylancr 695	. . . . . 6 |- ( ( ph /\ x e. Z ) -> ( ( A |` T ) e. ( CC ^m T ) <-> ( A |` T ) : T --> CC ) )
97	91, 96	mpbird 247	. . . . 5 |- ( ( ph /\ x e. Z ) -> ( A |` T ) e. ( CC ^m T ) )
98	97, 15	fmptd 6385	. . . 4 |- ( ph -> ( x e. Z |-> ( A |` T ) ) : Z --> ( CC ^m T ) )
99		eqidd 2623	. . . 4 |- ( ( ph /\ ( k e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) )
100		fvres 6207	. . . . 5 |- ( z e. T -> ( ( G |` T ) ` z ) = ( G ` z ) )
101	100	adantl 482	. . . 4 |- ( ( ph /\ z e. T ) -> ( ( G |` T ) ` z ) = ( G ` z ) )
102	81, 4	fssresd 6071	. . . 4 |- ( ph -> ( G |` T ) : T --> CC )
103	2, 69, 98, 99, 101, 102, 93	ulm2 24139	. . 3 |- ( ph -> ( ( x e. Z |-> ( A |` T ) ) ( ~~> u ` T ) ( G |` T ) <-> A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
104	54, 84, 103	3imtr4d 283	. 2 |- ( ph -> ( ( x e. Z |-> A ) ( ~~> u ` S ) G -> ( x e. Z |-> ( A |` T ) ) ( ~~> u ` T ) ( G |` T ) ) )
105	1, 104	mpd 15	1 |- ( ph -> ( x e. Z |-> ( A |` T ) ) ( ~~> u ` T ) ( G |` T ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   C_ wss 3574   class class class wbr 4653   |-> cmpt 4729   dom cdm 5114   ran crn 5115   |` cres 5116   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   CCcc 9934   < clt 10074   - cmin 10266   ZZcz 11377   ZZ>=cuz 11687   RR+crp 11832   abscabs 13974   ~~> uculm 24130

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  ax-cnex 9992  ax-resscn 9993  ax-pre-lttri 10010  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  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-nel 2898  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-pw 4160  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-po 5035  df-so 5036  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  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-neg 10269  df-z 11378  df-uz 11688  df-ulm 24131

This theorem is referenced by: (None)