MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1stcfb Structured version   Visualization version   Unicode version
Theorem 1stcfb 21248
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.)
Hypothesis
Ref Expression
1stcclb.1 |- X = U. J
Assertion
Ref Expression
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 ) ) )
Distinct variable groups:   f, k, y, A   f, J, k, y   k, X, y
Allowed substitution hint:   X( f)
Proof of Theorem 1stcfb
Dummy variables a g n w x z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1stcclb.1 . . 3 |- X = U. J
211stcclb 21247 . 2 |- ( ( 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 1stctop 21246 . . . . . . . . . . 11 |- ( J e. 1stc -> J e. Top )
43ad2antrr 762 . . . . . . . . . 10 |- ( ( ( 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 )
51topopn 20711 . . . . . . . . . 10 |- ( J e. Top -> X e. J )
64, 5syl 17 . . . . . . . . 9 |- ( ( ( 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 )
7 simprrr 805 . . . . . . . . 9 |- ( ( ( 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 ) ) )
8 simplr 792 . . . . . . . . 9 |- ( ( ( 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 )
9 eleq2 2690 . . . . . . . . . . 11 |- ( z = X -> ( A e. z <-> A e. X ) )
10 sseq2 3627 . . . . . . . . . . . . 13 |- ( z = X -> ( w C_ z <-> w C_ X ) )
1110anbi2d 740 . . . . . . . . . . . 12 |- ( z = X -> ( ( A e. w /\ w C_ z ) <-> ( A e. w /\ w C_ X ) ) )
1211rexbidv 3052 . . . . . . . . . . 11 |- ( z = X -> ( E. w e. x ( A e. w /\ w C_ z ) <-> E. w e. x ( A e. w /\ w C_ X ) ) )
139, 12imbi12d 334 . . . . . . . . . 10 |- ( 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 ) ) ) )
1413rspcv 3305 . . . . . . . . 9 |- ( X e. J -> ( 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 ) ) ) )
156, 7, 8, 14syl3c 66 . . . . . . . 8 |- ( ( ( 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 473 . . . . . . . . 9 |- ( ( A e. w /\ w C_ X ) -> A e. w )
1716reximi 3011 . . . . . . . 8 |- ( E. w e. x ( A e. w /\ w C_ X ) -> E. w e. x A e. w )
1815, 17syl 17 . . . . . . 7 |- ( ( ( 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 eleq2 2690 . . . . . . . 8 |- ( w = a -> ( A e. w <-> A e. a ) )
2019cbvrexv 3172 . . . . . . 7 |- ( E. w e. x A e. w <-> E. a e. x A e. a )
2118, 20sylib 208 . . . . . 6 |- ( ( ( 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 3958 . . . . . 6 |- ( { a e. x | A e. a } =/= (/) <-> E. a e. x A e. a )
2321, 22sylibr 224 . . . . 5 |- ( ( ( 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 3203 . . . . . . 7 |- x e. _V
2524rabex 4813 . . . . . 6 |- { a e. x | A e. a } e. _V
26250sdom 8091 . . . . 5 |- ( (/) ~< { a e. x | A e. a } <-> { a e. x | A e. a } =/= (/) )
2723, 26sylibr 224 . . . 4 |- ( ( ( 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 3687 . . . . . 6 |- { a e. x | A e. a } C_ x
29 ssdomg 8001 . . . . . 6 |- ( x e. _V -> ( { a e. x | A e. a } C_ x -> { a e. x | A e. a } ~<_ x ) )
3024, 28, 29mp2 9 . . . . 5 |- { a e. x | A e. a } ~<_ x
31 simprrl 804 . . . . . 6 |- ( ( ( 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 12779 . . . . . . 7 |- NN ~~ om
3332ensymi 8006 . . . . . 6 |- om ~~ NN
34 domentr 8015 . . . . . 6 |- ( ( x ~<_ om /\ om ~~ NN ) -> x ~<_ NN )
3531, 33, 34sylancl 694 . . . . 5 |- ( ( ( 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 8009 . . . . 5 |- ( ( { a e. x | A e. a } ~<_ x /\ x ~<_ NN ) -> { a e. x | A e. a } ~<_ NN )
3730, 35, 36sylancr 695 . . . 4 |- ( ( ( 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 8111 . . . 4 |- ( ( (/) ~< { a e. x | A e. a } /\ { a e. x | A e. a } ~<_ NN ) -> E. g g : NN -onto-> { a e. x | A e. a } )
3927, 37, 38syl2anc 693 . . 3 |- ( ( ( 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 } )
403ad3antrrr 766 . . . . . . . . 9 |- ( ( ( ( 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 5477 . . . . . . . . . 10 |- ( g " ( 1 ... n ) ) C_ ran g
42 forn 6118 . . . . . . . . . . . . 13 |- ( g : NN -onto-> { a e. x | A e. a } -> ran g = { a e. x | A e. a } )
4342ad2antll 765 . . . . . . . . . . . 12 |- ( ( ( 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 802 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
4544elpwid 4170 . . . . . . . . . . . . 13 |- ( ( ( 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 )
4628, 45syl5ss 3614 . . . . . . . . . . . 12 |- ( ( ( 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 )
4743, 46eqsstrd 3639 . . . . . . . . . . 11 |- ( ( ( 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 )
4847adantr 481 . . . . . . . . . 10 |- ( ( ( ( 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 )
4941, 48syl5ss 3614 . . . . . . . . 9 |- ( ( ( ( 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 elfznn 12370 . . . . . . . . . . . . . . 15 |- ( k e. ( 1 ... n ) -> k e. NN )
5150ssriv 3607 . . . . . . . . . . . . . 14 |- ( 1 ... n ) C_ NN
52 fof 6115 . . . . . . . . . . . . . . . 16 |- ( g : NN -onto-> { a e. x | A e. a } -> g : NN --> { a e. x | A e. a } )
5352ad2antll 765 . . . . . . . . . . . . . . 15 |- ( ( ( 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 } )
54 fdm 6051 . . . . . . . . . . . . . . 15 |- ( g : NN --> { a e. x | A e. a } -> dom g = NN )
5553, 54syl 17 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
5651, 55syl5sseqr 3654 . . . . . . . . . . . . 13 |- ( ( ( 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 )
5756adantr 481 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
58 sseqin2 3817 . . . . . . . . . . . 12 |- ( ( 1 ... n ) C_ dom g <-> ( dom g i^i ( 1 ... n ) ) = ( 1 ... n ) )
5957, 58sylib 208 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
60 elfz1end 12371 . . . . . . . . . . . 12 |- ( n e. NN <-> n e. ( 1 ... n ) )
61 ne0i 3921 . . . . . . . . . . . . 13 |- ( n e. ( 1 ... n ) -> ( 1 ... n ) =/= (/) )
6261adantl 482 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) =/= (/) )
6360, 62sylan2b 492 . . . . . . . . . . 11 |- ( ( ( ( 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 ) =/= (/) )
6459, 63eqnetrd 2861 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) =/= (/) )
65 imadisj 5484 . . . . . . . . . . 11 |- ( ( g " ( 1 ... n ) ) = (/) <-> ( dom g i^i ( 1 ... n ) ) = (/) )
6665necon3bii 2846 . . . . . . . . . 10 |- ( ( g " ( 1 ... n ) ) =/= (/) <-> ( dom g i^i ( 1 ... n ) ) =/= (/) )
6764, 66sylibr 224 . . . . . . . . 9 |- ( ( ( ( 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 ) ) =/= (/) )
68 fzfid 12772 . . . . . . . . . 10 |- ( ( ( ( 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 )
69 ffun 6048 . . . . . . . . . . . . 13 |- ( g : NN --> { a e. x | A e. a } -> Fun g )
7053, 69syl 17 . . . . . . . . . . . 12 |- ( ( ( 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 )
7170adantr 481 . . . . . . . . . . 11 |- ( ( ( ( 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 ) -> Fun g )
72 fores 6124 . . . . . . . . . . 11 |- ( ( Fun g /\ ( 1 ... n ) C_ dom g ) -> ( g |` ( 1 ... n ) ) : ( 1 ... n ) -onto-> ( g " ( 1 ... n ) ) )
7371, 57, 72syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
74 fofi 8252 . . . . . . . . . 10 |- ( ( ( 1 ... n ) e. Fin /\ ( g |` ( 1 ... n ) ) : ( 1 ... n ) -onto-> ( g " ( 1 ... n ) ) ) -> ( g " ( 1 ... n ) ) e. Fin )
7568, 73, 74syl2anc 693 . . . . . . . . 9 |- ( ( ( ( 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 )
76 fiinopn 20706 . . . . . . . . . 10 |- ( J e. Top -> ( ( ( g " ( 1 ... n ) ) C_ J /\ ( g " ( 1 ... n ) ) =/= (/) /\ ( g " ( 1 ... n ) ) e. Fin ) -> |^| ( g " ( 1 ... n ) ) e. J ) )
7776imp 445 . . . . . . . . 9 |- ( ( J e. Top /\ ( ( g " ( 1 ... n ) ) C_ J /\ ( g " ( 1 ... n ) ) =/= (/) /\ ( g " ( 1 ... n ) ) e. Fin ) ) -> |^| ( g " ( 1 ... n ) ) e. J )
7840, 49, 67, 75, 77syl13anc 1328 . . . . . . . 8 |- ( ( ( ( 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 )
79 eqid 2622 . . . . . . . 8 |- ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) )
8078, 79fmptd 6385 . . . . . . 7 |- ( ( ( 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 )
81 imassrn 5477 . . . . . . . . . . . . 13 |- ( g " ( 1 ... k ) ) C_ ran g
8243adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( 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 } )
8381, 82syl5sseq 3653 . . . . . . . . . . . 12 |- ( ( ( ( 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 } )
84 id 22 . . . . . . . . . . . . . 14 |- ( A e. n -> A e. n )
8584rgenw 2924 . . . . . . . . . . . . 13 |- A. n e. x ( A e. n -> A e. n )
86 eleq2 2690 . . . . . . . . . . . . . 14 |- ( a = n -> ( A e. a <-> A e. n ) )
8786ralrab 3368 . . . . . . . . . . . . 13 |- ( A. n e. { a e. x | A e. a } A e. n <-> A. n e. x ( A e. n -> A e. n ) )
8885, 87mpbir 221 . . . . . . . . . . . 12 |- A. n e. { a e. x | A e. a } A e. n
89 ssralv 3666 . . . . . . . . . . . 12 |- ( ( 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 ) )
9083, 88, 89mpisyl 21 . . . . . . . . . . 11 |- ( ( ( ( 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 )
91 elintg 4483 . . . . . . . . . . . 12 |- ( A e. X -> ( A e. |^| ( g " ( 1 ... k ) ) <-> A. n e. ( g " ( 1 ... k ) ) A e. n ) )
9291ad3antlr 767 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
9390, 92mpbird 247 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
94 simpr 477 . . . . . . . . . . 11 |- ( ( ( ( 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 )
9578ralrimiva 2966 . . . . . . . . . . . 12 |- ( ( ( 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 )
96 oveq2 6658 . . . . . . . . . . . . . . . 16 |- ( n = k -> ( 1 ... n ) = ( 1 ... k ) )
9796imaeq2d 5466 . . . . . . . . . . . . . . 15 |- ( n = k -> ( g " ( 1 ... n ) ) = ( g " ( 1 ... k ) ) )
9897inteqd 4480 . . . . . . . . . . . . . 14 |- ( n = k -> |^| ( g " ( 1 ... n ) ) = |^| ( g " ( 1 ... k ) ) )
9998eleq1d 2686 . . . . . . . . . . . . 13 |- ( n = k -> ( |^| ( g " ( 1 ... n ) ) e. J <-> |^| ( g " ( 1 ... k ) ) e. J ) )
10099rspccva 3308 . . . . . . . . . . . 12 |- ( ( A. n e. NN |^| ( g " ( 1 ... n ) ) e. J /\ k e. NN ) -> |^| ( g " ( 1 ... k ) ) e. J )
10195, 100sylan 488 . . . . . . . . . . 11 |- ( ( ( ( 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 )
10298, 79fvmptg 6280 . . . . . . . . . . 11 |- ( ( k e. NN /\ |^| ( g " ( 1 ... k ) ) e. J ) -> ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) = |^| ( g " ( 1 ... k ) ) )
10394, 101, 102syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
10493, 103eleqtrrd 2704 . . . . . . . . 9 |- ( ( ( ( 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 ) )
105 fzssp1 12384 . . . . . . . . . . . 12 |- ( 1 ... k ) C_ ( 1 ... ( k + 1 ) )
106 imass2 5501 . . . . . . . . . . . 12 |- ( ( 1 ... k ) C_ ( 1 ... ( k + 1 ) ) -> ( g " ( 1 ... k ) ) C_ ( g " ( 1 ... ( k + 1 ) ) ) )
107105, 106mp1i 13 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) )
108 intss 4498 . . . . . . . . . . 11 |- ( ( g " ( 1 ... k ) ) C_ ( g " ( 1 ... ( k + 1 ) ) ) -> |^| ( g " ( 1 ... ( k + 1 ) ) ) C_ |^| ( g " ( 1 ... k ) ) )
109107, 108syl 17 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
110 peano2nn 11032 . . . . . . . . . . . 12 |- ( k e. NN -> ( k + 1 ) e. NN )
111110adantl 482 . . . . . . . . . . 11 |- ( ( ( ( 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 )
112 oveq2 6658 . . . . . . . . . . . . . . . 16 |- ( n = ( k + 1 ) -> ( 1 ... n ) = ( 1 ... ( k + 1 ) ) )
113112imaeq2d 5466 . . . . . . . . . . . . . . 15 |- ( n = ( k + 1 ) -> ( g " ( 1 ... n ) ) = ( g " ( 1 ... ( k + 1 ) ) ) )
114113inteqd 4480 . . . . . . . . . . . . . 14 |- ( n = ( k + 1 ) -> |^| ( g " ( 1 ... n ) ) = |^| ( g " ( 1 ... ( k + 1 ) ) ) )
115114eleq1d 2686 . . . . . . . . . . . . 13 |- ( n = ( k + 1 ) -> ( |^| ( g " ( 1 ... n ) ) e. J <-> |^| ( g " ( 1 ... ( k + 1 ) ) ) e. J ) )
116115rspccva 3308 . . . . . . . . . . . 12 |- ( ( A. n e. NN |^| ( g " ( 1 ... n ) ) e. J /\ ( k + 1 ) e. NN ) -> |^| ( g " ( 1 ... ( k + 1 ) ) ) e. J )
11795, 110, 116syl2an 494 . . . . . . . . . . 11 |- ( ( ( ( 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 )
118114, 79fvmptg 6280 . . . . . . . . . . 11 |- ( ( ( k + 1 ) e. NN /\ |^| ( g " ( 1 ... ( k + 1 ) ) ) e. J ) -> ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) = |^| ( g " ( 1 ... ( k + 1 ) ) ) )
119111, 117, 118syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) ) )
120109, 119, 1033sstr4d 3648 . . . . . . . . 9 |- ( ( ( ( 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 ) )
121104, 120jca 554 . . . . . . . 8 |- ( ( ( ( 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 ) ) )
122121ralrimiva 2966 . . . . . . 7 |- ( ( ( 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 ) ) )
123 simprlr 803 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
124 eleq2 2690 . . . . . . . . . . . . 13 |- ( z = y -> ( A e. z <-> A e. y ) )
125 sseq2 3627 . . . . . . . . . . . . . . 15 |- ( z = y -> ( w C_ z <-> w C_ y ) )
126125anbi2d 740 . . . . . . . . . . . . . 14 |- ( z = y -> ( ( A e. w /\ w C_ z ) <-> ( A e. w /\ w C_ y ) ) )
127126rexbidv 3052 . . . . . . . . . . . . 13 |- ( z = y -> ( E. w e. x ( A e. w /\ w C_ z ) <-> E. w e. x ( A e. w /\ w C_ y ) ) )
128124, 127imbi12d 334 . . . . . . . . . . . 12 |- ( 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 ) ) ) )
129128rspccva 3308 . . . . . . . . . . 11 |- ( ( 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 ) ) )
130123, 129sylan 488 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
131 eleq2 2690 . . . . . . . . . . . 12 |- ( a = w -> ( A e. a <-> A e. w ) )
132131rexrab 3370 . . . . . . . . . . 11 |- ( E. w e. { a e. x | A e. a } w C_ y <-> E. w e. x ( A e. w /\ w C_ y ) )
13343rexeqdv 3145 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
134 fofn 6117 . . . . . . . . . . . . . . . 16 |- ( g : NN -onto-> { a e. x | A e. a } -> g Fn NN )
135134ad2antll 765 . . . . . . . . . . . . . . 15 |- ( ( ( 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 )
136 sseq1 3626 . . . . . . . . . . . . . . . 16 |- ( w = ( g ` k ) -> ( w C_ y <-> ( g ` k ) C_ y ) )
137136rexrn 6361 . . . . . . . . . . . . . . 15 |- ( g Fn NN -> ( E. w e. ran g w C_ y <-> E. k e. NN ( g ` k ) C_ y ) )
138135, 137syl 17 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
139133, 138bitr3d 270 . . . . . . . . . . . . 13 |- ( ( ( 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 ) )
140139adantr 481 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
141 elfz1end 12371 . . . . . . . . . . . . . . 15 |- ( k e. NN <-> k e. ( 1 ... k ) )
14270adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) -> Fun g )
143 elfznn 12370 . . . . . . . . . . . . . . . . . . 19 |- ( n e. ( 1 ... k ) -> n e. NN )
144143ssriv 3607 . . . . . . . . . . . . . . . . . 18 |- ( 1 ... k ) C_ NN
14555adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 )
146144, 145syl5sseqr 3654 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
147 funfvima2 6493 . . . . . . . . . . . . . . . . 17 |- ( ( Fun g /\ ( 1 ... k ) C_ dom g ) -> ( k e. ( 1 ... k ) -> ( g ` k ) e. ( g " ( 1 ... k ) ) ) )
148142, 146, 147syl2anc 693 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) ) )
149148imp 445 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) ) )
150141, 149sylan2b 492 . . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 ) ) )
151 intss1 4492 . . . . . . . . . . . . . 14 |- ( ( g ` k ) e. ( g " ( 1 ... k ) ) -> |^| ( g " ( 1 ... k ) ) C_ ( g ` k ) )
152 sstr2 3610 . . . . . . . . . . . . . 14 |- ( |^| ( g " ( 1 ... k ) ) C_ ( g ` k ) -> ( ( g ` k ) C_ y -> |^| ( g " ( 1 ... k ) ) C_ y ) )
153150, 151, 1523syl 18 . . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) )
154153reximdva 3017 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
155140, 154sylbid 230 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
156132, 155syl5bir 233 . . . . . . . . . 10 |- ( ( ( ( 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 ) )
157130, 156syld 47 . . . . . . . . 9 |- ( ( ( ( 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 ) )
158103sseq1d 3632 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
159158rexbidva 3049 . . . . . . . . . 10 |- ( ( ( 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 ) )
160159adantr 481 . . . . . . . . 9 |- ( ( ( ( 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 ) )
161157, 160sylibrd 249 . . . . . . . 8 |- ( ( ( ( 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 ) )
162161ralrimiva 2966 . . . . . . 7 |- ( ( ( 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 ) )
163 nnex 11026 . . . . . . . . 9 |- NN e. _V
164163mptex 6486 . . . . . . . 8 |- ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) e. _V
165 feq1 6026 . . . . . . . . 9 |- ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( f : NN --> J <-> ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) : NN --> J ) )
166 fveq1 6190 . . . . . . . . . . . 12 |- ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( f ` k ) = ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) )
167166eleq2d 2687 . . . . . . . . . . 11 |- ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( A e. ( f ` k ) <-> A e. ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) ) )
168 fveq1 6190 . . . . . . . . . . . 12 |- ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( f ` ( k + 1 ) ) = ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` ( k + 1 ) ) )
169168, 166sseq12d 3634 . . . . . . . . . . 11 |- ( 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 ) ) )
170167, 169anbi12d 747 . . . . . . . . . 10 |- ( 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 ) ) ) )
171170ralbidv 2986 . . . . . . . . 9 |- ( 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 ) ) ) )
172166sseq1d 3632 . . . . . . . . . . . 12 |- ( f = ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) -> ( ( f ` k ) C_ y <-> ( ( n e. NN |-> |^| ( g " ( 1 ... n ) ) ) ` k ) C_ y ) )
173172rexbidv 3052 . . . . . . . . . . 11 |- ( 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 ) )
174173imbi2d 330 . . . . . . . . . 10 |- ( 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 ) ) )
175174ralbidv 2986 . . . . . . . . 9 |- ( 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 ) ) )
176165, 171, 1753anbi123d 1399 . . . . . . . 8 |- ( 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 ) ) ) )
177164, 176spcev 3300 . . . . . . 7 |- ( ( ( 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 ) ) )
17880, 122, 162, 177syl3anc 1326 . . . . . 6 |- ( ( ( 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 ) ) )
179178expr 643 . . . . 5 |- ( ( ( 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 ) ) ) )
180179adantrrl 760 . . . 4 |- ( ( ( 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 ) ) ) )
181180exlimdv 1861 . . 3 |- ( ( ( 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 ) ) ) )
18239, 181mpd 15 . 2 |- ( ( ( 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 ) ) )
1832, 182rexlimddv 3035 1 |- ( ( 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 ) ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U.cuni 4436   |^|cint 4475   class class class wbr 4653   |-> cmpt 4729   dom cdm 5114   ran crn 5115   |` cres 5116   "cima 5117   Fun wfun 5882   Fn wfn 5883   -->wf 5884   -onto->wfo 5886   ` cfv 5888  (class class class)co 6650   omcom 7065   ~~ cen 7952   ~<_ cdom 7953   ~< csdm 7954   Fincfn 7955   1c1 9937   + caddc 9939   NNcn 11020   ...cfz 12326   Topctop 20698   1stcc1stc 21240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-top 20699  df-1stc 21242
This theorem is referenced by:  1stcelcls  21264
  Copyright terms: Public domain W3C validator