Metamath Proof Explorer

Theorem neibastop2lem

Description: Lemma for neibastop2 . (Contributed by Jeff Hankins, 12-Sep-2009)

Ref Expression
Hypotheses neibastop1.1 
|- ( ph -> X e. V )
neibastop1.2 
|- ( ph -> F : X --> ( ~P ~P X \ { (/) } ) )
neibastop1.3 
|- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )
neibastop1.4 
|- J = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) }
neibastop1.5 
|- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> x e. v )
neibastop1.6 
|- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )
neibastop2.p 
|- ( ph -> P e. X )
neibastop2.n 
|- ( ph -> N C_ X )
neibastop2.f 
|- ( ph -> U e. ( F ` P ) )
neibastop2.u 
|- ( ph -> U C_ N )
neibastop2.g 
|- G = ( rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { U } ) |` _om )
neibastop2.s 
|- S = { y e. X | E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) }
Assertion neibastop2lem 
|- ( ph -> E. u e. J ( P e. u /\ u C_ N ) )

Proof

Step Hyp Ref Expression
1 neibastop1.1 
 |-  ( ph -> X e. V )
2 neibastop1.2 
 |-  ( ph -> F : X --> ( ~P ~P X \ { (/) } ) )
3 neibastop1.3 
 |-  ( ( ph /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )
4 neibastop1.4 
 |-  J = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) }
5 neibastop1.5 
 |-  ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> x e. v )
6 neibastop1.6 
 |-  ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )
7 neibastop2.p 
 |-  ( ph -> P e. X )
8 neibastop2.n 
 |-  ( ph -> N C_ X )
9 neibastop2.f 
 |-  ( ph -> U e. ( F ` P ) )
10 neibastop2.u 
 |-  ( ph -> U C_ N )
11 neibastop2.g 
 |-  G = ( rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { U } ) |` _om )
12 neibastop2.s 
 |-  S = { y e. X | E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) }
13 ssrab2 
 |-  { y e. X | E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) } C_ X
14 12 13 eqsstri 
 |-  S C_ X
15 elpw2g 
 |-  ( X e. V -> ( S e. ~P X <-> S C_ X ) )
16 1 15 syl 
 |-  ( ph -> ( S e. ~P X <-> S C_ X ) )
17 14 16 mpbiri 
 |-  ( ph -> S e. ~P X )
18 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
19 18 ineq1d 
 |-  ( y = x -> ( ( F ` y ) i^i ~P f ) = ( ( F ` x ) i^i ~P f ) )
20 19 neeq1d 
 |-  ( y = x -> ( ( ( F ` y ) i^i ~P f ) =/= (/) <-> ( ( F ` x ) i^i ~P f ) =/= (/) ) )
21 20 rexbidv 
 |-  ( y = x -> ( E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) <-> E. f e. U. ran G ( ( F ` x ) i^i ~P f ) =/= (/) ) )
22 21 12 elrab2 
 |-  ( x e. S <-> ( x e. X /\ E. f e. U. ran G ( ( F ` x ) i^i ~P f ) =/= (/) ) )
23 frfnom 
 |-  ( rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { U } ) |` _om ) Fn _om
24 11 fneq1i 
 |-  ( G Fn _om <-> ( rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { U } ) |` _om ) Fn _om )
25 23 24 mpbir 
 |-  G Fn _om
26 fnunirn 
 |-  ( G Fn _om -> ( f e. U. ran G <-> E. k e. _om f e. ( G ` k ) ) )
27 25 26 ax-mp 
 |-  ( f e. U. ran G <-> E. k e. _om f e. ( G ` k ) )
28 n0 
 |-  ( ( ( F ` x ) i^i ~P f ) =/= (/) <-> E. v v e. ( ( F ` x ) i^i ~P f ) )
29 inss1 
 |-  ( ( F ` x ) i^i ~P f ) C_ ( F ` x )
30 29 sseli 
 |-  ( v e. ( ( F ` x ) i^i ~P f ) -> v e. ( F ` x ) )
31 6 anassrs 
 |-  ( ( ( ph /\ x e. X ) /\ v e. ( F ` x ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )
32 30 31 sylan2 
 |-  ( ( ( ph /\ x e. X ) /\ v e. ( ( F ` x ) i^i ~P f ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )
33 32 adantrl 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )
34 simprl 
 |-  ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ ( t e. ( F ` x ) /\ A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) ) ) -> t e. ( F ` x ) )
35 fvssunirn 
 |-  ( F ` x ) C_ U. ran F
36 2 frnd 
 |-  ( ph -> ran F C_ ( ~P ~P X \ { (/) } ) )
37 36 difss2d 
 |-  ( ph -> ran F C_ ~P ~P X )
38 sspwuni 
 |-  ( ran F C_ ~P ~P X <-> U. ran F C_ ~P X )
39 37 38 sylib 
 |-  ( ph -> U. ran F C_ ~P X )
40 39 ad2antrr 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> U. ran F C_ ~P X )
41 35 40 sstrid 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> ( F ` x ) C_ ~P X )
42 41 sselda 
 |-  ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ t e. ( F ` x ) ) -> t e. ~P X )
43 42 elpwid 
 |-  ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ t e. ( F ` x ) ) -> t C_ X )
