Theorem smflimlem3

Description: The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smflimlem3.z	|- Z = ( ZZ>= ` M )
	smflimlem3.s	|- ( ph -> S e. SAlg )
	smflimlem3.m	|- ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
	smflimlem3.d	|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
	smflimlem3.a	|- ( ph -> A e. RR )
	smflimlem3.p	|- P = ( m e. Z , k e. NN |-> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
	smflimlem3.h	|- H = ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) )
	smflimlem3.i	|- I = |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k )
	smflimlem3.c	|- ( ( ph /\ y e. ran P ) -> ( C ` y ) e. y )
	smflimlem3.x	|- ( ph -> X e. ( D i^i I ) )
	smflimlem3.k	|- ( ph -> K e. NN )
	smflimlem3.y	|- ( ph -> Y e. RR+ )
	smflimlem3.l	|- ( ph -> ( 1 / K ) < Y )
Assertion	smflimlem3	|- ( ph -> E. m e. Z A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		smflimlem3.z	|- Z = ( ZZ>= ` M )
2		smflimlem3.s	|- ( ph -> S e. SAlg )
3		smflimlem3.m	|- ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
4		smflimlem3.d	|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
5		smflimlem3.a	|- ( ph -> A e. RR )
6		smflimlem3.p	|- P = ( m e. Z , k e. NN |-> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
7		smflimlem3.h	|- H = ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) )
8		smflimlem3.i	|- I = |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k )
9		smflimlem3.c	|- ( ( ph /\ y e. ran P ) -> ( C ` y ) e. y )
10		smflimlem3.x	|- ( ph -> X e. ( D i^i I ) )
11		smflimlem3.k	|- ( ph -> K e. NN )
12		smflimlem3.y	|- ( ph -> Y e. RR+ )
13		smflimlem3.l	|- ( ph -> ( 1 / K ) < Y )
14		ssrab2	|- { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
15	4 14	eqsstri	|- D C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
16		inss1	|- ( D i^i I ) C_ D
17	16 10	sselid	|- ( ph -> X e. D )
18	15 17	sselid	|- ( ph -> X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
19		fveq2	|- ( i = m -> ( F ` i ) = ( F ` m ) )
20	19	dmeqd	|- ( i = m -> dom ( F ` i ) = dom ( F ` m ) )
21		eqcom	|- ( i = m <-> m = i )
22	21	imbi1i	|- ( ( i = m -> dom ( F ` i ) = dom ( F ` m ) ) <-> ( m = i -> dom ( F ` i ) = dom ( F ` m ) ) )
23		eqcom	|- ( dom ( F ` i ) = dom ( F ` m ) <-> dom ( F ` m ) = dom ( F ` i ) )
24	23	imbi2i	|- ( ( m = i -> dom ( F ` i ) = dom ( F ` m ) ) <-> ( m = i -> dom ( F ` m ) = dom ( F ` i ) ) )
25	22 24	bitri	|- ( ( i = m -> dom ( F ` i ) = dom ( F ` m ) ) <-> ( m = i -> dom ( F ` m ) = dom ( F ` i ) ) )
26	20 25	mpbi	|- ( m = i -> dom ( F ` m ) = dom ( F ` i ) )
27	26	cbviinv	|- |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ i e. ( ZZ>= ` n ) dom ( F ` i )
28	27	a1i	|- ( n e. Z -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ i e. ( ZZ>= ` n ) dom ( F ` i ) )
29	28	iuneq2i	|- U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ n e. Z |^|_ i e. ( ZZ>= ` n ) dom ( F ` i )
30		fveq2	|- ( n = m -> ( ZZ>= ` n ) = ( ZZ>= ` m ) )
31	30	iineq1d	|- ( n = m -> |^|_ i e. ( ZZ>= ` n ) dom ( F ` i ) = |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) )
32	31	cbviunv	|- U_ n e. Z |^|_ i e. ( ZZ>= ` n ) dom ( F ` i ) = U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i )
33	29 32	eqtri	|- U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i )
34	18 33	eleqtrdi	|- ( ph -> X e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) )
35		eqid	|- U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) = U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i )
36	1 35	allbutfi	|- ( X e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) <-> E. m e. Z A. i e. ( ZZ>= ` m ) X e. dom ( F ` i ) )
37	36	biimpi	|- ( X e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) -> E. m e. Z A. i e. ( ZZ>= ` m ) X e. dom ( F ` i ) )
38	34 37	syl	|- ( ph -> E. m e. Z A. i e. ( ZZ>= ` m ) X e. dom ( F ` i ) )
39	10	elin2d	|- ( ph -> X e. I )
40		oveq1	|- ( m = i -> ( m H k ) = ( i H k ) )
41	40	cbviinv	|- |^|_ m e. ( ZZ>= ` n ) ( m H k ) = |^|_ i e. ( ZZ>= ` n ) ( i H k )
42	41	a1i	|- ( n e. Z -> |^|_ m e. ( ZZ>= ` n ) ( m H k ) = |^|_ i e. ( ZZ>= ` n ) ( i H k ) )
43	42	iuneq2i	|- U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) = U_ n e. Z |^|_ i e. ( ZZ>= ` n ) ( i H k )
44	30	iineq1d	|- ( n = m -> |^|_ i e. ( ZZ>= ` n ) ( i H k ) = |^|_ i e. ( ZZ>= ` m ) ( i H k ) )
45	44	cbviunv	|- U_ n e. Z |^|_ i e. ( ZZ>= ` n ) ( i H k ) = U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H k )
46	43 45	eqtri	|- U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) = U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H k )
47	46	a1i	|- ( k e. NN -> U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) = U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H k ) )
48	47	iineq2i	|- |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) = |^|_ k e. NN U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H k )
49	8 48	eqtri	|- I = |^|_ k e. NN U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H k )
50	39 49	eleqtrdi	|- ( ph -> X e. |^|_ k e. NN U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H k ) )
51		oveq2	|- ( k = K -> ( i H k ) = ( i H K ) )
52	51	adantr	|- ( ( k = K /\ i e. ( ZZ>= ` m ) ) -> ( i H k ) = ( i H K ) )
53	52	iineq2dv	|- ( k = K -> |^|_ i e. ( ZZ>= ` m ) ( i H k ) = |^|_ i e. ( ZZ>= ` m ) ( i H K ) )
54	53	iuneq2d	|- ( k = K -> U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H k ) = U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H K ) )
55	54	eleq2d	|- ( k = K -> ( X e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H k ) <-> X e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H K ) ) )
56	50 11 55	eliind	|- ( ph -> X e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H K ) )
57		eqid	|- U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H K ) = U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H K )
58	1 57	allbutfi	|- ( X e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) ( i H K ) <-> E. m e. Z A. i e. ( ZZ>= ` m ) X e. ( i H K ) )
59	56 58	sylib	|- ( ph -> E. m e. Z A. i e. ( ZZ>= ` m ) X e. ( i H K ) )
60	38 59	jca	|- ( ph -> ( E. m e. Z A. i e. ( ZZ>= ` m ) X e. dom ( F ` i ) /\ E. m e. Z A. i e. ( ZZ>= ` m ) X e. ( i H K ) ) )
61	1	rexanuz2	|- ( E. m e. Z A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) <-> ( E. m e. Z A. i e. ( ZZ>= ` m ) X e. dom ( F ` i ) /\ E. m e. Z A. i e. ( ZZ>= ` m ) X e. ( i H K ) ) )
62	60 61	sylibr	|- ( ph -> E. m e. Z A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) )
63		simpll	|- ( ( ( ph /\ m e. Z ) /\ i e. ( ZZ>= ` m ) ) -> ph )
64		simpr	|- ( ( ph /\ m e. Z ) -> m e. Z )
65	1	uztrn2	|- ( ( m e. Z /\ i e. ( ZZ>= ` m ) ) -> i e. Z )
66	64 65	sylan	|- ( ( ( ph /\ m e. Z ) /\ i e. ( ZZ>= ` m ) ) -> i e. Z )
67		simprl	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) ) -> X e. dom ( F ` i ) )
68		simp3	|- ( ( ph /\ i e. Z /\ X e. ( i H K ) ) -> X e. ( i H K ) )
69	7	a1i	|- ( ( ph /\ i e. Z ) -> H = ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) ) )
70		oveq12	|- ( ( m = i /\ k = K ) -> ( m P k ) = ( i P K ) )
71	70	fveq2d	|- ( ( m = i /\ k = K ) -> ( C ` ( m P k ) ) = ( C ` ( i P K ) ) )
72	71	adantl	|- ( ( ( ph /\ i e. Z ) /\ ( m = i /\ k = K ) ) -> ( C ` ( m P k ) ) = ( C ` ( i P K ) ) )
73		simpr	|- ( ( ph /\ i e. Z ) -> i e. Z )
74	11	adantr	|- ( ( ph /\ i e. Z ) -> K e. NN )
75		fvexd	|- ( ( ph /\ i e. Z ) -> ( C ` ( i P K ) ) e. _V )
76	69 72 73 74 75	ovmpod	|- ( ( ph /\ i e. Z ) -> ( i H K ) = ( C ` ( i P K ) ) )
77	76	3adant3	|- ( ( ph /\ i e. Z /\ X e. ( i H K ) ) -> ( i H K ) = ( C ` ( i P K ) ) )
78	68 77	eleqtrd	|- ( ( ph /\ i e. Z /\ X e. ( i H K ) ) -> X e. ( C ` ( i P K ) ) )
79	78	3expa	|- ( ( ( ph /\ i e. Z ) /\ X e. ( i H K ) ) -> X e. ( C ` ( i P K ) ) )
80	79	adantrl	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) ) -> X e. ( C ` ( i P K ) ) )
81	80 67	elind	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) ) -> X e. ( ( C ` ( i P K ) ) i^i dom ( F ` i ) ) )
82		eqid	|- { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) }
83	82 2	rabexd	|- ( ph -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
84	83	ralrimivw	|- ( ph -> A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
85	84	a1d	|- ( ph -> ( m e. Z -> A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V ) )
86	85	imp	|- ( ( ph /\ m e. Z ) -> A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
87	86	ralrimiva	|- ( ph -> A. m e. Z A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
88	6	fnmpo	|- ( A. m e. Z A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V -> P Fn ( Z X. NN ) )
89	87 88	syl	|- ( ph -> P Fn ( Z X. NN ) )
90	89	adantr	|- ( ( ph /\ i e. Z ) -> P Fn ( Z X. NN ) )
91		fnovrn	|- ( ( P Fn ( Z X. NN ) /\ i e. Z /\ K e. NN ) -> ( i P K ) e. ran P )
92	90 73 74 91	syl3anc	|- ( ( ph /\ i e. Z ) -> ( i P K ) e. ran P )
93		ovex	|- ( i P K ) e. _V
94		eleq1	|- ( y = ( i P K ) -> ( y e. ran P <-> ( i P K ) e. ran P ) )
95	94	anbi2d	|- ( y = ( i P K ) -> ( ( ph /\ y e. ran P ) <-> ( ph /\ ( i P K ) e. ran P ) ) )
96		fveq2	|- ( y = ( i P K ) -> ( C ` y ) = ( C ` ( i P K ) ) )
97		id	|- ( y = ( i P K ) -> y = ( i P K ) )
98	96 97	eleq12d	|- ( y = ( i P K ) -> ( ( C ` y ) e. y <-> ( C ` ( i P K ) ) e. ( i P K ) ) )
99	95 98	imbi12d	|- ( y = ( i P K ) -> ( ( ( ph /\ y e. ran P ) -> ( C ` y ) e. y ) <-> ( ( ph /\ ( i P K ) e. ran P ) -> ( C ` ( i P K ) ) e. ( i P K ) ) ) )
100	93 99 9	vtocl	|- ( ( ph /\ ( i P K ) e. ran P ) -> ( C ` ( i P K ) ) e. ( i P K ) )
101	92 100	syldan	|- ( ( ph /\ i e. Z ) -> ( C ` ( i P K ) ) e. ( i P K ) )
102	6	a1i	|- ( ( ph /\ i e. Z ) -> P = ( m e. Z , k e. NN |-> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } ) )
103	26	adantr	|- ( ( m = i /\ k = K ) -> dom ( F ` m ) = dom ( F ` i ) )
104	19	fveq1d	|- ( i = m -> ( ( F ` i ) ` x ) = ( ( F ` m ) ` x ) )
105	21	imbi1i	|- ( ( i = m -> ( ( F ` i ) ` x ) = ( ( F ` m ) ` x ) ) <-> ( m = i -> ( ( F ` i ) ` x ) = ( ( F ` m ) ` x ) ) )
106		eqcom	|- ( ( ( F ` i ) ` x ) = ( ( F ` m ) ` x ) <-> ( ( F ` m ) ` x ) = ( ( F ` i ) ` x ) )
107	106	imbi2i	|- ( ( m = i -> ( ( F ` i ) ` x ) = ( ( F ` m ) ` x ) ) <-> ( m = i -> ( ( F ` m ) ` x ) = ( ( F ` i ) ` x ) ) )
108	105 107	bitri	|- ( ( i = m -> ( ( F ` i ) ` x ) = ( ( F ` m ) ` x ) ) <-> ( m = i -> ( ( F ` m ) ` x ) = ( ( F ` i ) ` x ) ) )
109	104 108	mpbi	|- ( m = i -> ( ( F ` m ) ` x ) = ( ( F ` i ) ` x ) )
110	109	adantr	|- ( ( m = i /\ k = K ) -> ( ( F ` m ) ` x ) = ( ( F ` i ) ` x ) )
111		oveq2	|- ( k = K -> ( 1 / k ) = ( 1 / K ) )
112	111	oveq2d	|- ( k = K -> ( A + ( 1 / k ) ) = ( A + ( 1 / K ) ) )
113	112	adantl	|- ( ( m = i /\ k = K ) -> ( A + ( 1 / k ) ) = ( A + ( 1 / K ) ) )
114	110 113	breq12d	|- ( ( m = i /\ k = K ) -> ( ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) <-> ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) ) )
115	103 114	rabeqbidv	|- ( ( m = i /\ k = K ) -> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } )
116	26	ineq2d	|- ( m = i -> ( s i^i dom ( F ` m ) ) = ( s i^i dom ( F ` i ) ) )
117	116	adantr	|- ( ( m = i /\ k = K ) -> ( s i^i dom ( F ` m ) ) = ( s i^i dom ( F ` i ) ) )
118	115 117	eqeq12d	|- ( ( m = i /\ k = K ) -> ( { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) <-> { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) ) )
119	118	rabbidv	|- ( ( m = i /\ k = K ) -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } = { s e. S | { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) } )
120	119	adantl	|- ( ( ( ph /\ i e. Z ) /\ ( m = i /\ k = K ) ) -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } = { s e. S | { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) } )
121		eqid	|- { s e. S | { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) } = { s e. S | { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) }
122	121 2	rabexd	|- ( ph -> { s e. S | { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) } e. _V )
123	122	adantr	|- ( ( ph /\ i e. Z ) -> { s e. S | { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) } e. _V )
124	102 120 73 74 123	ovmpod	|- ( ( ph /\ i e. Z ) -> ( i P K ) = { s e. S | { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) } )
125	101 124	eleqtrd	|- ( ( ph /\ i e. Z ) -> ( C ` ( i P K ) ) e. { s e. S | { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) } )
126		ineq1	|- ( s = ( C ` ( i P K ) ) -> ( s i^i dom ( F ` i ) ) = ( ( C ` ( i P K ) ) i^i dom ( F ` i ) ) )
127	126	eqeq2d	|- ( s = ( C ` ( i P K ) ) -> ( { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) <-> { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( ( C ` ( i P K ) ) i^i dom ( F ` i ) ) ) )
128	127	elrab	|- ( ( C ` ( i P K ) ) e. { s e. S | { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( s i^i dom ( F ` i ) ) } <-> ( ( C ` ( i P K ) ) e. S /\ { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( ( C ` ( i P K ) ) i^i dom ( F ` i ) ) ) )
129	125 128	sylib	|- ( ( ph /\ i e. Z ) -> ( ( C ` ( i P K ) ) e. S /\ { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( ( C ` ( i P K ) ) i^i dom ( F ` i ) ) ) )
130	129	simprd	|- ( ( ph /\ i e. Z ) -> { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } = ( ( C ` ( i P K ) ) i^i dom ( F ` i ) ) )
131	130	eqcomd	|- ( ( ph /\ i e. Z ) -> ( ( C ` ( i P K ) ) i^i dom ( F ` i ) ) = { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } )
132	131	adantr	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) ) -> ( ( C ` ( i P K ) ) i^i dom ( F ` i ) ) = { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } )
133	81 132	eleqtrd	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) ) -> X e. { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } )
134		fveq2	|- ( x = X -> ( ( F ` i ) ` x ) = ( ( F ` i ) ` X ) )
135		eqidd	|- ( x = X -> ( A + ( 1 / K ) ) = ( A + ( 1 / K ) ) )
136	134 135	breq12d	|- ( x = X -> ( ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) <-> ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) )
137	136	elrab	|- ( X e. { x e. dom ( F ` i ) | ( ( F ` i ) ` x ) < ( A + ( 1 / K ) ) } <-> ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) )
138	133 137	sylib	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) ) -> ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) )
139	138	simprd	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) ) -> ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) )
140	67 139	jca	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) ) -> ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) )
141	140	ex	|- ( ( ph /\ i e. Z ) -> ( ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) -> ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) )
142	63 66 141	syl2anc	|- ( ( ( ph /\ m e. Z ) /\ i e. ( ZZ>= ` m ) ) -> ( ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) -> ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) )
143	142	ralimdva	|- ( ( ph /\ m e. Z ) -> ( A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) -> A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) )
144	143	reximdva	|- ( ph -> ( E. m e. Z A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ X e. ( i H K ) ) -> E. m e. Z A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) )
145	62 144	mpd	|- ( ph -> E. m e. Z A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) )
146		simprl	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) -> X e. dom ( F ` i ) )
147		eleq1	|- ( m = i -> ( m e. Z <-> i e. Z ) )
148	147	anbi2d	|- ( m = i -> ( ( ph /\ m e. Z ) <-> ( ph /\ i e. Z ) ) )
149		fveq2	|- ( m = i -> ( F ` m ) = ( F ` i ) )
150	149 26	feq12d	|- ( m = i -> ( ( F ` m ) : dom ( F ` m ) --> RR <-> ( F ` i ) : dom ( F ` i ) --> RR ) )
151	148 150	imbi12d	|- ( m = i -> ( ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR ) <-> ( ( ph /\ i e. Z ) -> ( F ` i ) : dom ( F ` i ) --> RR ) ) )
152	2	adantr	|- ( ( ph /\ m e. Z ) -> S e. SAlg )
153		eqid	|- dom ( F ` m ) = dom ( F ` m )
154	152 3 153	smff	|- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
155	151 154	chvarvv	|- ( ( ph /\ i e. Z ) -> ( F ` i ) : dom ( F ` i ) --> RR )
156	155	adantr	|- ( ( ( ph /\ i e. Z ) /\ X e. dom ( F ` i ) ) -> ( F ` i ) : dom ( F ` i ) --> RR )
157		simpr	|- ( ( ( ph /\ i e. Z ) /\ X e. dom ( F ` i ) ) -> X e. dom ( F ` i ) )
158	156 157	ffvelcdmd	|- ( ( ( ph /\ i e. Z ) /\ X e. dom ( F ` i ) ) -> ( ( F ` i ) ` X ) e. RR )
159	158	adantrr	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) -> ( ( F ` i ) ` X ) e. RR )
160	11	nnrecred	|- ( ph -> ( 1 / K ) e. RR )
161	5 160	readdcld	|- ( ph -> ( A + ( 1 / K ) ) e. RR )
162	161	ad2antrr	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) -> ( A + ( 1 / K ) ) e. RR )
163	12	rpred	|- ( ph -> Y e. RR )
164	5 163	readdcld	|- ( ph -> ( A + Y ) e. RR )
165	164	ad2antrr	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) -> ( A + Y ) e. RR )
166		simprr	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) -> ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) )
167	160 163 5 13	ltadd2dd	|- ( ph -> ( A + ( 1 / K ) ) < ( A + Y ) )
168	167	ad2antrr	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) -> ( A + ( 1 / K ) ) < ( A + Y ) )
169	159 162 165 166 168	lttrd	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) -> ( ( F ` i ) ` X ) < ( A + Y ) )
170	146 169	jca	|- ( ( ( ph /\ i e. Z ) /\ ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) ) -> ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + Y ) ) )
171	170	ex	|- ( ( ph /\ i e. Z ) -> ( ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) -> ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + Y ) ) ) )
172	63 66 171	syl2anc	|- ( ( ( ph /\ m e. Z ) /\ i e. ( ZZ>= ` m ) ) -> ( ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) -> ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + Y ) ) ) )
173	172	ralimdva	|- ( ( ph /\ m e. Z ) -> ( A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) -> A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + Y ) ) ) )
174	173	reximdva	|- ( ph -> ( E. m e. Z A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + ( 1 / K ) ) ) -> E. m e. Z A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + Y ) ) ) )
175	145 174	mpd	|- ( ph -> E. m e. Z A. i e. ( ZZ>= ` m ) ( X e. dom ( F ` i ) /\ ( ( F ` i ) ` X ) < ( A + Y ) ) )