MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  marypha1lem Structured version   Unicode version

Theorem marypha1lem 7441
Description: Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.)
Assertion
Ref Expression
marypha1lem  |-  ( A  e.  Fin  ->  (
b  e.  Fin  ->  A. c  e.  ~P  ( A  X.  b ) ( A. d  e.  ~P  A d  ~<_  ( c
" d )  ->  E. e  e.  ~P  c e : A -1-1-> _V ) ) )
Distinct variable group:    A, b, c, d, e

Proof of Theorem marypha1lem
Dummy variables  a 
f  g  h  i  j  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpeq1 4895 . . . . 5  |-  ( a  =  f  ->  (
a  X.  b )  =  ( f  X.  b ) )
21pweqd 3806 . . . 4  |-  ( a  =  f  ->  ~P ( a  X.  b
)  =  ~P (
f  X.  b ) )
3 pweq 3804 . . . . . 6  |-  ( a  =  f  ->  ~P a  =  ~P f
)
43raleqdv 2912 . . . . 5  |-  ( a  =  f  ->  ( A. d  e.  ~P  a d  ~<_  ( c
" d )  <->  A. d  e.  ~P  f d  ~<_  ( c " d ) ) )
5 f1eq2 5638 . . . . . 6  |-  ( a  =  f  ->  (
e : a -1-1-> _V  <->  e : f -1-1-> _V )
)
65rexbidv 2728 . . . . 5  |-  ( a  =  f  ->  ( E. e  e.  ~P  c e : a
-1-1-> _V  <->  E. e  e.  ~P  c e : f
-1-1-> _V ) )
74, 6imbi12d 313 . . . 4  |-  ( a  =  f  ->  (
( A. d  e. 
~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V )  <->  ( A. d  e.  ~P  f
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : f -1-1-> _V ) ) )
82, 7raleqbidv 2918 . . 3  |-  ( a  =  f  ->  ( A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V )  <->  A. c  e.  ~P  ( f  X.  b ) ( A. d  e.  ~P  f
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : f -1-1-> _V ) ) )
98imbi2d 309 . 2  |-  ( a  =  f  ->  (
( b  e.  Fin  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) )  <->  ( b  e.  Fin  ->  A. c  e.  ~P  ( f  X.  b ) ( A. d  e.  ~P  f
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : f -1-1-> _V ) ) ) )
10 xpeq1 4895 . . . . 5  |-  ( a  =  A  ->  (
a  X.  b )  =  ( A  X.  b ) )
1110pweqd 3806 . . . 4  |-  ( a  =  A  ->  ~P ( a  X.  b
)  =  ~P ( A  X.  b ) )
12 pweq 3804 . . . . . 6  |-  ( a  =  A  ->  ~P a  =  ~P A
)
1312raleqdv 2912 . . . . 5  |-  ( a  =  A  ->  ( A. d  e.  ~P  a d  ~<_  ( c
" d )  <->  A. d  e.  ~P  A d  ~<_  ( c " d ) ) )
14 f1eq2 5638 . . . . . 6  |-  ( a  =  A  ->  (
e : a -1-1-> _V  <->  e : A -1-1-> _V )
)
1514rexbidv 2728 . . . . 5  |-  ( a  =  A  ->  ( E. e  e.  ~P  c e : a
-1-1-> _V  <->  E. e  e.  ~P  c e : A -1-1-> _V ) )
1613, 15imbi12d 313 . . . 4  |-  ( a  =  A  ->  (
( A. d  e. 
~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V )  <->  ( A. d  e.  ~P  A
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : A -1-1-> _V ) ) )
1711, 16raleqbidv 2918 . . 3  |-  ( a  =  A  ->  ( A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V )  <->  A. c  e.  ~P  ( A  X.  b ) ( A. d  e.  ~P  A
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : A -1-1-> _V ) ) )
1817imbi2d 309 . 2  |-  ( a  =  A  ->  (
( b  e.  Fin  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) )  <->  ( b  e.  Fin  ->  A. c  e.  ~P  ( A  X.  b ) ( A. d  e.  ~P  A
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : A -1-1-> _V ) ) ) )
19 bi2.04 352 . . . . 5  |-  ( ( a  C.  f  -> 
( b  e.  Fin  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  <-> 
( b  e.  Fin  ->  ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) ) )
2019albii 1576 . . . 4  |-  ( A. a ( a  C.  f  ->  ( b  e. 
Fin  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  <->  A. a ( b  e. 
Fin  ->  ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) ) )
21 19.21v 1914 . . . 4  |-  ( A. a ( b  e. 
Fin  ->  ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  <-> 
( b  e.  Fin  ->  A. a ( a 
C.  f  ->  A. c  e.  ~P  ( a  X.  b ) ( A. d  e.  ~P  a
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : a -1-1-> _V ) ) ) )
2220, 21bitri 242 . . 3  |-  ( A. a ( a  C.  f  ->  ( b  e. 
Fin  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  <-> 
( b  e.  Fin  ->  A. a ( a 
C.  f  ->  A. c  e.  ~P  ( a  X.  b ) ( A. d  e.  ~P  a
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : a -1-1-> _V ) ) ) )
23 0elpw 4372 . . . . . . . . . . . . 13  |-  (/)  e.  ~P g
24 f10 5712 . . . . . . . . . . . . 13  |-  (/) : (/) -1-1-> _V
25 f1eq1 5637 . . . . . . . . . . . . . 14  |-  ( e  =  (/)  ->  ( e : (/) -1-1-> _V  <->  (/) : (/) -1-1-> _V )
)
2625rspcev 3054 . . . . . . . . . . . . 13  |-  ( (
(/)  e.  ~P g  /\  (/) : (/) -1-1-> _V )  ->  E. e  e.  ~P  g e : (/) -1-1-> _V )
2723, 24, 26mp2an 655 . . . . . . . . . . . 12  |-  E. e  e.  ~P  g e :
(/) -1-1-> _V
28 f1eq2 5638 . . . . . . . . . . . . 13  |-  ( f  =  (/)  ->  ( e : f -1-1-> _V  <->  e : (/) -1-1->
_V ) )
2928rexbidv 2728 . . . . . . . . . . . 12  |-  ( f  =  (/)  ->  ( E. e  e.  ~P  g
e : f -1-1-> _V  <->  E. e  e.  ~P  g
e : (/) -1-1-> _V )
)
3027, 29mpbiri 226 . . . . . . . . . . 11  |-  ( f  =  (/)  ->  E. e  e.  ~P  g e : f -1-1-> _V )
3130a1i 11 . . . . . . . . . 10  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) ) )  ->  ( f  =  (/)  ->  E. e  e.  ~P  g e : f
-1-1-> _V ) )
32 n0 3639 . . . . . . . . . . 11  |-  ( f  =/=  (/)  <->  E. i  i  e.  f )
33 snelpwi 4412 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  f  ->  { i }  e.  ~P f
)
34 id 21 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  =  { i }  ->  d  =  {
i } )
35 imaeq2 5202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  =  { i }  ->  ( g "
d )  =  ( g " { i } ) )
3634, 35breq12d 4228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d  =  { i }  ->  ( d  ~<_  ( g " d )  <->  { i }  ~<_  ( g
" { i } ) ) )
3736rspcva 3052 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( { i }  e.  ~P f  /\  A. d  e.  ~P  f d  ~<_  ( g " d ) )  ->  { i }  ~<_  ( g " { i } ) )
38 vex 2961 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  i  e. 
_V
3938snnz 3924 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { i }  =/=  (/)
40 snex 4408 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { i }  e.  _V
41400sdom 7241 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (/)  ~<  { i }  <->  { i }  =/=  (/) )
4239, 41mpbir 202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (/)  ~<  { i }
43 sdomdomtr 7243 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
(/)  ~<  { i }  /\  { i }  ~<_  ( g " {
i } ) )  ->  (/)  ~<  ( g " { i } ) )
4442, 43mpan 653 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { i }  ~<_  ( g
" { i } )  ->  (/)  ~<  (
g " { i } ) )
45 vex 2961 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  g  e. 
_V
46 imaexg 5220 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  e.  _V  ->  (
g " { i } )  e.  _V )
4745, 46ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g
" { i } )  e.  _V
48470sdom 7241 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (/)  ~< 
( g " {
i } )  <->  ( g " { i } )  =/=  (/) )
4944, 48sylib 190 . . . . . . . . . . . . . . . . . . . . 21  |-  ( { i }  ~<_  ( g
" { i } )  ->  ( g " { i } )  =/=  (/) )
5037, 49syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { i }  e.  ~P f  /\  A. d  e.  ~P  f d  ~<_  ( g " d ) )  ->  ( g " { i } )  =/=  (/) )
5150expcom 426 . . . . . . . . . . . . . . . . . . 19  |-  ( A. d  e.  ~P  f
d  ~<_  ( g "
d )  ->  ( { i }  e.  ~P f  ->  ( g
" { i } )  =/=  (/) ) )
5233, 51syl5 31 . . . . . . . . . . . . . . . . . 18  |-  ( A. d  e.  ~P  f
d  ~<_  ( g "
d )  ->  (
i  e.  f  -> 
( g " {
i } )  =/=  (/) ) )
5352adantl 454 . . . . . . . . . . . . . . . . 17  |-  ( ( g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) )  ->  ( i  e.  f  ->  ( g
" { i } )  =/=  (/) ) )
5453ad2antlr 709 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) ) )  ->  ( i  e.  f  ->  ( g " { i } )  =/=  (/) ) )
5554impr 604 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )
)  ->  ( g " { i } )  =/=  (/) )
56 n0 3639 . . . . . . . . . . . . . . 15  |-  ( ( g " { i } )  =/=  (/)  <->  E. j 
j  e.  ( g
" { i } ) )
5755, 56sylib 190 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )
)  ->  E. j 
j  e.  ( g
" { i } ) )
58 imaexg 5220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( g  e.  _V  ->  (
g " c )  e.  _V )
59 difexg 4354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( g " c )  e.  _V  ->  (
( g " c
)  \  { j } )  e.  _V )
6045, 58, 59mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( g " c ) 
\  { j } )  e.  _V
61600dom 7240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (/)  ~<_  ( ( g " c ) 
\  { j } )
62 breq1 4218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  (/)  ->  ( c  ~<_  ( ( g "
c )  \  {
j } )  <->  (/)  ~<_  ( ( g " c ) 
\  { j } ) ) )
6361, 62mpbiri 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  (/)  ->  c  ~<_  ( ( g " c
)  \  { j } ) )
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  c  e.  ~P ( f  \  {
i } ) )  ->  ( c  =  (/)  ->  c  ~<_  ( ( g " c ) 
\  { j } ) ) )
65 simpll 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  ->  A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) ) )
66 elpwi 3809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  e.  ~P ( f 
\  { i } )  ->  c  C_  ( f  \  {
i } ) )
6766ad2antrl 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
c  C_  ( f  \  { i } ) )
68 difsnpss 3943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( i  e.  f  <->  ( f  \  { i } ) 
C.  f )
6968biimpi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( i  e.  f  ->  (
f  \  { i } )  C.  f
)
7069ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
( f  \  {
i } )  C.  f )
7167, 70sspsstrd 3457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
c  C.  f )
72 simprr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
c  =/=  (/) )
7371, 72jca 520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
( c  C.  f  /\  c  =/=  (/) ) )
74 psseq1 3436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  c  ->  (
h  C.  f  <->  c  C.  f ) )
75 neeq1 2611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  c  ->  (
h  =/=  (/)  <->  c  =/=  (/) ) )
7674, 75anbi12d 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  =  c  ->  (
( h  C.  f  /\  h  =/=  (/) )  <->  ( c  C.  f  /\  c  =/=  (/) ) ) )
77 id 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  c  ->  h  =  c )
78 imaeq2 5202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  c  ->  (
g " h )  =  ( g "
c ) )
7977, 78breq12d 4228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  =  c  ->  (
h  ~<  ( g "
h )  <->  c  ~<  ( g " c ) ) )
8076, 79imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( h  =  c  ->  (
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  <->  ( (
c  C.  f  /\  c  =/=  (/) )  ->  c  ~<  ( g " c
) ) ) )
8180spv 1966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) )  ->  (
( c  C.  f  /\  c  =/=  (/) )  -> 
c  ~<  ( g "
c ) ) )
8265, 73, 81sylc 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
c  ~<  ( g "
c ) )
83 domdifsn 7194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c 
~<  ( g " c
)  ->  c  ~<_  ( ( g " c ) 
\  { j } ) )
8482, 83syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
c  ~<_  ( ( g
" c )  \  { j } ) )
8584expr 600 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  c  e.  ~P ( f  \  {
i } ) )  ->  ( c  =/=  (/)  ->  c  ~<_  ( ( g " c ) 
\  { j } ) ) )
8664, 85pm2.61dne 2683 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  c  e.  ~P ( f  \  {
i } ) )  ->  c  ~<_  ( ( g " c ) 
\  { j } ) )
8786adantlrr 703 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  ( i  e.  f  /\  j  e.  ( g " { i } ) ) )  /\  c  e.  ~P ( f  \  {
i } ) )  ->  c  ~<_  ( ( g " c ) 
\  { j } ) )
8887adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  ( A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) )  /\  (
i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  /\  c  e.  ~P (
f  \  { i } ) )  -> 
c  ~<_  ( ( g
" c )  \  { j } ) )
89 df-ss 3336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c 
C_  ( f  \  { i } )  <-> 
( c  i^i  (
f  \  { i } ) )  =  c )
9066, 89sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  ~P ( f 
\  { i } )  ->  ( c  i^i  ( f  \  {
i } ) )  =  c )
9190imaeq2d 5206 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  ~P ( f 
\  { i } )  ->  ( g " ( c  i^i  ( f  \  {
i } ) ) )  =  ( g
" c ) )
9291ineq1d 3543 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  e.  ~P ( f 
\  { i } )  ->  ( (
g " ( c  i^i  ( f  \  { i } ) ) )  i^i  (
b  \  { j } ) )  =  ( ( g "
c )  i^i  (
b  \  { j } ) ) )
9392adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  ( A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) )  /\  (
i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  /\  c  e.  ~P (
f  \  { i } ) )  -> 
( ( g "
( c  i^i  (
f  \  { i } ) ) )  i^i  ( b  \  { j } ) )  =  ( ( g " c )  i^i  ( b  \  { j } ) ) )
94 indif2 3586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( g " c )  i^i  ( b  \  { j } ) )  =  ( ( ( g " c
)  i^i  b )  \  { j } )
95 imassrn 5219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( g
" c )  C_  ran  g
96 elpwi 3809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( g  e.  ~P ( f  X.  b )  -> 
g  C_  ( f  X.  b ) )
97 rnss 5101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( g 
C_  ( f  X.  b )  ->  ran  g  C_  ran  ( f  X.  b ) )
98 rnxpss 5304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ran  (
f  X.  b ) 
C_  b
9997, 98syl6ss 3362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( g 
C_  ( f  X.  b )  ->  ran  g  C_  b )
10096, 99syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( g  e.  ~P ( f  X.  b )  ->  ran  g  C_  b )
10195, 100syl5ss 3361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( g  e.  ~P ( f  X.  b )  -> 
( g " c
)  C_  b )
102 df-ss 3336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( g " c ) 
C_  b  <->  ( (
g " c )  i^i  b )  =  ( g " c
) )
103101, 102sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( g  e.  ~P ( f  X.  b )  -> 
( ( g "
c )  i^i  b
)  =  ( g
" c ) )
104103difeq1d 3466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( g  e.  ~P ( f  X.  b )  -> 
( ( ( g
" c )  i^i  b )  \  {
j } )  =  ( ( g "
c )  \  {
j } ) )
105104ad2antrl 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  ( g  e.  ~P ( f  X.  b
)  /\  A. d  e.  ~P  f d  ~<_  ( g " d ) ) )  ->  (
( ( g "
c )  i^i  b
)  \  { j } )  =  ( ( g " c
)  \  { j } ) )
10694, 105syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  ( g  e.  ~P ( f  X.  b
)  /\  A. d  e.  ~P  f d  ~<_  ( g " d ) ) )  ->  (
( g " c
)  i^i  ( b  \  { j } ) )  =  ( ( g " c ) 
\  { j } ) )
107106ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  ( A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) )  /\  (
i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  /\  c  e.  ~P (
f  \  { i } ) )  -> 
( ( g "
c )  i^i  (
b  \  { j } ) )  =  ( ( g "
c )  \  {
j } ) )
10893, 107eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  ( A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) )  /\  (
i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  /\  c  e.  ~P (
f  \  { i } ) )  -> 
( ( g "
( c  i^i  (
f  \  { i } ) ) )  i^i  ( b  \  { j } ) )  =  ( ( g " c ) 
\  { j } ) )
10988, 108breqtrrd 4241 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  ( A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) )  /\  (
i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  /\  c  e.  ~P (
f  \  { i } ) )  -> 
c  ~<_  ( ( g
" ( c  i^i  ( f  \  {
i } ) ) )  i^i  ( b 
\  { j } ) ) )
110109ralrimiva 2791 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( f  e. 
Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  ( A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) )  /\  (
i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  A. c  e.  ~P  ( f  \  {
i } ) c  ~<_  ( ( g "
( c  i^i  (
f  \  { i } ) ) )  i^i  ( b  \  { j } ) ) )
111 id 21 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  d  ->  c  =  d )
112 imainrect 5315 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( g  i^i  ( ( f  \  { i } )  X.  (
b  \  { j } ) ) )
" c )  =  ( ( g "
( c  i^i  (
f  \  { i } ) ) )  i^i  ( b  \  { j } ) )
113 imaeq2 5202 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  d  ->  (
( g  i^i  (
( f  \  {
i } )  X.  ( b  \  {
j } ) ) ) " c )  =  ( ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) ) "
d ) )
114112, 113syl5eqr 2484 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  d  ->  (
( g " (
c  i^i  ( f  \  { i } ) ) )  i^i  (
b  \  { j } ) )  =  ( ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) " d
) )
115111, 114breq12d 4228 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  d  ->  (
c  ~<_  ( ( g
" ( c  i^i  ( f  \  {
i } ) ) )  i^i  ( b 
\  { j } ) )  <->  d  ~<_  ( ( g  i^i  ( ( f  \  { i } )  X.  (
b  \  { j } ) ) )
" d ) ) )
116115cbvralv 2934 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. c  e.  ~P  (
f  \  { i } ) c  ~<_  ( ( g " (
c  i^i  ( f  \  { i } ) ) )  i^i  (
b  \  { j } ) )  <->  A. d  e.  ~P  ( f  \  { i } ) d  ~<_  ( ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) ) "
d ) )
117110, 116sylib 190 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( f  e. 
Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  ( A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) )  /\  (
i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  A. d  e.  ~P  ( f  \  {
i } ) d  ~<_  ( ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) " d
) )
118117adantllr 701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  ( i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  A. d  e.  ~P  ( f  \  { i } ) d  ~<_  ( ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) ) "
d ) )
119 inss2 3564 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  C_  ( ( f  \  { i } )  X.  ( b  \  { j } ) )
120 difss 3476 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( b 
\  { j } )  C_  b
121 xpss2 4988 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  \  { j } )  C_  b  ->  ( ( f  \  { i } )  X.  ( b  \  { j } ) )  C_  ( (
f  \  { i } )  X.  b
) )
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f  \  { i } )  X.  (
b  \  { j } ) )  C_  ( ( f  \  { i } )  X.  b )
123119, 122sstri 3359 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  C_  ( ( f  \  { i } )  X.  b )
12445inex1 4347 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  e. 
_V
125124elpw 3807 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  i^i  ( ( f  \  { i } )  X.  (
b  \  { j } ) ) )  e.  ~P ( ( f  \  { i } )  X.  b
)  <->  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) )  C_  (
( f  \  {
i } )  X.  b ) )
126123, 125mpbir 202 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  e. 
~P ( ( f 
\  { i } )  X.  b )
127 simpllr 737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  ( i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  A. a
( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )
12869adantr 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  f  /\  j  e.  ( g " { i } ) )  ->  ( f  \  { i } ) 
C.  f )
129128ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  ( i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  ( f  \  { i } ) 
C.  f )
130 vex 2961 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  f  e. 
_V
131 difexg 4354 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  e.  _V  ->  (
f  \  { i } )  e.  _V )
132130, 131ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f 
\  { i } )  e.  _V
133 psseq1 3436 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  ( f  \  { i } )  ->  ( a  C.  f 
<->  ( f  \  {
i } )  C.  f ) )
134 xpeq1 4895 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f  \  { i } )  ->  ( a  X.  b )  =  ( ( f  \  {
i } )  X.  b ) )
135134pweqd 3806 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( f  \  { i } )  ->  ~P ( a  X.  b )  =  ~P ( ( f 
\  { i } )  X.  b ) )
136 pweq 3804 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  ( f  \  { i } )  ->  ~P a  =  ~P ( f  \  { i } ) )
137136raleqdv 2912 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f  \  { i } )  ->  ( A. d  e.  ~P  a d  ~<_  ( c " d )  <->  A. d  e.  ~P  ( f  \  {
i } ) d  ~<_  ( c " d
) ) )
138 f1eq2 5638 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  ( f  \  { i } )  ->  ( e : a -1-1-> _V  <->  e : ( f  \  { i } ) -1-1-> _V )
)
139138rexbidv 2728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f  \  { i } )  ->  ( E. e  e.  ~P  c e : a -1-1-> _V  <->  E. e  e.  ~P  c e : ( f  \  { i } ) -1-1-> _V )
)
140137, 139imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( f  \  { i } )  ->  ( ( A. d  e.  ~P  a
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : a -1-1-> _V )  <->  ( A. d  e.  ~P  (
f  \  { i } ) d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : ( f  \  { i } ) -1-1-> _V )
) )
141135, 140raleqbidv 2918 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  ( f  \  { i } )  ->  ( A. c  e.  ~P  ( a  X.  b ) ( A. d  e.  ~P  a
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : a -1-1-> _V )  <->  A. c  e.  ~P  ( ( f 
\  { i } )  X.  b ) ( A. d  e. 
~P  ( f  \  { i } ) d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : ( f  \  {
i } ) -1-1-> _V ) ) )
142133, 141imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  ( f  \  { i } )  ->  ( ( a 
C.  f  ->  A. c  e.  ~P  ( a  X.  b ) ( A. d  e.  ~P  a
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : a -1-1-> _V ) )  <->  ( (
f  \  { i } )  C.  f  ->  A. c  e.  ~P  ( ( f  \  { i } )  X.  b ) ( A. d  e.  ~P  ( f  \  {
i } ) d  ~<_  ( c " d
)  ->  E. e  e.  ~P  c e : ( f  \  {
i } ) -1-1-> _V ) ) ) )
143132, 142spcv 3044 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) )  -> 
( ( f  \  { i } ) 
C.  f  ->  A. c  e.  ~P  ( ( f 
\  { i } )  X.  b ) ( A. d  e. 
~P  ( f  \  { i } ) d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : ( f  \  {
i } ) -1-1-> _V ) ) )
144127, 129, 143sylc 59 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  ( i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  A. c  e.  ~P  ( ( f 
\  { i } )  X.  b ) ( A. d  e. 
~P  ( f  \  { i } ) d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : ( f  \  {
i } ) -1-1-> _V ) )
145 imaeq1 5201 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) )  ->  (
c " d )  =  ( ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) ) "
d ) )
146145breq2d 4227 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) )  ->  (
d  ~<_  ( c "
d )  <->  d  ~<_  ( ( g  i^i  ( ( f  \  { i } )  X.  (
b  \  { j } ) ) )
" d ) ) )
147146ralbidv 2727 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) )  ->  ( A. d  e.  ~P  ( f  \  {
i } ) d  ~<_  ( c " d
)  <->  A. d  e.  ~P  ( f  \  {
i } ) d  ~<_  ( ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) " d
) ) )
148 pweq 3804 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) )  ->  ~P c  =  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) )
149148rexeqdv 2913 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) )  ->  ( E. e  e.  ~P  c e : ( f  \  { i } ) -1-1-> _V  <->  E. e  e.  ~P  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) e : ( f  \  {
i } ) -1-1-> _V ) )
150147, 149imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  =  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) )  ->  (
( A. d  e. 
~P  ( f  \  { i } ) d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : ( f  \  {
i } ) -1-1-> _V ) 
<->  ( A. d  e. 
~P  ( f  \  { i } ) d  ~<_  ( ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) ) "
d )  ->  E. e  e.  ~P  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) e : ( f  \  {
i } ) -1-1-> _V ) ) )
151150rspcva 3052 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( g  i^i  (
( f  \  {
i } )  X.  ( b  \  {
j } ) ) )  e.  ~P (
( f  \  {
i } )  X.  b )  /\  A. c  e.  ~P  (
( f  \  {
i } )  X.  b ) ( A. d  e.  ~P  (
f  \  { i } ) d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : ( f  \  { i } ) -1-1-> _V )
)  ->  ( A. d  e.  ~P  (
f  \  { i } ) d  ~<_  ( ( g  i^i  (
( f  \  {
i } )  X.  ( b  \  {
j } ) ) ) " d )  ->  E. e  e.  ~P  ( g  i^i  (
( f  \  {
i } )  X.  ( b  \  {
j } ) ) ) e : ( f  \  { i } ) -1-1-> _V )
)
152126, 144, 151sylancr 646 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  ( i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  ( A. d  e.  ~P  (
f  \  { i } ) d  ~<_  ( ( g  i^i  (
( f  \  {
i } )  X.  ( b  \  {
j } ) ) ) " d )  ->  E. e  e.  ~P  ( g  i^i  (
( f  \  {
i } )  X.  ( b  \  {
j } ) ) ) e : ( f  \  { i } ) -1-1-> _V )
)
153118, 152mpd 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  ( i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  E. e  e.  ~P  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) e : ( f  \  {
i } ) -1-1-> _V )
154 f1eq1 5637 . . . . . . . . . . . . . . . . . . . . 21  |-  ( e  =  k  ->  (
e : ( f 
\  { i } ) -1-1-> _V  <->  k : ( f  \  { i } ) -1-1-> _V )
)
155154cbvrexv 2935 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. e  e.  ~P  (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) e : ( f 
\  { i } ) -1-1-> _V  <->  E. k  e.  ~P  ( g  i^i  (
( f  \  {
i } )  X.  ( b  \  {
j } ) ) ) k : ( f  \  { i } ) -1-1-> _V )
156153, 155sylib 190 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  ( i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  E. k  e.  ~P  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) k : ( f  \  {
i } ) -1-1-> _V )
157 vex 2961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  j  e. 
_V
15838, 157elimasn 5232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  e.  ( g " { i } )  <->  <. i ,  j >.  e.  g )
159158biimpi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ( g " { i } )  ->  <. i ,  j
>.  e.  g )
160159snssd 3945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  e.  ( g " { i } )  ->  { <. i ,  j >. }  C_  g )
161160ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( i  e.  f  /\  j  e.  ( g " { i } ) )  /\  k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) )  ->  { <. i ,  j >. }  C_  g )
162 elpwi 3809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  -> 
k  C_  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) )
163 inss1 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  C_  g
164162, 163syl6ss 3362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  -> 
k  C_  g )
165164adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( i  e.  f  /\  j  e.  ( g " { i } ) )  /\  k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) )  ->  k  C_  g )
166161, 165unssd 3525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( i  e.  f  /\  j  e.  ( g " { i } ) )  /\  k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) )  ->  ( { <. i ,  j >. }  u.  k )  C_  g )
16745elpw2 4367 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( { <. i ,  j
>. }  u.  k )  e.  ~P g  <->  ( { <. i ,  j >. }  u.  k )  C_  g )
168166, 167sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( i  e.  f  /\  j  e.  ( g " { i } ) )  /\  k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) )  ->  ( { <. i ,  j >. }  u.  k )  e.  ~P g )
169168ad2ant2lr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( g  e.  ~P ( f  X.  b
)  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  /\  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  /\  k : ( f  \  { i } )
-1-1-> _V ) )  -> 
( { <. i ,  j >. }  u.  k )  e.  ~P g )
17038, 157f1osn 5718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  { <. i ,  j >. } : { i } -1-1-onto-> { j }
171170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) )  /\  k : ( f  \  { i } ) -1-1-> _V )  ->  { <. i ,  j
>. } : { i } -1-1-onto-> { j } )
172 f1f1orn 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k : ( f  \  { i } )
-1-1-> _V  ->  k :
( f  \  {
i } ) -1-1-onto-> ran  k
)
173172adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) )  /\  k : ( f  \  { i } ) -1-1-> _V )  ->  k : ( f 
\  { i } ) -1-1-onto-> ran  k )
174 disjdif 3702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( { i }  i^i  (
f  \  { i } ) )  =  (/)
175174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) )  /\  k : ( f  \  { i } ) -1-1-> _V )  ->  ( { i }  i^i  ( f  \  { i } ) )  =  (/) )
176 incom 3535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( { j }  i^i  ran  k )  =  ( ran  k  i^i  {
j } )
177162, 119syl6ss 3362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  -> 
k  C_  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) )
178 rnss 5101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k 
C_  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) )  ->  ran  k  C_  ran  ( ( f  \  { i } )  X.  (
b  \  { j } ) ) )
179 rnxpss 5304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ran  (
( f  \  {
i } )  X.  ( b  \  {
j } ) ) 
C_  ( b  \  { j } )
180178, 179syl6ss 3362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k 
C_  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) )  ->  ran  k  C_  ( b  \  { j } ) )
181177, 180syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  ->  ran  k  C_  ( b 
\  { j } ) )
182 incom 3535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( b  \  { j } )  i^i  {
j } )  =  ( { j }  i^i  ( b  \  { j } ) )
183 disjdif 3702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( { j }  i^i  (
b  \  { j } ) )  =  (/)
184182, 183eqtri 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( b  \  { j } )  i^i  {
j } )  =  (/)
185 ssdisj 3679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ran  k  C_  (
b  \  { j } )  /\  (
( b  \  {
j } )  i^i 
{ j } )  =  (/) )  ->  ( ran  k  i^i  { j } )  =  (/) )
186181, 184, 185sylancl 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  -> 
( ran  k  i^i  { j } )  =  (/) )
187176, 186syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  -> 
( { j }  i^i  ran  k )  =  (/) )
188187adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) )  /\  k : ( f  \  { i } ) -1-1-> _V )  ->  ( { j }  i^i  ran  k )  =  (/) )
189 f1oun 5697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( { <. i ,  j >. } : { i } -1-1-onto-> { j }  /\  k : ( f  \  { i } ) -1-1-onto-> ran  k )  /\  (
( { i }  i^i  ( f  \  { i } ) )  =  (/)  /\  ( { j }  i^i  ran  k )  =  (/) ) )  ->  ( { <. i ,  j
>. }  u.  k ) : ( { i }  u.  ( f 
\  { i } ) ) -1-1-onto-> ( { j }  u.  ran  k ) )
190171, 173, 175, 188, 189syl22anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) )  /\  k : ( f  \  { i } ) -1-1-> _V )  ->  ( { <. i ,  j >. }  u.  k ) : ( { i }  u.  ( f  \  {
i } ) ) -1-1-onto-> ( { j }  u.  ran  k ) )
191190adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( g  e.  ~P ( f  X.  b
)  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  /\  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  /\  k : ( f  \  { i } )
-1-1-> _V ) )  -> 
( { <. i ,  j >. }  u.  k ) : ( { i }  u.  ( f  \  {
i } ) ) -1-1-onto-> ( { j }  u.  ran  k ) )
192 snssi 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  f  ->  { i }  C_  f )
193192ad2antrl 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( g  e.  ~P (
f  X.  b )  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  ->  { i }  C_  f )
194 undif 3710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( { i }  C_  f  <->  ( { i }  u.  ( f  \  {
i } ) )  =  f )
195193, 194sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( g  e.  ~P (
f  X.  b )  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  ->  ( {
i }  u.  (
f  \  { i } ) )  =  f )
196 f1oeq2 5669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( { i }  u.  ( f  \  {
i } ) )  =  f  ->  (
( { <. i ,  j >. }  u.  k ) : ( { i }  u.  ( f  \  {
i } ) ) -1-1-onto-> ( { j }  u.  ran  k )  <->  ( { <. i ,  j >. }  u.  k ) : f -1-1-onto-> ( { j }  u.  ran  k ) ) )
197195, 196syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( g  e.  ~P (
f  X.  b )  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  ->  ( ( { <. i ,  j
>. }  u.  k ) : ( { i }  u.  ( f 
\  { i } ) ) -1-1-onto-> ( { j }  u.  ran  k )  <-> 
( { <. i ,  j >. }  u.  k ) : f -1-1-onto-> ( { j }  u.  ran  k ) ) )
198197adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( g  e.  ~P ( f  X.  b
)  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  /\  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  /\  k : ( f  \  { i } )
-1-1-> _V ) )  -> 
( ( { <. i ,  j >. }  u.  k ) : ( { i }  u.  ( f  \  {
i } ) ) -1-1-onto-> ( { j }  u.  ran  k )  <->  ( { <. i ,  j >. }  u.  k ) : f -1-1-onto-> ( { j }  u.  ran  k ) ) )
199191, 198mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( g  e.  ~P ( f  X.  b
)  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  /\  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  /\  k : ( f  \  { i } )
-1-1-> _V ) )  -> 
( { <. i ,  j >. }  u.  k ) : f -1-1-onto-> ( { j }  u.  ran  k ) )
200 f1of1 5676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( { <. i ,  j
>. }  u.  k ) : f -1-1-onto-> ( { j }  u.  ran  k )  ->  ( { <. i ,  j >. }  u.  k ) : f
-1-1-> ( { j }  u.  ran  k ) )
201 ssv 3370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( { j }  u.  ran  k )  C_  _V
202 f1ss 5647 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( { <. i ,  j >. }  u.  k ) : f
-1-1-> ( { j }  u.  ran  k )  /\  ( { j }  u.  ran  k
)  C_  _V )  ->  ( { <. i ,  j >. }  u.  k ) : f
-1-1-> _V )
203200, 201, 202sylancl 645 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( { <. i ,  j
>. }  u.  k ) : f -1-1-onto-> ( { j }  u.  ran  k )  ->  ( { <. i ,  j >. }  u.  k ) : f
-1-1-> _V )
204199, 203syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( g  e.  ~P ( f  X.  b
)  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  /\  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  /\  k : ( f  \  { i } )
-1-1-> _V ) )  -> 
( { <. i ,  j >. }  u.  k ) : f
-1-1-> _V )
205 f1eq1 5637 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( e  =  ( { <. i ,  j >. }  u.  k )  ->  (
e : f -1-1-> _V  <->  ( { <. i ,  j
>. }  u.  k ) : f -1-1-> _V )
)
206205rspcev 3054 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( { <. i ,  j >. }  u.  k )  e.  ~P g  /\  ( { <. i ,  j >. }  u.  k ) : f
-1-1-> _V )  ->  E. e  e.  ~P  g e : f -1-1-> _V )
207169, 204, 206syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( g  e.  ~P ( f  X.  b
)  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  /\  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  /\  k : ( f  \  { i } )
-1-1-> _V ) )  ->  E. e  e.  ~P  g e : f
-1-1-> _V )
208207rexlimdvaa 2833 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g  e.  ~P (
f  X.  b )  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  ->  ( E. k  e.  ~P  (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) k : ( f 
\  { i } ) -1-1-> _V  ->  E. e  e.  ~P  g e : f -1-1-> _V ) )
209208ex 425 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  e.  ~P ( f  X.  b )  -> 
( ( i  e.  f  /\  j  e.  ( g " {
i } ) )  ->  ( E. k  e.  ~P  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) k : ( f  \  {
i } ) -1-1-> _V  ->  E. e  e.  ~P  g e : f
-1-1-> _V ) ) )
210209adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) )  ->  ( (
i  e.  f  /\  j  e.  ( g " { i } ) )  ->  ( E. k  e.  ~P  (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) k : ( f 
\  { i } ) -1-1-> _V  ->  E. e  e.  ~P  g e : f -1-1-> _V ) ) )
211210ad2antlr 709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( f  e. 
Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) ) )  -> 
( ( i  e.  f  /\  j  e.  ( g " {
i } ) )  ->  ( E. k  e.  ~P  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) k : ( f  \  {
i } ) -1-1-> _V  ->  E. e  e.  ~P  g e : f
-1-1-> _V ) ) )
212211impr 604 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( f  e. 
Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  ( A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) )  /\  (
i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  -> 
( E. k  e. 
~P  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) k : ( f  \  {
i } ) -1-1-> _V  ->  E. e  e.  ~P  g e : f
-1-1-> _V ) )
213212adantllr 701 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  ( i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  ( E. k  e.  ~P  (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) k : ( f 
\  { i } ) -1-1-> _V  ->  E. e  e.  ~P  g e : f -1-1-> _V ) )
214156, 213mpd 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  ( i  e.  f  /\  j  e.  ( g " { i } ) ) ) )  ->  E. e  e.  ~P  g e : f -1-1-> _V )
215214expr 600 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) ) )  ->  ( ( i  e.  f  /\  j  e.  ( g " {
i } ) )  ->  E. e  e.  ~P  g e : f
-1-1-> _V ) )
216215exp3a 427 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) ) )  ->  ( i  e.  f  ->  ( j  e.  ( g " {
i } )  ->  E. e  e.  ~P  g e : f
-1-1-> _V ) ) )
217216impr 604 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )
)  ->  ( j  e.  ( g " {
i } )  ->  E. e  e.  ~P  g e : f
-1-1-> _V ) )
218217exlimdv 1647 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )
)  ->  ( E. j  j  e.  (
g " { i } )  ->  E. e  e.  ~P  g e : f -1-1-> _V ) )
21957, 218mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )
)  ->  E. e  e.  ~P  g e : f -1-1-> _V )
220219expr 600 . . . . . . . . . . . 12  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) ) )  ->  ( i  e.  f  ->  E. e  e.  ~P  g e : f -1-1-> _V ) )
221220exlimdv 1647 . . . . . . . . . . 11  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) ) )  ->  ( E. i 
i  e.  f  ->  E. e  e.  ~P  g e : f
-1-1-> _V ) )
22232, 221syl5bi 210 . . . . . . . . . 10  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) ) )  ->  ( f  =/=  (/)  ->  E. e  e.  ~P  g e : f
-1-1-> _V ) )
22331, 222pm2.61dne 2683 . . . . . . . . 9  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) ) )  ->  E. e  e.  ~P  g e : f
-1-1-> _V )
224 exanali 1596 . . . . . . . . . 10  |-  ( E. h ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) )  <->  -.  A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) ) )
225 simprll 740 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  h  C.  f
)
226 pssss 3444 . . . . . . . . . . . . . . . . . . . 20  |-  ( h 
C.  f  ->  h  C_  f )
227225, 226syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  h  C_  f
)
228 sspwb 4416 . . . . . . . . . . . . . . . . . . 19  |-  ( h 
C_  f  <->  ~P h  C_ 
~P f )
229227, 228sylib 190 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  ~P h  C_  ~P f )
230 simplrr 739 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  A. d  e.  ~P  f d  ~<_  ( g
" d ) )
231 ssralv 3409 . . . . . . . . . . . . . . . . . 18  |-  ( ~P h  C_  ~P f  ->  ( A. d  e. 
~P  f d  ~<_  ( g " d )  ->  A. d  e.  ~P  h d  ~<_  ( g
" d ) ) )
232229, 230, 231sylc 59 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  A. d  e.  ~P  h d  ~<_  ( g
" d ) )
233 elpwi 3809 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  e.  ~P h  -> 
d  C_  h )
234 resima2 5182 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d 
C_  h  ->  (
( g  |`  h
) " d )  =  ( g "
d ) )
235233, 234syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  e.  ~P h  -> 
( ( g  |`  h ) " d
)  =  ( g
" d ) )
236235eqcomd 2443 . . . . . . . . . . . . . . . . . . 19  |-  ( d  e.  ~P h  -> 
( g " d
)  =  ( ( g  |`  h ) " d ) )
237236breq2d 4227 . . . . . . . . . . . . . . . . . 18  |-  ( d  e.  ~P h  -> 
( d  ~<_  ( g
" d )  <->  d  ~<_  ( ( g  |`  h ) " d ) ) )
238237ralbiia 2739 . . . . . . . . . . . . . . . . 17  |-  ( A. d  e.  ~P  h
d  ~<_  ( g "
d )  <->  A. d  e.  ~P  h d  ~<_  ( ( g  |`  h
) " d ) )
239232, 238sylib 190 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  A. d  e.  ~P  h d  ~<_  ( ( g  |`  h ) " d ) )
240 simplrl 738 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  g  e.  ~P ( f  X.  b
) )
241 ssres 5175 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g 
C_  ( f  X.  b )  ->  (
g  |`  h )  C_  ( ( f  X.  b )  |`  h
) )
242 df-res 4893 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f  X.  b )  |`  h )  =  ( ( f  X.  b
)  i^i  ( h  X.  _V ) )
243 inxp 5010 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f  X.  b )  i^i  ( h  X.  _V ) )  =  ( ( f  i^i  h
)  X.  ( b  i^i  _V ) )
244 inss2 3564 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  i^i  h )  C_  h
245 inss1 3563 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  i^i  _V )  C_  b
246 xpss12 4984 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( f  i^i  h
)  C_  h  /\  ( b  i^i  _V )  C_  b )  -> 
( ( f  i^i  h )  X.  (
b  i^i  _V )
)  C_  ( h  X.  b ) )
247244, 245, 246mp2an 655 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f  i^i  h )  X.  ( b  i^i 
_V ) )  C_  ( h  X.  b
)
248243, 247eqsstri 3380 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f  X.  b )  i^i  ( h  X.  _V ) )  C_  (
h  X.  b )
249242, 248eqsstri 3380 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  X.  b )  |`  h )  C_  (
h  X.  b )
250241, 249syl6ss 3362 . . . . . . . . . . . . . . . . . . . 20  |-  ( g 
C_  ( f  X.  b )  ->  (
g  |`  h )  C_  ( h  X.  b
) )
25196, 250syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( g  e.  ~P ( f  X.  b )  -> 
( g  |`  h
)  C_  ( h  X.  b ) )
25245resex 5189 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  |`  h )  e.  _V
253252elpw 3807 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g  |`  h )  e.  ~P ( h  X.  b )  <->  ( g  |`  h )  C_  (
h  X.  b ) )
254251, 253sylibr 205 . . . . . . . . . . . . . . . . . 18  |-  ( g  e.  ~P ( f  X.  b )  -> 
( g  |`  h
)  e.  ~P (
h  X.  b ) )
255240, 254syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  ( g  |`  h )  e.  ~P ( h  X.  b
) )
256 simpllr 737 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  A. a ( a 
C.  f  ->  A. c  e.  ~P  ( a  X.  b ) ( A. d  e.  ~P  a
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : a -1-1-> _V ) ) )
257 psseq1 3436 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  h  ->  (
a  C.  f  <->  h  C.  f ) )
258 xpeq1 4895 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  h  ->  (
a  X.  b )  =  ( h  X.  b ) )
259258pweqd 3806 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  h  ->  ~P ( a  X.  b
)  =  ~P (
h  X.  b ) )
260 pweq 3804 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  h  ->  ~P a  =  ~P h
)
261260raleqdv 2912 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  h  ->  ( A. d  e.  ~P  a d  ~<_  ( c
" d )  <->  A. d  e.  ~P  h d  ~<_  ( c " d ) ) )
262 f1eq2 5638 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  h  ->  (
e : a -1-1-> _V  <->  e : h -1-1-> _V )
)
263262rexbidv 2728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  h  ->  ( E. e  e.  ~P  c e : a
-1-1-> _V  <->  E. e  e.  ~P  c e : h
-1-1-> _V ) )
264261, 263imbi12d 313 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  h  ->  (
( A. d  e. 
~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V )  <->  ( A. d  e.  ~P  h
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : h -1-1-> _V ) ) )
265259, 264raleqbidv 2918 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  h  ->  ( A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V )  <->  A. c  e.  ~P  ( h  X.  b ) ( A. d  e.  ~P  h
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : h -1-1-> _V ) ) )
266257, 265imbi12d 313 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  h  ->  (
( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) )  <->  ( h  C.  f  ->  A. c  e.  ~P  ( h  X.  b ) ( A. d  e.  ~P  h
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : h -1-1-> _V ) ) ) )
267266spv 1966 . . . . . . . . . . . . . . . . . 18  |-  ( A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) )  -> 
( h  C.  f  ->  A. c  e.  ~P  ( h  X.  b
) ( A. d  e.  ~P  h d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : h
-1-1-> _V ) ) )
268256, 225, 267sylc 59 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  A. c  e.  ~P  ( h  X.  b
) ( A. d  e.  ~P  h d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : h
-1-1-> _V ) )
269 imaeq1 5201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  =  ( g  |`  h )  ->  (
c " d )  =  ( ( g  |`  h ) " d
) )
270269breq2d 4227 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  ( g  |`  h )  ->  (
d  ~<_  ( c "
d )  <->  d  ~<_  ( ( g  |`  h ) " d ) ) )
271270ralbidv 2727 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  ( g  |`  h )  ->  ( A. d  e.  ~P  h d  ~<_  ( c
" d )  <->  A. d  e.  ~P  h d  ~<_  ( ( g  |`  h
) " d ) ) )
272 pweq 3804 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  ( g  |`  h )  ->  ~P c  =  ~P (
g  |`  h ) )
273272rexeqdv 2913 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  ( g  |`  h )  ->  ( E. e  e.  ~P  c e : h
-1-1-> _V  <->  E. e  e.  ~P  ( g  |`  h
) e : h
-1-1-> _V ) )
274271, 273imbi12d 313 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  ( g  |`  h )  ->  (
( A. d  e. 
~P  h d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : h
-1-1-> _V )  <->  ( A. d  e.  ~P  h
d  ~<_  ( ( g  |`  h ) " d
)  ->  E. e  e.  ~P  ( g  |`  h ) e : h -1-1-> _V ) ) )
275274rspcva 3052 . . . . . . . . . . . . . . . . 17  |-  ( ( ( g  |`  h
)  e.  ~P (
h  X.  b )  /\  A. c  e. 
~P  ( h  X.  b ) ( A. d  e.  ~P  h
d  ~<_  ( c "
d )  ->  E. e  e.  ~P  c e : h -1-1-> _V ) )  -> 
( A. d  e. 
~P  h d  ~<_  ( ( g  |`  h
) " d )  ->  E. e  e.  ~P  ( g  |`  h
) e : h
-1-1-> _V ) )
276255, 268, 275syl2anc 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  ( A. d  e.  ~P  h d  ~<_  ( ( g  |`  h
) " d )  ->  E. e  e.  ~P  ( g  |`  h
) e : h
-1-1-> _V ) )
277239, 276mpd 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  E. e  e.  ~P  ( g  |`  h
) e : h
-1-1-> _V )
278 f1eq1 5637 . . . . . . . . . . . . . . . 16  |-  ( e  =  i  ->  (
e : h -1-1-> _V  <->  i : h -1-1-> _V )
)
279278cbvrexv 2935 . . . . . . . . . . . . . . 15  |-  ( E. e  e.  ~P  (
g  |`  h ) e : h -1-1-> _V  <->  E. i  e.  ~P  ( g  |`  h ) i : h -1-1-> _V )
280277, 279sylib 190 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  A. a ( a  C.  f  ->  A. c  e.  ~P  ( a  X.  b
) ( A. d  e.  ~P  a d  ~<_  ( c " d )  ->  E. e  e.  ~P  c e : a
-1-1-> _V ) ) )  /\  ( g  e. 
~P ( f  X.  b )  /\  A. d  e.  ~P  f
d  ~<_  ( g "
d ) ) )  /\  ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) ) )  ->  E. i  e.  ~P  ( g  |`  h
) i : h
-1-1-> _V )
281226ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( h  C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g
" h ) )  ->  h  C_  f
)
282281ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  (
( h  C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g
" h ) ) )  /\  c  e. 
~P ( f  \  h ) )  ->  h  C_  f )
283 elpwi 3809 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  ~P ( f 
\  h )  -> 
c  C_  ( f  \  h ) )
284 difss 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f 
\  h )  C_  f
285283, 284syl6ss 3362 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  e.  ~P ( f 
\  h )  -> 
c  C_  f )
286285adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  (
( h  C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g
" h ) ) )  /\  c  e. 
~P ( f  \  h ) )  -> 
c  C_  f )
287282, 286unssd 3525 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  (
( h  C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g
" h ) ) )  /\  c  e. 
~P ( f  \  h ) )  -> 
( h  u.  c
)  C_  f )
288130elpw2 4367 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  u.  c )  e.  ~P f  <->  ( h  u.  c )  C_  f
)
289287, 288sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  (
( h  C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g
" h ) ) )  /\  c  e. 
~P ( f  \  h ) )  -> 
( h  u.  c
)  e.  ~P f
)
290 simprr 735 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  ( g  e.  ~P ( f  X.  b
)  /\  A. d  e.  ~P  f d  ~<_  ( g " d ) ) )  ->  A. d  e.  ~P  f d  ~<_  ( g " d ) )
291290ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  (
( h  C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g
" h ) ) )  /\  c  e. 
~P ( f  \  h ) )  ->  A. d  e.  ~P  f d  ~<_  ( g
" d ) )
292 id 21 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( d  =  ( h  u.  c )  ->  d  =  ( h  u.  c ) )
293 imaeq2 5202 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( d  =  ( h  u.  c )  ->  (
g " d )  =  ( g "
( h  u.  c
) ) )
294292, 293breq12d 4228 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( d  =  ( h  u.  c )  ->  (
d  ~<_  ( g "
d )  <->  ( h  u.  c )  ~<_  ( g
" ( h  u.  c ) ) ) )
295294rspcva 3052 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h  u.  c
)  e.  ~P f  /\  A. d  e.  ~P  f d  ~<_  ( g
" d ) )  ->  ( h  u.  c )  ~<_  ( g
" ( h  u.  c ) ) )
296289, 291, 295syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( f  e.  Fin  /\  b  e.  Fin )  /\  (
g  e.  ~P (
f  X.  b )  /\  A. d  e. 
~P  f d  ~<_  ( g " d ) ) )  /\  (
( h  C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g
" h ) ) )  /\  c  e. 
~P ( f  \  h ) )  -> 
( h  u.  c
)  ~<_  ( g "
( h  u.  c
) ) )
297 imaundi 5287 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g
" ( h  u.  c ) )  =  ( ( g "
h )  u.  (
g " c ) )
298 undif2 3706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g " h )  u.  ( ( g
" c )  \