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

Metamath Proof Explorer

Theorem 1stcfb

Description: For any point A in a first-countable topology, there is a function f : NN --> J enumerating neighborhoods of A which is decreasing and forms a local base. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis 1stcclb.1 
|- X = U. J
Assertion 1stcfb 
|- ( ( J e. 1stc /\ A e. X ) -> E. f ( f : NN --> J /\ A. k e. NN ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( f ` k ) C_ y ) ) )

Proof

Step Hyp Ref Expression
1 1stcclb.1 
 |-  X = U. J
2 1 1stcclb 
 |-  ( ( J e. 1stc /\ A e. X ) -> E. x e. ~P J ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) )
3 simplr 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> A e. X )
4 eleq2 
 |-  ( z = X -> ( A e. z <-> A e. X ) )
5 sseq2 
 |-  ( z = X -> ( w C_ z <-> w C_ X ) )
6 5 anbi2d 
 |-  ( z = X -> ( ( A e. w /\ w C_ z ) <-> ( A e. w /\ w C_ X ) ) )
7 6 rexbidv 
 |-  ( z = X -> ( E. w e. x ( A e. w /\ w C_ z ) <-> E. w e. x ( A e. w /\ w C_ X ) ) )
8 4 7 imbi12d 
 |-  ( z = X -> ( ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) <-> ( A e. X -> E. w e. x ( A e. w /\ w C_ X ) ) ) )
9 simprrr 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) )
10 1stctop 
 |-  ( J e. 1stc -> J e. Top )
11 10 ad2antrr 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> J e. Top )
12 1 topopn 
 |-  ( J e. Top -> X e. J )
13 11 12 syl 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> X e. J )
14 8 9 13 rspcdva 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> ( A e. X -> E. w e. x ( A e. w /\ w C_ X ) ) )
15 3 14 mpd 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> E. w e. x ( A e. w /\ w C_ X ) )
16 simpl 
 |-  ( ( A e. w /\ w C_ X ) -> A e. w )
17 16 reximi 
 |-  ( E. w e. x ( A e. w /\ w C_ X ) -> E. w e. x A e. w )
18 15 17 syl 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> E. w e. x A e. w )
19 eleq2w 
 |-  ( w = a -> ( A e. w <-> A e. a ) )
20 19 cbvrexvw 
 |-  ( E. w e. x A e. w <-> E. a e. x A e. a )
21 18 20 sylib 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> E. a e. x A e. a )
22 rabn0 
 |-  ( { a e. x | A e. a } =/= (/) <-> E. a e. x A e. a )
23 21 22 sylibr 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> { a e. x | A e. a } =/= (/) )
24 vex 
 |-  x e. _V
25 24 rabex 
 |-  { a e. x | A e. a } e. _V
26 25 0sdom 
 |-  ( (/) ~< { a e. x | A e. a } <-> { a e. x | A e. a } =/= (/) )
27 23 26 sylibr 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> (/) ~< { a e. x | A e. a } )
28 ssrab2 
 |-  { a e. x | A e. a } C_ x
29 ssdomg 
 |-  ( x e. _V -> ( { a e. x | A e. a } C_ x -> { a e. x | A e. a } ~<_ x ) )
30 24 28 29 mp2 
 |-  { a e. x | A e. a } ~<_ x
31 simprrl 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> x ~<_ _om )
32 nnenom 
 |-  NN ~~ _om
33 32 ensymi 
 |-  _om ~~ NN
34 domentr 
 |-  ( ( x ~<_ _om /\ _om ~~ NN ) -> x ~<_ NN )
35 31 33 34 sylancl 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> x ~<_ NN )
36 domtr 
 |-  ( ( { a e. x | A e. a } ~<_ x /\ x ~<_ NN ) -> { a e. x | A e. a } ~<_ NN )
37 30 35 36 sylancr 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> { a e. x | A e. a } ~<_ NN )
38 fodomr 
 |-  ( ( (/) ~< { a e. x | A e. a } /\ { a e. x | A e. a } ~<_ NN ) -> E. g g : NN -onto-> { a e. x | A e. a } )
39 27 37 38 syl2anc 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> E. g g : NN -onto-> { a e. x | A e. a } )
40 10 ad3antrrr 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> J e. Top )
41 imassrn 
 |-  ( g " ( 1 ... n ) ) C_ ran g
42 forn 
 |-  ( g : NN -onto-> { a e. x | A e. a } -> ran g = { a e. x | A e. a } )
43 42 ad2antll 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> ran g = { a e. x | A e. a } )
44 simprll 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> x e. ~P J )
45 44 elpwid 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> x C_ J )
46 28 45 sstrid 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> { a e. x | A e. a } C_ J )
47 43 46 eqsstrd 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> ran g C_ J )
48 47 adantr 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> ran g C_ J )
49 41 48 sstrid 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> ( g " ( 1 ... n ) ) C_ J )
50 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
51 fof 
 |-  ( g : NN -onto-> { a e. x | A e. a } -> g : NN --> { a e. x | A e. a } )
52 51 ad2antll 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> g : NN --> { a e. x | A e. a } )
53 52 fdmd 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> dom g = NN )
54 50 53 sseqtrrid 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> ( 1 ... n ) C_ dom g )
55 54 adantr 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> ( 1 ... n ) C_ dom g )
56 sseqin2 
 |-  ( ( 1 ... n ) C_ dom g <-> ( dom g i^i ( 1 ... n ) ) = ( 1 ... n ) )
57 55 56 sylib 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> ( dom g i^i ( 1 ... n ) ) = ( 1 ... n ) )
58 elfz1end 
 |-  ( n e. NN <-> n e. ( 1 ... n ) )
59 ne0i 
 |-  ( n e. ( 1 ... n ) -> ( 1 ... n ) =/= (/) )
60 59 adantl 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. ( 1 ... n ) ) -> ( 1 ... n ) =/= (/) )
61 58 60 sylan2b 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> ( 1 ... n ) =/= (/) )
62 57 61 eqnetrd 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> ( dom g i^i ( 1 ... n ) ) =/= (/) )
63 imadisj 
 |-  ( ( g " ( 1 ... n ) ) = (/) <-> ( dom g i^i ( 1 ... n ) ) = (/) )
64 63 necon3bii 
 |-  ( ( g " ( 1 ... n ) ) =/= (/) <-> ( dom g i^i ( 1 ... n ) ) =/= (/) )
65 62 64 sylibr 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> ( g " ( 1 ... n ) ) =/= (/) )
66 fzfid 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> ( 1 ... n ) e. Fin )
67 52 ffund 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> Fun g )
68 fores 
 |-  ( ( Fun g /\ ( 1 ... n ) C_ dom g ) -> ( g |` ( 1 ... n ) ) : ( 1 ... n ) -onto-> ( g " ( 1 ... n ) ) )
69 67 55 68 syl2an2r 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> ( g |` ( 1 ... n ) ) : ( 1 ... n ) -onto-> ( g " ( 1 ... n ) ) )
70 fofi 
 |-  ( ( ( 1 ... n ) e. Fin /\ ( g |` ( 1 ... n ) ) : ( 1 ... n ) -onto-> ( g " ( 1 ... n ) ) ) -> ( g " ( 1 ... n ) ) e. Fin )
71 66 69 70 syl2anc 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> ( g " ( 1 ... n ) ) e. Fin )
72 fiinopn 
 |-  ( J e. Top -> ( ( ( g " ( 1 ... n ) ) C_ J /\ ( g " ( 1 ... n ) ) =/= (/) /\ ( g " ( 1 ... n ) ) e. Fin ) -> |^| ( g " ( 1 ... n ) ) e. J ) )
73 72 imp 
 |-  ( ( J e. Top /\ ( ( g " ( 1 ... n ) ) C_ J /\ ( g " ( 1 ... n ) ) =/= (/) /\ ( g " ( 1 ... n ) ) e. Fin ) ) -> |^| ( g " ( 1 ... n ) ) e. J )
74 40 49 65 71 73 syl13anc 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ n e. NN ) -> |^| ( g " ( 1 ... n ) ) e. J )
75 74 fmpttd 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) : NN --> J )
76 imassrn 
 |-  ( g " ( 1 ... k ) ) C_ ran g
77 43 adantr 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> ran g = { a e. x | A e. a } )
78 76 77 sseqtrid 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> ( g " ( 1 ... k ) ) C_ { a e. x | A e. a } )
79 id 
 |-  ( A e. n -> A e. n )
80 79 rgenw 
 |-  A. n e. x ( A e. n -> A e. n )
81 eleq2w 
 |-  ( a = n -> ( A e. a <-> A e. n ) )
82 81 ralrab 
 |-  ( A. n e. { a e. x | A e. a } A e. n <-> A. n e. x ( A e. n -> A e. n ) )
83 80 82 mpbir 
 |-  A. n e. { a e. x | A e. a } A e. n
84 ssralv 
 |-  ( ( g " ( 1 ... k ) ) C_ { a e. x | A e. a } -> ( A. n e. { a e. x | A e. a } A e. n -> A. n e. ( g " ( 1 ... k ) ) A e. n ) )
85 78 83 84 mpisyl 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> A. n e. ( g " ( 1 ... k ) ) A e. n )
86 elintg 
 |-  ( A e. X -> ( A e. |^| ( g " ( 1 ... k ) ) <-> A. n e. ( g " ( 1 ... k ) ) A e. n ) )
87 86 ad3antlr 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> ( A e. |^| ( g " ( 1 ... k ) ) <-> A. n e. ( g " ( 1 ... k ) ) A e. n ) )
88 85 87 mpbird 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> A e. |^| ( g " ( 1 ... k ) ) )
89 eqid 
 |-  ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) )
90 oveq2 
 |-  ( n = k -> ( 1 ... n ) = ( 1 ... k ) )
91 90 imaeq2d 
 |-  ( n = k -> ( g " ( 1 ... n ) ) = ( g " ( 1 ... k ) ) )
92 91 inteqd 
 |-  ( n = k -> |^| ( g " ( 1 ... n ) ) = |^| ( g " ( 1 ... k ) ) )
93 simpr 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> k e. NN )
94 74 ralrimiva 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> A. n e. NN |^| ( g " ( 1 ... n ) ) e. J )
95 92 eleq1d 
 |-  ( n = k -> ( |^| ( g " ( 1 ... n ) ) e. J <-> |^| ( g " ( 1 ... k ) ) e. J ) )
96 95 rspccva 
 |-  ( ( A. n e. NN |^| ( g " ( 1 ... n ) ) e. J /\ k e. NN ) -> |^| ( g " ( 1 ... k ) ) e. J )
97 94 96 sylan 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> |^| ( g " ( 1 ... k ) ) e. J )
98 89 92 93 97 fvmptd3 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) = |^| ( g " ( 1 ... k ) ) )
99 88 98 eleqtrrd 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> A e. ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) )
100 fzssp1 
 |-  ( 1 ... k ) C_ ( 1 ... ( k + 1 ) )
101 imass2 
 |-  ( ( 1 ... k ) C_ ( 1 ... ( k + 1 ) ) -> ( g " ( 1 ... k ) ) C_ ( g " ( 1 ... ( k + 1 ) ) ) )
102 100 101 mp1i 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> ( g " ( 1 ... k ) ) C_ ( g " ( 1 ... ( k + 1 ) ) ) )
103 intss 
 |-  ( ( g " ( 1 ... k ) ) C_ ( g " ( 1 ... ( k + 1 ) ) ) -> |^| ( g " ( 1 ... ( k + 1 ) ) ) C_ |^| ( g " ( 1 ... k ) ) )
104 102 103 syl 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> |^| ( g " ( 1 ... ( k + 1 ) ) ) C_ |^| ( g " ( 1 ... k ) ) )
105 oveq2 
 |-  ( n = ( k + 1 ) -> ( 1 ... n ) = ( 1 ... ( k + 1 ) ) )
106 105 imaeq2d 
 |-  ( n = ( k + 1 ) -> ( g " ( 1 ... n ) ) = ( g " ( 1 ... ( k + 1 ) ) ) )
107 106 inteqd 
 |-  ( n = ( k + 1 ) -> |^| ( g " ( 1 ... n ) ) = |^| ( g " ( 1 ... ( k + 1 ) ) ) )
108 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
109 108 adantl 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> ( k + 1 ) e. NN )
110 107 eleq1d 
 |-  ( n = ( k + 1 ) -> ( |^| ( g " ( 1 ... n ) ) e. J <-> |^| ( g " ( 1 ... ( k + 1 ) ) ) e. J ) )