44 43 sselda 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ t e. ( F ` x ) ) /\ y e. t ) -> y e. X )
45 44 adantrr 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ t e. ( F ` x ) ) /\ ( y e. t /\ ( ( F ` y ) i^i ~P v ) =/= (/) ) ) -> y e. X )
46 simprlr 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> f e. ( G ` k ) )
47 rspe 
 |-  ( ( x e. X /\ v e. ( ( F ` x ) i^i ~P f ) ) -> E. x e. X v e. ( ( F ` x ) i^i ~P f ) )
48 47 ad2ant2l 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> E. x e. X v e. ( ( F ` x ) i^i ~P f ) )
49 eliun 
 |-  ( v e. U_ x e. X ( ( F ` x ) i^i ~P z ) <-> E. x e. X v e. ( ( F ` x ) i^i ~P z ) )
50 pweq 
 |-  ( z = f -> ~P z = ~P f )
51 50 ineq2d 
 |-  ( z = f -> ( ( F ` x ) i^i ~P z ) = ( ( F ` x ) i^i ~P f ) )
52 51 eleq2d 
 |-  ( z = f -> ( v e. ( ( F ` x ) i^i ~P z ) <-> v e. ( ( F ` x ) i^i ~P f ) ) )
53 52 rexbidv 
 |-  ( z = f -> ( E. x e. X v e. ( ( F ` x ) i^i ~P z ) <-> E. x e. X v e. ( ( F ` x ) i^i ~P f ) ) )
54 49 53 syl5bb 
 |-  ( z = f -> ( v e. U_ x e. X ( ( F ` x ) i^i ~P z ) <-> E. x e. X v e. ( ( F ` x ) i^i ~P f ) ) )
55 54 rspcev 
 |-  ( ( f e. ( G ` k ) /\ E. x e. X v e. ( ( F ` x ) i^i ~P f ) ) -> E. z e. ( G ` k ) v e. U_ x e. X ( ( F ` x ) i^i ~P z ) )
56 46 48 55 syl2anc 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> E. z e. ( G ` k ) v e. U_ x e. X ( ( F ` x ) i^i ~P z ) )
57 eliun 
 |-  ( v e. U_ z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) <-> E. z e. ( G ` k ) v e. U_ x e. X ( ( F ` x ) i^i ~P z ) )
58 56 57 sylibr 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> v e. U_ z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) )
59 simpll 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> ph )
60 simprll 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> k e. _om )
61 fvssunirn 
 |-  ( G ` k ) C_ U. ran G
62 fveq2 
 |-  ( n = (/) -> ( G ` n ) = ( G ` (/) ) )
63 11 fveq1i 
 |-  ( G ` (/) ) = ( ( rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { U } ) |` _om ) ` (/) )
64 snex 
 |-  { U } e. _V
65 fr0g 
 |-  ( { U } e. _V -> ( ( rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { U } ) |` _om ) ` (/) ) = { U } )
66 64 65 ax-mp 
 |-  ( ( rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { U } ) |` _om ) ` (/) ) = { U }
67 63 66 eqtri 
 |-  ( G ` (/) ) = { U }
68 62 67 eqtrdi 
 |-  ( n = (/) -> ( G ` n ) = { U } )
69 68 sseq1d 
 |-  ( n = (/) -> ( ( G ` n ) C_ ~P U <-> { U } C_ ~P U ) )
70 fveq2 
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
71 70 sseq1d 
 |-  ( n = k -> ( ( G ` n ) C_ ~P U <-> ( G ` k ) C_ ~P U ) )
72 fveq2 
 |-  ( n = suc k -> ( G ` n ) = ( G ` suc k ) )
73 72 sseq1d 
 |-  ( n = suc k -> ( ( G ` n ) C_ ~P U <-> ( G ` suc k ) C_ ~P U ) )
74 pwidg 
 |-  ( U e. ( F ` P ) -> U e. ~P U )
75 9 74 syl 
 |-  ( ph -> U e. ~P U )
76 75 snssd 
 |-  ( ph -> { U } C_ ~P U )
77 simprl 
 |-  ( ( ph /\ ( k e. _om /\ ( G ` k ) C_ ~P U ) ) -> k e. _om )
78 9 adantr 
 |-  ( ( ph /\ ( k e. _om /\ ( G ` k ) C_ ~P U ) ) -> U e. ( F ` P ) )
79 78 pwexd 
 |-  ( ( ph /\ ( k e. _om /\ ( G ` k ) C_ ~P U ) ) -> ~P U e. _V )
80 inss2 
 |-  ( ( F ` x ) i^i ~P z ) C_ ~P z
81 elpwi 
 |-  ( z e. ~P U -> z C_ U )
82 81 adantl 
 |-  ( ( ph /\ z e. ~P U ) -> z C_ U )
83 82 sspwd 
 |-  ( ( ph /\ z e. ~P U ) -> ~P z C_ ~P U )
84 80 83 sstrid 
 |-  ( ( ph /\ z e. ~P U ) -> ( ( F ` x ) i^i ~P z ) C_ ~P U )
85 84 ralrimivw 
 |-  ( ( ph /\ z e. ~P U ) -> A. x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U )
86 iunss 
 |-  ( U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U <-> A. x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U )
87 85 86 sylibr 
 |-  ( ( ph /\ z e. ~P U ) -> U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U )
88 87 ralrimiva 
 |-  ( ph -> A. z e. ~P U U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U )
89 ssralv 
 |-  ( ( G ` k ) C_ ~P U -> ( A. z e. ~P U U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U -> A. z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U ) )
90 89 adantl 
 |-  ( ( k e. _om /\ ( G ` k ) C_ ~P U ) -> ( A. z e. ~P U U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U -> A. z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U ) )
91 88 90 mpan9 
 |-  ( ( ph /\ ( k e. _om /\ ( G ` k ) C_ ~P U ) ) -> A. z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U )
92 iunss 
 |-  ( U_ z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U <-> A. z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U )
93 91 92 sylibr 
 |-  ( ( ph /\ ( k e. _om /\ ( G ` k ) C_ ~P U ) ) -> U_ z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) C_ ~P U )
94 79 93 ssexd 
 |-  ( ( ph /\ ( k e. _om /\ ( G ` k ) C_ ~P U ) ) -> U_ z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) e. _V )
95 iuneq1 
 |-  ( y = a -> U_ z e. y U_ x e. X ( ( F ` x ) i^i ~P z ) = U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) )
96 iuneq1 
 |-  ( y = ( G ` k ) -> U_ z e. y U_ x e. X ( ( F ` x ) i^i ~P z ) = U_ z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) )
97 11 95 96 frsucmpt2 
 |-  ( ( k e. _om /\ U_ z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) e. _V ) -> ( G ` suc k ) = U_ z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) )
98 77 94 97 syl2anc 
 |-  ( ( ph /\ ( k e. _om /\ ( G ` k ) C_ ~P U ) ) -> ( G ` suc k ) = U_ z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) )
99 98 93 eqsstrd 
 |-  ( ( ph /\ ( k e. _om /\ ( G ` k ) C_ ~P U ) ) -> ( G ` suc k ) C_ ~P U )
100 99 expr 
 |-  ( ( ph /\ k e. _om ) -> ( ( G ` k ) C_ ~P U -> ( G ` suc k ) C_ ~P U ) )
101 100 expcom 
 |-  ( k e. _om -> ( ph -> ( ( G ` k ) C_ ~P U -> ( G ` suc k ) C_ ~P U ) ) )
102 69 71 73 76 101 finds2 
 |-  ( n e. _om -> ( ph -> ( G ` n ) C_ ~P U ) )
103 fvex 
 |-  ( G ` n ) e. _V
104 103 elpw 
 |-  ( ( G ` n ) e. ~P ~P U <-> ( G ` n ) C_ ~P U )
105 102 104 syl6ibr 
 |-  ( n e. _om -> ( ph -> ( G ` n ) e. ~P ~P U ) )
106 105 com12 
 |-  ( ph -> ( n e. _om -> ( G ` n ) e. ~P ~P U ) )
107 106 ralrimiv 
 |-  ( ph -> A. n e. _om ( G ` n ) e. ~P ~P U )
108 ffnfv 
 |-  ( G : _om --> ~P ~P U <-> ( G Fn _om /\ A. n e. _om ( G ` n ) e. ~P ~P U ) )
109 25 108 mpbiran 
 |-  ( G : _om --> ~P ~P U <-> A. n e. _om ( G ` n ) e. ~P ~P U )
110 107 109 sylibr 
 |-  ( ph -> G : _om --> ~P ~P U )
111 110 frnd 
 |-  ( ph -> ran G C_ ~P ~P U )
112 sspwuni 
 |-  ( ran G C_ ~P ~P U <-> U. ran G C_ ~P U )
113 111 112 sylib 
 |-  ( ph -> U. ran G C_ ~P U )
114 113 ad2antrr 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> U. ran G C_ ~P U )
115 61 114 sstrid 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> ( G ` k ) C_ ~P U )
116 59 60 115 98 syl12anc 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> ( G ` suc k ) = U_ z e. ( G ` k ) U_ x e. X ( ( F ` x ) i^i ~P z ) )
117 58 116 eleqtrrd 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> v e. ( G ` suc k ) )
118 peano2 
 |-  ( k e. _om -> suc k e. _om )
119 60 118 syl 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> suc k e. _om )
120 fnfvelrn 
 |-  ( ( G Fn _om /\ suc k e. _om ) -> ( G ` suc k ) e. ran G )
121 25 119 120 sylancr 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> ( G ` suc k ) e. ran G )
122 elunii 
 |-  ( ( v e. ( G ` suc k ) /\ ( G ` suc k ) e. ran G ) -> v e. U. ran G )
123 117 121 122 syl2anc 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> v e. U. ran G )
124 123 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ t e. ( F ` x ) ) /\ ( y e. t /\ ( ( F ` y ) i^i ~P v ) =/= (/) ) ) -> v e. U. ran G )
125 simprr 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ t e. ( F ` x ) ) /\ ( y e. t /\ ( ( F ` y ) i^i ~P v ) =/= (/) ) ) -> ( ( F ` y ) i^i ~P v ) =/= (/) )
126 pweq 
 |-  ( f = v -> ~P f = ~P v )
127 126 ineq2d 
 |-  ( f = v -> ( ( F ` y ) i^i ~P f ) = ( ( F ` y ) i^i ~P v ) )
128 127 neeq1d 
 |-  ( f = v -> ( ( ( F ` y ) i^i ~P f ) =/= (/) <-> ( ( F ` y ) i^i ~P v ) =/= (/) ) )
129 128 rspcev 
 |-  ( ( v e. U. ran G /\ ( ( F ` y ) i^i ~P v ) =/= (/) ) -> E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) )
