Theorem smflimsuplem5

Description: H converges to the superior limit of F . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smflimsuplem5.a	|- F/ n ph
	smflimsuplem5.b	|- F/ m ph
	smflimsuplem5.m	|- ( ph -> M e. ZZ )
	smflimsuplem5.z	|- Z = ( ZZ>= ` M )
	smflimsuplem5.s	|- ( ph -> S e. SAlg )
	smflimsuplem5.f	|- ( ph -> F : Z --> ( SMblFn ` S ) )
	smflimsuplem5.e	|- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
	smflimsuplem5.h	|- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
	smflimsuplem5.r	|- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
	smflimsuplem5.n	|- ( ph -> N e. Z )
	smflimsuplem5.x	|- ( ph -> X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) )
Assertion	smflimsuplem5	|- ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		smflimsuplem5.a	|- F/ n ph
2		smflimsuplem5.b	|- F/ m ph
3		smflimsuplem5.m	|- ( ph -> M e. ZZ )
4		smflimsuplem5.z	|- Z = ( ZZ>= ` M )
5		smflimsuplem5.s	|- ( ph -> S e. SAlg )
6		smflimsuplem5.f	|- ( ph -> F : Z --> ( SMblFn ` S ) )
7		smflimsuplem5.e	|- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
8		smflimsuplem5.h	|- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
9		smflimsuplem5.r	|- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
10		smflimsuplem5.n	|- ( ph -> N e. Z )
11		smflimsuplem5.x	|- ( ph -> X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) )
12	4	eleq2i	|- ( N e. Z <-> N e. ( ZZ>= ` M ) )
13	12	biimpi	|- ( N e. Z -> N e. ( ZZ>= ` M ) )
14		uzss	|- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
15	13 14	syl	|- ( N e. Z -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
16	15 4	sseqtrrdi	|- ( N e. Z -> ( ZZ>= ` N ) C_ Z )
17	10 16	syl	|- ( ph -> ( ZZ>= ` N ) C_ Z )
18	17	sselda	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. Z )
19		nfcv	|- F/_ x Z
20		nfrab1	|- F/_ x { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR }
21	19 20	nfmpt	|- F/_ x ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
22	7 21	nfcxfr	|- F/_ x E
23		nfcv	|- F/_ x n
24	22 23	nffv	|- F/_ x ( E ` n )
25		fvex	|- ( E ` n ) e. _V
26	24 25	mptexf	|- ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V
27	26	a1i	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V )
28	8	fvmpt2	|- ( ( n e. Z /\ ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V ) -> ( H ` n ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
29	18 27 28	syl2anc	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( H ` n ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
30	29	fveq1d	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( H ` n ) ` X ) = ( ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) ` X ) )
31		nfcv	|- F/_ y ( E ` n )
32		nfcv	|- F/_ y sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < )
33		nfcv	|- F/_ x sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < )
34		fveq2	|- ( x = y -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) )
35	34	mpteq2dv	|- ( x = y -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) )
36	35	rneqd	|- ( x = y -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) )
37	36	supeq1d	|- ( x = y -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) )
38	24 31 32 33 37	cbvmptf	|- ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( y e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) )
39		simpl	|- ( ( y = X /\ m e. ( ZZ>= ` n ) ) -> y = X )
40	39	fveq2d	|- ( ( y = X /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` y ) = ( ( F ` m ) ` X ) )
41	40	mpteq2dva	|- ( y = X -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) )
42	41	rneqd	|- ( y = X -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) )
43	42	supeq1d	|- ( y = X -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) )
44	43	eleq1d	|- ( y = X -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR <-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR ) )
45		uzss	|- ( n e. ( ZZ>= ` N ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` N ) )
46		iinss1	|- ( ( ZZ>= ` n ) C_ ( ZZ>= ` N ) -> |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
47	45 46	syl	|- ( n e. ( ZZ>= ` N ) -> |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
48	47	adantl	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
49	11	adantr	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) )
50	48 49	sseldd	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
51		nfv	|- F/ m n e. ( ZZ>= ` N )
52	2 51	nfan	|- F/ m ( ph /\ n e. ( ZZ>= ` N ) )
53		eqid	|- ( ZZ>= ` n ) = ( ZZ>= ` n )
54		simpll	|- ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ZZ>= ` n ) ) -> ph )
55	45	sselda	|- ( ( n e. ( ZZ>= ` N ) /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` N ) )
56	55	adantll	|- ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` N ) )
57	5	adantr	|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> S e. SAlg )
58		simpl	|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ph )
59	17	sselda	|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> m e. Z )
60	6	ffvelcdmda	|- ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
61	58 59 60	syl2anc	|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( F ` m ) e. ( SMblFn ` S ) )
62		eqid	|- dom ( F ` m ) = dom ( F ` m )
63	57 61 62	smff	|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( F ` m ) : dom ( F ` m ) --> RR )
64		eliin	|- ( X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) -> ( X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) <-> A. m e. ( ZZ>= ` N ) X e. dom ( F ` m ) ) )
65	11 64	syl	|- ( ph -> ( X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) <-> A. m e. ( ZZ>= ` N ) X e. dom ( F ` m ) ) )
66	11 65	mpbid	|- ( ph -> A. m e. ( ZZ>= ` N ) X e. dom ( F ` m ) )
67	66	adantr	|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> A. m e. ( ZZ>= ` N ) X e. dom ( F ` m ) )
68		simpr	|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> m e. ( ZZ>= ` N ) )
69		rspa	|- ( ( A. m e. ( ZZ>= ` N ) X e. dom ( F ` m ) /\ m e. ( ZZ>= ` N ) ) -> X e. dom ( F ` m ) )
70	67 68 69	syl2anc	|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> X e. dom ( F ` m ) )
71	63 70	ffvelcdmd	|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( ( F ` m ) ` X ) e. RR )
72	54 56 71	syl2anc	|- ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` X ) e. RR )
73		eluzelz	|- ( n e. ( ZZ>= ` N ) -> n e. ZZ )
74	73	adantl	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. ZZ )
75	3	adantr	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> M e. ZZ )
76		fvex	|- ( ( F ` m ) ` X ) e. _V
77	76	a1i	|- ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. Z ) -> ( ( F ` m ) ` X ) e. _V )
78	52 74 75 53 4 72 77	limsupequzmpt	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) = ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
79	9	adantr	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
80	78 79	eqeltrd	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) e. RR )
81	80	renepnfd	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) =/= +oo )
82	52 53 72 81	limsupubuzmpt	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> E. y e. RR A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) <_ y )
83		uzid2	|- ( n e. ( ZZ>= ` N ) -> n e. ( ZZ>= ` n ) )
84	83	ne0d	|- ( n e. ( ZZ>= ` N ) -> ( ZZ>= ` n ) =/= (/) )
85	84	adantl	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ZZ>= ` n ) =/= (/) )
86	52 85 72	supxrre3rnmpt	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR <-> E. y e. RR A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) <_ y ) )
87	82 86	mpbird	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR )
88	44 50 87	elrabd	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> X e. { y e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR } )
89		simpl	|- ( ( y = x /\ m e. ( ZZ>= ` n ) ) -> y = x )
90	89	fveq2d	|- ( ( y = x /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` y ) = ( ( F ` m ) ` x ) )
91	90	mpteq2dva	|- ( y = x -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) )
92	91	rneqd	|- ( y = x -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) )
93	92	supeq1d	|- ( y = x -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) )
94	93	eleq1d	|- ( y = x -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR <-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR ) )
95	94	cbvrabv	|- { y e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR } = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR }
96	88 95	eleqtrdi	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> X e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
97		eqid	|- { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR }
98		fvex	|- ( F ` m ) e. _V
99	98	dmex	|- dom ( F ` m ) e. _V
100	99	rgenw	|- A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V
101	100	a1i	|- ( n e. ( ZZ>= ` N ) -> A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
102	84 101	iinexd	|- ( n e. ( ZZ>= ` N ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
103	102	adantl	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
104	97 103	rabexd	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } e. _V )
105	7	fvmpt2	|- ( ( n e. Z /\ { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } e. _V ) -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
106	18 104 105	syl2anc	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
107	96 106	eleqtrrd	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> X e. ( E ` n ) )
108	38 43 107 87	fvmptd3	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) ` X ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) )
109	30 108	eqtrd	|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( H ` n ) ` X ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) )
110	1 109	mpteq2da	|- ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` X ) ) = ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) ) )
111	4	eluzelz2	|- ( N e. Z -> N e. ZZ )
112	10 111	syl	|- ( ph -> N e. ZZ )
113		eqid	|- ( ZZ>= ` N ) = ( ZZ>= ` N )
114	76	a1i	|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( ( F ` m ) ` X ) e. _V )
115	76	a1i	|- ( ( ph /\ m e. Z ) -> ( ( F ` m ) ` X ) e. _V )
116	2 112 3 113 4 114 115	limsupequzmpt	|- ( ph -> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) = ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
117	116 9	eqeltrd	|- ( ph -> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) e. RR )
118	2 112 113 71 117	supcnvlimsupmpt	|- ( ph -> ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) )
119	110 118	eqbrtrd	|- ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) )