111 110 rspccva 
 |-  ( ( A. n e. NN |^| ( g " ( 1 ... n ) ) e. J /\ ( k + 1 ) e. NN ) -> |^| ( g " ( 1 ... ( k + 1 ) ) ) e. J )
112 94 108 111 syl2an 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> |^| ( g " ( 1 ... ( k + 1 ) ) ) e. J )
113 89 107 109 112 fvmptd3 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) = |^| ( g " ( 1 ... ( k + 1 ) ) ) )
114 104 113 98 3sstr4d 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) C_ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) )
115 99 114 jca 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> ( A e. ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) /\ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) C_ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) ) )
116 115 ralrimiva 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> A. k e. NN ( A e. ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) /\ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) C_ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) ) )
117 simprlr 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) )
118 eleq2w 
 |-  ( z = y -> ( A e. z <-> A e. y ) )
119 sseq2 
 |-  ( z = y -> ( w C_ z <-> w C_ y ) )
120 119 anbi2d 
 |-  ( z = y -> ( ( A e. w /\ w C_ z ) <-> ( A e. w /\ w C_ y ) ) )
121 120 rexbidv 
 |-  ( z = y -> ( E. w e. x ( A e. w /\ w C_ z ) <-> E. w e. x ( A e. w /\ w C_ y ) ) )