130 124 125 129 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ t e. ( F ` x ) ) /\ ( y e. t /\ ( ( F ` y ) i^i ~P v ) =/= (/) ) ) -> E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) )
131 12 rabeq2i 
 |-  ( y e. S <-> ( y e. X /\ E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) ) )
132 45 130 131 sylanbrc 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ t e. ( F ` x ) ) /\ ( y e. t /\ ( ( F ` y ) i^i ~P v ) =/= (/) ) ) -> y e. S )
133 132 expr 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ t e. ( F ` x ) ) /\ y e. t ) -> ( ( ( F ` y ) i^i ~P v ) =/= (/) -> y e. S ) )
134 133 ralimdva 
 |-  ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ t e. ( F ` x ) ) -> ( A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) -> A. y e. t y e. S ) )
135 134 impr 
 |-  ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ ( t e. ( F ` x ) /\ A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) ) ) -> A. y e. t y e. S )
136 dfss3 
 |-  ( t C_ S <-> A. y e. t y e. S )
137 135 136 sylibr 
 |-  ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ ( t e. ( F ` x ) /\ A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) ) ) -> t C_ S )
138 velpw 
 |-  ( t e. ~P S <-> t C_ S )
139 137 138 sylibr 
 |-  ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ ( t e. ( F ` x ) /\ A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) ) ) -> t e. ~P S )
