This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1stckgenlem

Description: The one-point compactification of NN is compact. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypotheses 1stckgen.1 
|- ( ph -> J e. ( TopOn ` X ) )
1stckgen.2 
|- ( ph -> F : NN --> X )
1stckgen.3 
|- ( ph -> F ( ~~>t ` J ) A )
Assertion 1stckgenlem 
|- ( ph -> ( J |`t ( ran F u. { A } ) ) e. Comp )

Proof

Step Hyp Ref Expression
1 1stckgen.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 1stckgen.2 
 |-  ( ph -> F : NN --> X )
3 1stckgen.3 
 |-  ( ph -> F ( ~~>t ` J ) A )
4 simprr 
 |-  ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) -> ( ran F u. { A } ) C_ U. u )
5 ssun2 
 |-  { A } C_ ( ran F u. { A } )
6 lmcl 
 |-  ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) A ) -> A e. X )
7 1 3 6 syl2anc 
 |-  ( ph -> A e. X )
8 snssg 
 |-  ( A e. X -> ( A e. ( ran F u. { A } ) <-> { A } C_ ( ran F u. { A } ) ) )
9 7 8 syl 
 |-  ( ph -> ( A e. ( ran F u. { A } ) <-> { A } C_ ( ran F u. { A } ) ) )
10 5 9 mpbiri 
 |-  ( ph -> A e. ( ran F u. { A } ) )
11 10 adantr 
 |-  ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) -> A e. ( ran F u. { A } ) )
12 4 11 sseldd 
 |-  ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) -> A e. U. u )
13 eluni2 
 |-  ( A e. U. u <-> E. w e. u A e. w )
14 12 13 sylib 
 |-  ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) -> E. w e. u A e. w )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 simprr 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( w e. u /\ A e. w ) ) -> A e. w )