122 118 121 imbi12d 
 |-  ( z = y -> ( ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) <-> ( A e. y -> E. w e. x ( A e. w /\ w C_ y ) ) ) )
123 122 rspccva 
 |-  ( ( A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) /\ y e. J ) -> ( A e. y -> E. w e. x ( A e. w /\ w C_ y ) ) )
124 117 123 sylan 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> ( A e. y -> E. w e. x ( A e. w /\ w C_ y ) ) )
125 eleq2w 
 |-  ( a = w -> ( A e. a <-> A e. w ) )
126 125 rexrab 
 |-  ( E. w e. { a e. x | A e. a } w C_ y <-> E. w e. x ( A e. w /\ w C_ y ) )
127 43 rexeqdv 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> ( E. w e. ran g w C_ y <-> E. w e. { a e. x | A e. a } w C_ y ) )
128 fofn 
 |-  ( g : NN -onto-> { a e. x | A e. a } -> g Fn NN )
129 128 ad2antll 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> g Fn NN )
130 sseq1 
 |-  ( w = ( g ` k ) -> ( w C_ y <-> ( g ` k ) C_ y ) )
131 130 rexrn 
 |-  ( g Fn NN -> ( E. w e. ran g w C_ y <-> E. k e. NN ( g ` k ) C_ y ) )
132 129 131 syl 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> ( E. w e. ran g w C_ y <-> E. k e. NN ( g ` k ) C_ y ) )
133 127 132 bitr3d 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> ( E. w e. { a e. x | A e. a } w C_ y <-> E. k e. NN ( g ` k ) C_ y ) )
134 133 adantr 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> ( E. w e. { a e. x | A e. a } w C_ y <-> E. k e. NN ( g ` k ) C_ y ) )
135 elfz1end 
 |-  ( k e. NN <-> k e. ( 1 ... k ) )