140 inelcm 
 |-  ( ( t e. ( F ` x ) /\ t e. ~P S ) -> ( ( F ` x ) i^i ~P S ) =/= (/) )
141 34 139 140 syl2anc 
 |-  ( ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) /\ ( t e. ( F ` x ) /\ A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) ) ) -> ( ( F ` x ) i^i ~P S ) =/= (/) )
142 33 141 rexlimddv 
 |-  ( ( ( ph /\ x e. X ) /\ ( ( k e. _om /\ f e. ( G ` k ) ) /\ v e. ( ( F ` x ) i^i ~P f ) ) ) -> ( ( F ` x ) i^i ~P S ) =/= (/) )
143 142 expr 
 |-  ( ( ( ph /\ x e. X ) /\ ( k e. _om /\ f e. ( G ` k ) ) ) -> ( v e. ( ( F ` x ) i^i ~P f ) -> ( ( F ` x ) i^i ~P S ) =/= (/) ) )
144 143 exlimdv 
 |-  ( ( ( ph /\ x e. X ) /\ ( k e. _om /\ f e. ( G ` k ) ) ) -> ( E. v v e. ( ( F ` x ) i^i ~P f ) -> ( ( F ` x ) i^i ~P S ) =/= (/) ) )
145 28 144 syl5bi 
 |-  ( ( ( ph /\ x e. X ) /\ ( k e. _om /\ f e. ( G ` k ) ) ) -> ( ( ( F ` x ) i^i ~P f ) =/= (/) -> ( ( F ` x ) i^i ~P S ) =/= (/) ) )