17 1zzd 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( w e. u /\ A e. w ) ) -> 1 e. ZZ )
18 3 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( w e. u /\ A e. w ) ) -> F ( ~~>t ` J ) A )
19 simplrl 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( w e. u /\ A e. w ) ) -> u e. ~P J )
20 19 elpwid 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( w e. u /\ A e. w ) ) -> u C_ J )
21 simprl 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( w e. u /\ A e. w ) ) -> w e. u )
22 20 21 sseldd 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( w e. u /\ A e. w ) ) -> w e. J )
23 15 16 17 18 22 lmcvg 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( w e. u /\ A e. w ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( F ` k ) e. w )
24 imassrn 
 |-  ( F " ( 1 ... j ) ) C_ ran F
25 ssun1 
 |-  ran F C_ ( ran F u. { A } )
26 24 25 sstri 
 |-  ( F " ( 1 ... j ) ) C_ ( ran F u. { A } )
27 id 
 |-  ( ( ran F u. { A } ) C_ U. u -> ( ran F u. { A } ) C_ U. u )
28 26 27 sstrid 
 |-  ( ( ran F u. { A } ) C_ U. u -> ( F " ( 1 ... j ) ) C_ U. u )
29 2 frnd 
 |-  ( ph -> ran F C_ X )
30 24 29 sstrid 
 |-  ( ph -> ( F " ( 1 ... j ) ) C_ X )
31 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ ( F " ( 1 ... j ) ) C_ X ) -> ( J |`t ( F " ( 1 ... j ) ) ) e. ( TopOn ` ( F " ( 1 ... j ) ) ) )
32 1 30 31 syl2anc 
 |-  ( ph -> ( J |`t ( F " ( 1 ... j ) ) ) e. ( TopOn ` ( F " ( 1 ... j ) ) ) )
33 topontop 
 |-  ( ( J |`t ( F " ( 1 ... j ) ) ) e. ( TopOn ` ( F " ( 1 ... j ) ) ) -> ( J |`t ( F " ( 1 ... j ) ) ) e. Top )
34 32 33 syl 
 |-  ( ph -> ( J |`t ( F " ( 1 ... j ) ) ) e. Top )
35 fzfid 
 |-  ( ph -> ( 1 ... j ) e. Fin )
36 2 ffund 
 |-  ( ph -> Fun F )
37 fz1ssnn 
 |-  ( 1 ... j ) C_ NN
38 2 fdmd 
 |-  ( ph -> dom F = NN )
39 37 38 sseqtrrid 
 |-  ( ph -> ( 1 ... j ) C_ dom F )
40 fores 
 |-  ( ( Fun F /\ ( 1 ... j ) C_ dom F ) -> ( F |` ( 1 ... j ) ) : ( 1 ... j ) -onto-> ( F " ( 1 ... j ) ) )
41 36 39 40 syl2anc 
 |-  ( ph -> ( F |` ( 1 ... j ) ) : ( 1 ... j ) -onto-> ( F " ( 1 ... j ) ) )
42 fofi 
 |-  ( ( ( 1 ... j ) e. Fin /\ ( F |` ( 1 ... j ) ) : ( 1 ... j ) -onto-> ( F " ( 1 ... j ) ) ) -> ( F " ( 1 ... j ) ) e. Fin )
43 35 41 42 syl2anc 
 |-  ( ph -> ( F " ( 1 ... j ) ) e. Fin )
44 pwfi 
 |-  ( ( F " ( 1 ... j ) ) e. Fin <-> ~P ( F " ( 1 ... j ) ) e. Fin )
45 43 44 sylib 
 |-  ( ph -> ~P ( F " ( 1 ... j ) ) e. Fin )
46 restsspw 
 |-  ( J |`t ( F " ( 1 ... j ) ) ) C_ ~P ( F " ( 1 ... j ) )
47 ssfi 
 |-  ( ( ~P ( F " ( 1 ... j ) ) e. Fin /\ ( J |`t ( F " ( 1 ... j ) ) ) C_ ~P ( F " ( 1 ... j ) ) ) -> ( J |`t ( F " ( 1 ... j ) ) ) e. Fin )
48 45 46 47 sylancl 
 |-  ( ph -> ( J |`t ( F " ( 1 ... j ) ) ) e. Fin )
49 34 48 elind 
 |-  ( ph -> ( J |`t ( F " ( 1 ... j ) ) ) e. ( Top i^i Fin ) )
50 fincmp 
 |-  ( ( J |`t ( F " ( 1 ... j ) ) ) e. ( Top i^i Fin ) -> ( J |`t ( F " ( 1 ... j ) ) ) e. Comp )
51 49 50 syl 
 |-  ( ph -> ( J |`t ( F " ( 1 ... j ) ) ) e. Comp )
52 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
53 1 52 syl 
 |-  ( ph -> J e. Top )
54 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
55 1 54 syl 
 |-  ( ph -> X = U. J )
56 30 55 sseqtrd 
 |-  ( ph -> ( F " ( 1 ... j ) ) C_ U. J )
57 eqid 
 |-  U. J = U. J
58 57 cmpsub 
 |-  ( ( J e. Top /\ ( F " ( 1 ... j ) ) C_ U. J ) -> ( ( J |`t ( F " ( 1 ... j ) ) ) e. Comp <-> A. u e. ~P J ( ( F " ( 1 ... j ) ) C_ U. u -> E. s e. ( ~P u i^i Fin ) ( F " ( 1 ... j ) ) C_ U. s ) ) )
59 53 56 58 syl2anc 
 |-  ( ph -> ( ( J |`t ( F " ( 1 ... j ) ) ) e. Comp <-> A. u e. ~P J ( ( F " ( 1 ... j ) ) C_ U. u -> E. s e. ( ~P u i^i Fin ) ( F " ( 1 ... j ) ) C_ U. s ) ) )
60 51 59 mpbid 
 |-  ( ph -> A. u e. ~P J ( ( F " ( 1 ... j ) ) C_ U. u -> E. s e. ( ~P u i^i Fin ) ( F " ( 1 ... j ) ) C_ U. s ) )
61 60 r19.21bi 
 |-  ( ( ph /\ u e. ~P J ) -> ( ( F " ( 1 ... j ) ) C_ U. u -> E. s e. ( ~P u i^i Fin ) ( F " ( 1 ... j ) ) C_ U. s ) )
62 28 61 syl5 
 |-  ( ( ph /\ u e. ~P J ) -> ( ( ran F u. { A } ) C_ U. u -> E. s e. ( ~P u i^i Fin ) ( F " ( 1 ... j ) ) C_ U. s ) )
63 62 impr 
 |-  ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) -> E. s e. ( ~P u i^i Fin ) ( F " ( 1 ... j ) ) C_ U. s )
64 63 adantr 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) -> E. s e. ( ~P u i^i Fin ) ( F " ( 1 ... j ) ) C_ U. s )
65 simprl 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> s e. ( ~P u i^i Fin ) )
66 65 elin1d 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> s e. ~P u )
67 66 elpwid 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> s C_ u )
68 simprll 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) -> w e. u )
69 68 adantr 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> w e. u )
70 69 snssd 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> { w } C_ u )
71 67 70 unssd 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> ( s u. { w } ) C_ u )
72 vex 
 |-  u e. _V
73 72 elpw2 
 |-  ( ( s u. { w } ) e. ~P u <-> ( s u. { w } ) C_ u )
74 71 73 sylibr 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> ( s u. { w } ) e. ~P u )
75 65 elin2d 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> s e. Fin )
76 snfi 
 |-  { w } e. Fin
77 unfi 
 |-  ( ( s e. Fin /\ { w } e. Fin ) -> ( s u. { w } ) e. Fin )
78 75 76 77 sylancl 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> ( s u. { w } ) e. Fin )
79 74 78 elind 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> ( s u. { w } ) e. ( ~P u i^i Fin ) )
80 2 ffnd 
 |-  ( ph -> F Fn NN )
81 80 ad3antrrr 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> F Fn NN )
82 simprrr 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. w )
83 82 adantr 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. w )
84 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
85 84 eleq1d 
 |-  ( k = n -> ( ( F ` k ) e. w <-> ( F ` n ) e. w ) )
86 85 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( F ` k ) e. w /\ n e. ( ZZ>= ` j ) ) -> ( F ` n ) e. w )
87 83 86 sylan 
 |-  ( ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) /\ n e. ( ZZ>= ` j ) ) -> ( F ` n ) e. w )
88 elun2 
 |-  ( ( F ` n ) e. w -> ( F ` n ) e. ( U. s u. w ) )
89 87 88 syl 
 |-  ( ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) /\ n e. ( ZZ>= ` j ) ) -> ( F ` n ) e. ( U. s u. w ) )
90 89 adantlr 
 |-  ( ( ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) /\ n e. NN ) /\ n e. ( ZZ>= ` j ) ) -> ( F ` n ) e. ( U. s u. w ) )
91 elnnuz 
 |-  ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
92 91 anbi1i 
 |-  ( ( n e. NN /\ j e. ( ZZ>= ` n ) ) <-> ( n e. ( ZZ>= ` 1 ) /\ j e. ( ZZ>= ` n ) ) )
93 elfzuzb 
 |-  ( n e. ( 1 ... j ) <-> ( n e. ( ZZ>= ` 1 ) /\ j e. ( ZZ>= ` n ) ) )
94 92 93 bitr4i 
 |-  ( ( n e. NN /\ j e. ( ZZ>= ` n ) ) <-> n e. ( 1 ... j ) )
95 simprr 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> ( F " ( 1 ... j ) ) C_ U. s )
96 funimass4 
 |-  ( ( Fun F /\ ( 1 ... j ) C_ dom F ) -> ( ( F " ( 1 ... j ) ) C_ U. s <-> A. n e. ( 1 ... j ) ( F ` n ) e. U. s ) )
97 36 39 96 syl2anc 
 |-  ( ph -> ( ( F " ( 1 ... j ) ) C_ U. s <-> A. n e. ( 1 ... j ) ( F ` n ) e. U. s ) )
98 97 ad3antrrr 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> ( ( F " ( 1 ... j ) ) C_ U. s <-> A. n e. ( 1 ... j ) ( F ` n ) e. U. s ) )
99 95 98 mpbid 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> A. n e. ( 1 ... j ) ( F ` n ) e. U. s )
100 99 r19.21bi 
 |-  ( ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) /\ n e. ( 1 ... j ) ) -> ( F ` n ) e. U. s )
101 elun1 
 |-  ( ( F ` n ) e. U. s -> ( F ` n ) e. ( U. s u. w ) )
102 100 101 syl 
 |-  ( ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) /\ n e. ( 1 ... j ) ) -> ( F ` n ) e. ( U. s u. w ) )
103 94 102 sylan2b 
 |-  ( ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) /\ ( n e. NN /\ j e. ( ZZ>= ` n ) ) ) -> ( F ` n ) e. ( U. s u. w ) )
104 103 anassrs 
 |-  ( ( ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) /\ n e. NN ) /\ j e. ( ZZ>= ` n ) ) -> ( F ` n ) e. ( U. s u. w ) )
105 simprl 
 |-  ( ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) -> j e. NN )
106 105 ad2antlr 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> j e. NN )
107 nnz 
 |-  ( j e. NN -> j e. ZZ )
108 nnz 
 |-  ( n e. NN -> n e. ZZ )
109 uztric 
 |-  ( ( j e. ZZ /\ n e. ZZ ) -> ( n e. ( ZZ>= ` j ) \/ j e. ( ZZ>= ` n ) ) )
110 107 108 109 syl2an 
 |-  ( ( j e. NN /\ n e. NN ) -> ( n e. ( ZZ>= ` j ) \/ j e. ( ZZ>= ` n ) ) )
111 106 110 sylan 
 |-  ( ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) /\ n e. NN ) -> ( n e. ( ZZ>= ` j ) \/ j e. ( ZZ>= ` n ) ) )
112 90 104 111 mpjaodan 
 |-  ( ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) /\ n e. NN ) -> ( F ` n ) e. ( U. s u. w ) )
113 112 ralrimiva 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> A. n e. NN ( F ` n ) e. ( U. s u. w ) )
114 fnfvrnss 
 |-  ( ( F Fn NN /\ A. n e. NN ( F ` n ) e. ( U. s u. w ) ) -> ran F C_ ( U. s u. w ) )
115 81 113 114 syl2anc 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> ran F C_ ( U. s u. w ) )
116 elun2 
 |-  ( A e. w -> A e. ( U. s u. w ) )
117 116 ad2antlr 
 |-  ( ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) -> A e. ( U. s u. w ) )
118 117 ad2antlr 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> A e. ( U. s u. w ) )
119 118 snssd 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> { A } C_ ( U. s u. w ) )
120 115 119 unssd 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> ( ran F u. { A } ) C_ ( U. s u. w ) )
121 uniun 
 |-  U. ( s u. { w } ) = ( U. s u. U. { w } )
122 unisnv 
 |-  U. { w } = w
123 122 uneq2i 
 |-  ( U. s u. U. { w } ) = ( U. s u. w )
124 121 123 eqtri 
 |-  U. ( s u. { w } ) = ( U. s u. w )
125 120 124 sseqtrrdi 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> ( ran F u. { A } ) C_ U. ( s u. { w } ) )
126 unieq 
 |-  ( v = ( s u. { w } ) -> U. v = U. ( s u. { w } ) )
127 126 sseq2d 
 |-  ( v = ( s u. { w } ) -> ( ( ran F u. { A } ) C_ U. v <-> ( ran F u. { A } ) C_ U. ( s u. { w } ) ) )
128 127 rspcev 
 |-  ( ( ( s u. { w } ) e. ( ~P u i^i Fin ) /\ ( ran F u. { A } ) C_ U. ( s u. { w } ) ) -> E. v e. ( ~P u i^i Fin ) ( ran F u. { A } ) C_ U. v )
129 79 125 128 syl2anc 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) /\ ( s e. ( ~P u i^i Fin ) /\ ( F " ( 1 ... j ) ) C_ U. s ) ) -> E. v e. ( ~P u i^i Fin ) ( ran F u. { A } ) C_ U. v )
130 64 129 rexlimddv 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) ) -> E. v e. ( ~P u i^i Fin ) ( ran F u. { A } ) C_ U. v )
131 130 anassrs 
 |-  ( ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( w e. u /\ A e. w ) ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) -> E. v e. ( ~P u i^i Fin ) ( ran F u. { A } ) C_ U. v )
132 23 131 rexlimddv 
 |-  ( ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) /\ ( w e. u /\ A e. w ) ) -> E. v e. ( ~P u i^i Fin ) ( ran F u. { A } ) C_ U. v )
133 14 132 rexlimddv 
 |-  ( ( ph /\ ( u e. ~P J /\ ( ran F u. { A } ) C_ U. u ) ) -> E. v e. ( ~P u i^i Fin ) ( ran F u. { A } ) C_ U. v )
134 133 expr 
 |-  ( ( ph /\ u e. ~P J ) -> ( ( ran F u. { A } ) C_ U. u -> E. v e. ( ~P u i^i Fin ) ( ran F u. { A } ) C_ U. v ) )
135 134 ralrimiva 
 |-  ( ph -> A. u e. ~P J ( ( ran F u. { A } ) C_ U. u -> E. v e. ( ~P u i^i Fin ) ( ran F u. { A } ) C_ U. v ) )
136 7 snssd 
 |-  ( ph -> { A } C_ X )
137 29 136 unssd 
 |-  ( ph -> ( ran F u. { A } ) C_ X )
138 137 55 sseqtrd 
 |-  ( ph -> ( ran F u. { A } ) C_ U. J )
139 57 cmpsub 
 |-  ( ( J e. Top /\ ( ran F u. { A } ) C_ U. J ) -> ( ( J |`t ( ran F u. { A } ) ) e. Comp <-> A. u e. ~P J ( ( ran F u. { A } ) C_ U. u -> E. v e. ( ~P u i^i Fin ) ( ran F u. { A } ) C_ U. v ) ) )
140 53 138 139 syl2anc 
 |-  ( ph -> ( ( J |`t ( ran F u. { A } ) ) e. Comp <-> A. u e. ~P J ( ( ran F u. { A } ) C_ U. u -> E. v e. ( ~P u i^i Fin ) ( ran F u. { A } ) C_ U. v ) ) )
141 135 140 mpbird 
 |-  ( ph -> ( J |`t ( ran F u. { A } ) ) e. Comp )