136 fz1ssnn 
 |-  ( 1 ... k ) C_ NN
137 53 adantr 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> dom g = NN )
138 136 137 sseqtrrid 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> ( 1 ... k ) C_ dom g )
139 funfvima2 
 |-  ( ( Fun g /\ ( 1 ... k ) C_ dom g ) -> ( k e. ( 1 ... k ) -> ( g ` k ) e. ( g " ( 1 ... k ) ) ) )
140 67 138 139 syl2an2r 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> ( k e. ( 1 ... k ) -> ( g ` k ) e. ( g " ( 1 ... k ) ) ) )
141 140 imp 
 |-  ( ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) /\ k e. ( 1 ... k ) ) -> ( g ` k ) e. ( g " ( 1 ... k ) ) )
142 135 141 sylan2b 
 |-  ( ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) /\ k e. NN ) -> ( g ` k ) e. ( g " ( 1 ... k ) ) )
143 intss1 
 |-  ( ( g ` k ) e. ( g " ( 1 ... k ) ) -> |^| ( g " ( 1 ... k ) ) C_ ( g ` k ) )
144 sstr2 
 |-  ( |^| ( g " ( 1 ... k ) ) C_ ( g ` k ) -> ( ( g ` k ) C_ y -> |^| ( g " ( 1 ... k ) ) C_ y ) )
145 142 143 144 3syl 
 |-  ( ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) /\ k e. NN ) -> ( ( g ` k ) C_ y -> |^| ( g " ( 1 ... k ) ) C_ y ) )
146 145 reximdva 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> ( E. k e. NN ( g ` k ) C_ y -> E. k e. NN |^| ( g " ( 1 ... k ) ) C_ y ) )
147 134 146 sylbid 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> ( E. w e. { a e. x | A e. a } w C_ y -> E. k e. NN |^| ( g " ( 1 ... k ) ) C_ y ) )
148 126 147 biimtrrid 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> ( E. w e. x ( A e. w /\ w C_ y ) -> E. k e. NN |^| ( g " ( 1 ... k ) ) C_ y ) )
149 124 148 syld 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> ( A e. y -> E. k e. NN |^| ( g " ( 1 ... k ) ) C_ y ) )
150 98 sseq1d 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ k e. NN ) -> ( ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y <-> |^| ( g " ( 1 ... k ) ) C_ y ) )
151 150 rexbidva 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> ( E. k e. NN ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y <-> E. k e. NN |^| ( g " ( 1 ... k ) ) C_ y ) )
152 151 adantr 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> ( E. k e. NN ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y <-> E. k e. NN |^| ( g " ( 1 ... k ) ) C_ y ) )
153 149 152 sylibrd 
 |-  ( ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) /\ y e. J ) -> ( A e. y -> E. k e. NN ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y ) )
154 153 ralrimiva 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> A. y e. J ( A e. y -> E. k e. NN ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y ) )
155 nnex 
 |-  NN e. _V
156 155 mptex 
 |-  ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) e. _V
157 feq1 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( f : NN --> J <-> ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) : NN --> J ) )
158 fveq1 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( f ` k ) = ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) )
159 158 eleq2d 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( A e. ( f ` k ) <-> A e. ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) ) )
160 fveq1 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( f ` ( k + 1 ) ) = ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) )
161 160 158 sseq12d 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( ( f ` ( k + 1 ) ) C_ ( f ` k ) <-> ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) C_ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) ) )
162 159 161 anbi12d 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) <-> ( A e. ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) /\ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) C_ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) ) ) )
163 162 ralbidv 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( A. k e. NN ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) <-> A. k e. NN ( A e. ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) /\ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) C_ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) ) ) )
164 158 sseq1d 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( ( f ` k ) C_ y <-> ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y ) )
165 164 rexbidv 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( E. k e. NN ( f ` k ) C_ y <-> E. k e. NN ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y ) )
166 165 imbi2d 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( ( A e. y -> E. k e. NN ( f ` k ) C_ y ) <-> ( A e. y -> E. k e. NN ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y ) ) )
167 166 ralbidv 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( A. y e. J ( A e. y -> E. k e. NN ( f ` k ) C_ y ) <-> A. y e. J ( A e. y -> E. k e. NN ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y ) ) )
168 157 163 167 3anbi123d 
 |-  ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( ( f : NN --> J /\ A. k e. NN ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( f ` k ) C_ y ) ) <-> ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) : NN --> J /\ A. k e. NN ( A e. ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) /\ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) C_ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y ) ) ) )