146 145 rexlimdvaa 
 |-  ( ( ph /\ x e. X ) -> ( E. k e. _om f e. ( G ` k ) -> ( ( ( F ` x ) i^i ~P f ) =/= (/) -> ( ( F ` x ) i^i ~P S ) =/= (/) ) ) )
147 27 146 syl5bi 
 |-  ( ( ph /\ x e. X ) -> ( f e. U. ran G -> ( ( ( F ` x ) i^i ~P f ) =/= (/) -> ( ( F ` x ) i^i ~P S ) =/= (/) ) ) )
148 147 rexlimdv 
 |-  ( ( ph /\ x e. X ) -> ( E. f e. U. ran G ( ( F ` x ) i^i ~P f ) =/= (/) -> ( ( F ` x ) i^i ~P S ) =/= (/) ) )
149 148 expimpd 
 |-  ( ph -> ( ( x e. X /\ E. f e. U. ran G ( ( F ` x ) i^i ~P f ) =/= (/) ) -> ( ( F ` x ) i^i ~P S ) =/= (/) ) )
150 22 149 syl5bi 
 |-  ( ph -> ( x e. S -> ( ( F ` x ) i^i ~P S ) =/= (/) ) )
151 150 ralrimiv 
 |-  ( ph -> A. x e. S ( ( F ` x ) i^i ~P S ) =/= (/) )
152 pweq 
 |-  ( o = S -> ~P o = ~P S )
153 152 ineq2d 
 |-  ( o = S -> ( ( F ` x ) i^i ~P o ) = ( ( F ` x ) i^i ~P S ) )
154 153 neeq1d 
 |-  ( o = S -> ( ( ( F ` x ) i^i ~P o ) =/= (/) <-> ( ( F ` x ) i^i ~P S ) =/= (/) ) )
155 154 raleqbi1dv 
 |-  ( o = S -> ( A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) <-> A. x e. S ( ( F ` x ) i^i ~P S ) =/= (/) ) )
