# 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 } ) )`
` |-  ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( w e. u /\ A e. w ) /\ ( j e. NN /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. w ) ) -> A e. ( U. s u. w ) )`
` |-  ( ( ( ( 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 vex
` |-  w e. _V`
123 122 unisn
` |-  U. { w } = w`
124 123 uneq2i
` |-  ( U. s u. U. { w } ) = ( U. s u. w )`
125 121 124 eqtri
` |-  U. ( s u. { w } ) = ( U. s u. w )`
126 120 125 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 } ) )`
127 unieq
` |-  ( v = ( s u. { w } ) -> U. v = U. ( s u. { w } ) )`
128 127 sseq2d
` |-  ( v = ( s u. { w } ) -> ( ( ran F u. { A } ) C_ U. v <-> ( ran F u. { A } ) C_ U. ( s u. { w } ) ) )`
129 128 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 )`
130 79 126 129 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 )`
131 64 130 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 )`
132 131 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 )`
133 23 132 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 )`
134 14 133 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 )`
135 134 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 ) )`
136 135 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 ) )`
137 7 snssd
` |-  ( ph -> { A } C_ X )`
138 29 137 unssd
` |-  ( ph -> ( ran F u. { A } ) C_ X )`
139 138 55 sseqtrd
` |-  ( ph -> ( ran F u. { A } ) C_ U. J )`
140 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 ) ) )`
141 53 139 140 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 ) ) )`
142 136 141 mpbird
` |-  ( ph -> ( J |`t ( ran F u. { A } ) ) e. Comp )`