169 156 168 spcev 
 |-  ( ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) : NN --> J /\ A. k e. NN ( A e. ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) /\ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) C_ ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y ) ) -> E. f ( f : NN --> J /\ A. k e. NN ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( f ` k ) C_ y ) ) )
170 75 116 154 169 syl3anc 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) /\ g : NN -onto-> { a e. x | A e. a } ) ) -> E. f ( f : NN --> J /\ A. k e. NN ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( f ` k ) C_ y ) ) )
171 170 expr 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) -> ( g : NN -onto-> { a e. x | A e. a } -> E. f ( f : NN --> J /\ A. k e. NN ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( f ` k ) C_ y ) ) ) )
172 171 adantrrl 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> ( g : NN -onto-> { a e. x | A e. a } -> E. f ( f : NN --> J /\ A. k e. NN ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( f ` k ) C_ y ) ) ) )
173 172 exlimdv 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> ( E. g g : NN -onto-> { a e. x | A e. a } -> E. f ( f : NN --> J /\ A. k e. NN ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( f ` k ) C_ y ) ) ) )
174 39 173 mpd 
 |-  ( ( ( J e. 1stc /\ A e. X ) /\ ( x e. ~P J /\ ( x ~<_ _om /\ A. z e. J ( A e. z -> E. w e. x ( A e. w /\ w C_ z ) ) ) ) ) -> E. f ( f : NN --> J /\ A. k e. NN ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( f ` k ) C_ y ) ) )
175 2 174 rexlimddv 
 |-  ( ( J e. 1stc /\ A e. X ) -> E. f ( f : NN --> J /\ A. k e. NN ( A e. ( f ` k ) /\ ( f ` ( k + 1 ) ) C_ ( f ` k ) ) /\ A. y e. J ( A e. y -> E. k e. NN ( f ` k ) C_ y ) ) )