156 155 4 elrab2 
 |-  ( S e. J <-> ( S e. ~P X /\ A. x e. S ( ( F ` x ) i^i ~P S ) =/= (/) ) )
157 17 151 156 sylanbrc 
 |-  ( ph -> S e. J )
158 snidg 
 |-  ( U e. ( F ` P ) -> U e. { U } )
159 9 158 syl 
 |-  ( ph -> U e. { U } )
160 peano1 
 |-  (/) e. _om
161 fnfvelrn 
 |-  ( ( G Fn _om /\ (/) e. _om ) -> ( G ` (/) ) e. ran G )
162 25 160 161 mp2an 
 |-  ( G ` (/) ) e. ran G
163 67 162 eqeltrri 
 |-  { U } e. ran G
164 elunii 
 |-  ( ( U e. { U } /\ { U } e. ran G ) -> U e. U. ran G )
165 159 163 164 sylancl 
 |-  ( ph -> U e. U. ran G )
166 inelcm 
 |-  ( ( U e. ( F ` P ) /\ U e. ~P U ) -> ( ( F ` P ) i^i ~P U ) =/= (/) )
167 9 75 166 syl2anc 
 |-  ( ph -> ( ( F ` P ) i^i ~P U ) =/= (/) )
168 pweq 
 |-  ( f = U -> ~P f = ~P U )
169 168 ineq2d 
 |-  ( f = U -> ( ( F ` P ) i^i ~P f ) = ( ( F ` P ) i^i ~P U ) )
170 169 neeq1d 
 |-  ( f = U -> ( ( ( F ` P ) i^i ~P f ) =/= (/) <-> ( ( F ` P ) i^i ~P U ) =/= (/) ) )
171 170 rspcev 
 |-  ( ( U e. U. ran G /\ ( ( F ` P ) i^i ~P U ) =/= (/) ) -> E. f e. U. ran G ( ( F ` P ) i^i ~P f ) =/= (/) )
172 165 167 171 syl2anc 
 |-  ( ph -> E. f e. U. ran G ( ( F ` P ) i^i ~P f ) =/= (/) )
173 fveq2 
 |-  ( y = P -> ( F ` y ) = ( F ` P ) )
174 173 ineq1d 
 |-  ( y = P -> ( ( F ` y ) i^i ~P f ) = ( ( F ` P ) i^i ~P f ) )
175 174 neeq1d 
 |-  ( y = P -> ( ( ( F ` y ) i^i ~P f ) =/= (/) <-> ( ( F ` P ) i^i ~P f ) =/= (/) ) )
176 175 rexbidv 
 |-  ( y = P -> ( E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) <-> E. f e. U. ran G ( ( F ` P ) i^i ~P f ) =/= (/) ) )
177 176 12 elrab2 
 |-  ( P e. S <-> ( P e. X /\ E. f e. U. ran G ( ( F ` P ) i^i ~P f ) =/= (/) ) )
178 7 172 177 sylanbrc 
 |-  ( ph -> P e. S )
179 eluni2 
 |-  ( f e. U. ran G <-> E. z e. ran G f e. z )
180 eleq2 
 |-  ( z = ( G ` k ) -> ( f e. z <-> f e. ( G ` k ) ) )
181 180 rexrn 
 |-  ( G Fn _om -> ( E. z e. ran G f e. z <-> E. k e. _om f e. ( G ` k ) ) )
182 25 181 ax-mp 
 |-  ( E. z e. ran G f e. z <-> E. k e. _om f e. ( G ` k ) )
183 110 adantr 
 |-  ( ( ph /\ y e. X ) -> G : _om --> ~P ~P U )
184 183 ffvelrnda 
 |-  ( ( ( ph /\ y e. X ) /\ k e. _om ) -> ( G ` k ) e. ~P ~P U )
185 184 elpwid 
 |-  ( ( ( ph /\ y e. X ) /\ k e. _om ) -> ( G ` k ) C_ ~P U )
186 185 sselda 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ f e. ( G ` k ) ) -> f e. ~P U )
187 186 adantrr 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( ( F ` y ) i^i ~P f ) =/= (/) ) ) -> f e. ~P U )
188 187 elpwid 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( ( F ` y ) i^i ~P f ) =/= (/) ) ) -> f C_ U )
189 10 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( ( F ` y ) i^i ~P f ) =/= (/) ) ) -> U C_ N )
190 188 189 sstrd 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( ( F ` y ) i^i ~P f ) =/= (/) ) ) -> f C_ N )
191 n0 
 |-  ( ( ( F ` y ) i^i ~P f ) =/= (/) <-> E. v v e. ( ( F ` y ) i^i ~P f ) )
192 elin 
 |-  ( v e. ( ( F ` y ) i^i ~P f ) <-> ( v e. ( F ` y ) /\ v e. ~P f ) )
193 simprrr 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( v e. ( F ` y ) /\ v e. ~P f ) ) ) -> v e. ~P f )
194 193 elpwid 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( v e. ( F ` y ) /\ v e. ~P f ) ) ) -> v C_ f )
195 simpllr 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( v e. ( F ` y ) /\ v e. ~P f ) ) ) -> y e. X )
196 5 expr 
 |-  ( ( ph /\ x e. X ) -> ( v e. ( F ` x ) -> x e. v ) )
197 196 ralrimiva 
 |-  ( ph -> A. x e. X ( v e. ( F ` x ) -> x e. v ) )
198 197 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( v e. ( F ` y ) /\ v e. ~P f ) ) ) -> A. x e. X ( v e. ( F ` x ) -> x e. v ) )
199 simprrl 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( v e. ( F ` y ) /\ v e. ~P f ) ) ) -> v e. ( F ` y ) )
200 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
201 200 eleq2d 
 |-  ( x = y -> ( v e. ( F ` x ) <-> v e. ( F ` y ) ) )
202 elequ1 
 |-  ( x = y -> ( x e. v <-> y e. v ) )
203 201 202 imbi12d 
 |-  ( x = y -> ( ( v e. ( F ` x ) -> x e. v ) <-> ( v e. ( F ` y ) -> y e. v ) ) )
204 203 rspcv 
 |-  ( y e. X -> ( A. x e. X ( v e. ( F ` x ) -> x e. v ) -> ( v e. ( F ` y ) -> y e. v ) ) )
205 195 198 199 204 syl3c 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( v e. ( F ` y ) /\ v e. ~P f ) ) ) -> y e. v )
206 194 205 sseldd 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( v e. ( F ` y ) /\ v e. ~P f ) ) ) -> y e. f )
207 206 expr 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ f e. ( G ` k ) ) -> ( ( v e. ( F ` y ) /\ v e. ~P f ) -> y e. f ) )
208 192 207 syl5bi 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ f e. ( G ` k ) ) -> ( v e. ( ( F ` y ) i^i ~P f ) -> y e. f ) )
209 208 exlimdv 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ f e. ( G ` k ) ) -> ( E. v v e. ( ( F ` y ) i^i ~P f ) -> y e. f ) )
210 191 209 syl5bi 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ f e. ( G ` k ) ) -> ( ( ( F ` y ) i^i ~P f ) =/= (/) -> y e. f ) )
211 210 impr 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( ( F ` y ) i^i ~P f ) =/= (/) ) ) -> y e. f )
212 190 211 sseldd 
 |-  ( ( ( ( ph /\ y e. X ) /\ k e. _om ) /\ ( f e. ( G ` k ) /\ ( ( F ` y ) i^i ~P f ) =/= (/) ) ) -> y e. N )
213 212 exp32 
 |-  ( ( ( ph /\ y e. X ) /\ k e. _om ) -> ( f e. ( G ` k ) -> ( ( ( F ` y ) i^i ~P f ) =/= (/) -> y e. N ) ) )
214 213 rexlimdva 
 |-  ( ( ph /\ y e. X ) -> ( E. k e. _om f e. ( G ` k ) -> ( ( ( F ` y ) i^i ~P f ) =/= (/) -> y e. N ) ) )
215 182 214 syl5bi 
 |-  ( ( ph /\ y e. X ) -> ( E. z e. ran G f e. z -> ( ( ( F ` y ) i^i ~P f ) =/= (/) -> y e. N ) ) )
216 179 215 syl5bi 
 |-  ( ( ph /\ y e. X ) -> ( f e. U. ran G -> ( ( ( F ` y ) i^i ~P f ) =/= (/) -> y e. N ) ) )
217 216 rexlimdv 
 |-  ( ( ph /\ y e. X ) -> ( E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) -> y e. N ) )
218 217 3impia 
 |-  ( ( ph /\ y e. X /\ E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) ) -> y e. N )
219 218 rabssdv 
 |-  ( ph -> { y e. X | E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) } C_ N )
220 12 219 eqsstrid 
 |-  ( ph -> S C_ N )
221 eleq2 
 |-  ( u = S -> ( P e. u <-> P e. S ) )
222 sseq1 
 |-  ( u = S -> ( u C_ N <-> S C_ N ) )
223 221 222 anbi12d 
 |-  ( u = S -> ( ( P e. u /\ u C_ N ) <-> ( P e. S /\ S C_ N ) ) )
224 223 rspcev 
 |-  ( ( S e. J /\ ( P e. S /\ S C_ N ) ) -> E. u e. J ( P e. u /\ u C_ N ) )
225 157 178 220 224 syl12anc 
 |-  ( ph -> E. u e. J ( P e. u /\ u C_ N ) )