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

Theorem marypha1lem 7070
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
StepHypRef Expression
1 xpeq1 4610 . . . . 5  |-  ( a  =  f  ->  (
a  X.  b )  =  ( f  X.  b ) )
21pweqd 3535 . . . 4  |-  ( a  =  f  ->  ~P ( a  X.  b
)  =  ~P (
f  X.  b ) )
3 pweq 3533 . . . . . 6  |-  ( a  =  f  ->  ~P a  =  ~P f
)
43raleqdv 2694 . . . . 5  |-  ( a  =  f  ->  ( A. d  e.  ~P  a d  ~<_  ( c
" d )  <->  A. d  e.  ~P  f d  ~<_  ( c " d ) ) )
5 f1eq2 5290 . . . . . 6  |-  ( a  =  f  ->  (
e : a -1-1-> _V  <->  e : f -1-1-> _V )
)
65rexbidv 2528 . . . . 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 2699 . . 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 4610 . . . . 5  |-  ( a  =  A  ->  (
a  X.  b )  =  ( A  X.  b ) )
1110pweqd 3535 . . . 4  |-  ( a  =  A  ->  ~P ( a  X.  b
)  =  ~P ( A  X.  b ) )
12 pweq 3533 . . . . . 6  |-  ( a  =  A  ->  ~P a  =  ~P A
)
1312raleqdv 2694 . . . . 5  |-  ( a  =  A  ->  ( A. d  e.  ~P  a d  ~<_  ( c
" d )  <->  A. d  e.  ~P  A d  ~<_  ( c " d ) ) )
14 f1eq2 5290 . . . . . 6  |-  ( a  =  A  ->  (
e : a -1-1-> _V  <->  e : A -1-1-> _V )
)
1514rexbidv 2528 . . . . 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 2699 . . 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 1554 . . . 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 2011 . . . 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 4074 . . . . . . . . . . . . 13  |-  (/)  e.  ~P g
24 f10 5364 . . . . . . . . . . . . 13  |-  (/) : (/) -1-1-> _V
25 f1eq1 5289 . . . . . . . . . . . . . 14  |-  ( e  =  (/)  ->  ( e : (/) -1-1-> _V  <->  (/) : (/) -1-1-> _V )
)
2625rcla4ev 2821 . . . . . . . . . . . . 13  |-  ( (
(/)  e.  ~P g  /\  (/) : (/) -1-1-> _V )  ->  E. e  e.  ~P  g e : (/) -1-1-> _V )
2723, 24, 26mp2an 656 . . . . . . . . . . . 12  |-  E. e  e.  ~P  g e :
(/) -1-1-> _V
28 f1eq2 5290 . . . . . . . . . . . . 13  |-  ( f  =  (/)  ->  ( e : f -1-1-> _V  <->  e : (/) -1-1->
_V ) )
2928rexbidv 2528 . . . . . . . . . . . 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 12 . . . . . . . . . 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 3371 . . . . . . . . . . 11  |-  ( f  =/=  (/)  <->  E. i  i  e.  f )
33 snelpwi 4114 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  f  ->  { i }  e.  ~P f
)
34 id 21 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  =  { i }  ->  d  =  {
i } )
35 imaeq2 4915 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  =  { i }  ->  ( g "
d )  =  ( g " { i } ) )
3634, 35breq12d 3933 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d  =  { i }  ->  ( d  ~<_  ( g " d )  <->  { i }  ~<_  ( g
" { i } ) ) )
3736rcla4va 2819 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( { i }  e.  ~P f  /\  A. d  e.  ~P  f d  ~<_  ( g " d ) )  ->  { i }  ~<_  ( g " { i } ) )
38 vex 2730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  i  e. 
_V
3938snnz 3648 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { i }  =/=  (/)
40 snex 4110 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { i }  e.  _V
41400sdom 6877 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (/)  ~<  { i }  <->  { i }  =/=  (/) )
4239, 41mpbir 202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (/)  ~<  { i }
43 sdomdomtr 6879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
(/)  ~<  { i }  /\  { i }  ~<_  ( g " {
i } ) )  ->  (/)  ~<  ( g " { i } ) )
4442, 43mpan 654 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { i }  ~<_  ( g
" { i } )  ->  (/)  ~<  (
g " { i } ) )
45 vex 2730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  g  e. 
_V
46 imaexg 4933 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  e.  _V  ->  (
g " { i } )  e.  _V )
4745, 46ax-mp 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g
" { i } )  e.  _V
48470sdom 6877 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (/)  ~< 
( g " {
i } )  <->  ( g " { i } )  =/=  (/) )
4944, 48sylib 190 . . . . . . . . . . . . . . . . . . . . 21  |-  ( { i }  ~<_  ( g
" { i } )  ->  ( g " { i } )  =/=  (/) )
5037, 49syl 17 . . . . . . . . . . . . . . . . . . . 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 30 . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . 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 605 . . . . . . . . . . . . . . 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 3371 . . . . . . . . . . . . . . 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 4933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( g  e.  _V  ->  (
g " c )  e.  _V )
59 difexg 4058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( g " c )  e.  _V  ->  (
( g " c
)  \  { j } )  e.  _V )
6045, 58, 59mp2b 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( g " c ) 
\  { j } )  e.  _V
61600dom 6876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (/)  ~<_  ( ( g " c ) 
\  { j } )
62 breq1 3923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  (/)  ->  ( c  ~<_  ( ( g "
c )  \  {
j } )  <->  (/)  ~<_  ( ( g " c ) 
\  { j } ) ) )
6361, 62mpbiri 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  (/)  ->  c  ~<_  ( ( g " c
)  \  { j } ) )
6463a1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  e.  ~P ( f 
\  { i } )  ->  c  C_  ( f  \  {
i } ) )
6766ad2antrl 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
c  C_  ( f  \  { i } ) )
68 disjsn 3597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( f  i^i  { i } )  =  (/)  <->  -.  i  e.  f )
69 disj4 3410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( f  i^i  { i } )  =  (/)  <->  -.  ( f  \  {
i } )  C.  f )
7068, 69bitr3i 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( -.  i  e.  f  <->  -.  (
f  \  { i } )  C.  f
)
7170con4bii 290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( i  e.  f  <->  ( f  \  { i } ) 
C.  f )
7271biimpi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( i  e.  f  ->  (
f  \  { i } )  C.  f
)
7372ad2antlr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
( f  \  {
i } )  C.  f )
74 sspsstr 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  C_  ( f  \  { i } )  /\  ( f  \  { i } ) 
C.  f )  -> 
c  C.  f )
7567, 73, 74syl2anc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
c  C.  f )
76 simprr 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
c  =/=  (/) )
7775, 76jca 520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
( c  C.  f  /\  c  =/=  (/) ) )
78 psseq1 3184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  c  ->  (
h  C.  f  <->  c  C.  f ) )
79 neeq1 2420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  c  ->  (
h  =/=  (/)  <->  c  =/=  (/) ) )
8078, 79anbi12d 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  =  c  ->  (
( h  C.  f  /\  h  =/=  (/) )  <->  ( c  C.  f  /\  c  =/=  (/) ) ) )
81 id 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  c  ->  h  =  c )
82 imaeq2 4915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  =  c  ->  (
g " h )  =  ( g "
c ) )
8381, 82breq12d 3933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  =  c  ->  (
h  ~<  ( g "
h )  <->  c  ~<  ( g " c ) ) )
8480, 83imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( h  =  c  ->  (
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  <->  ( (
c  C.  f  /\  c  =/=  (/) )  ->  c  ~<  ( g " c
) ) ) )
8584a4v 1996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( A. h ( ( h 
C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g " h
) )  ->  (
( c  C.  f  /\  c  =/=  (/) )  -> 
c  ~<  ( g "
c ) ) )
8665, 77, 85sylc 58 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
c  ~<  ( g "
c ) )
87 domdifsn 6830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c 
~<  ( g " c
)  ->  c  ~<_  ( ( g " c ) 
\  { j } ) )
8886, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  ( c  e.  ~P ( f  \  {
i } )  /\  c  =/=  (/) ) )  -> 
c  ~<_  ( ( g
" c )  \  { j } ) )
8988expr 601 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  c  e.  ~P ( f  \  {
i } ) )  ->  ( c  =/=  (/)  ->  c  ~<_  ( ( g " c ) 
\  { j } ) ) )
9064, 89pm2.61dne 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A. h ( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) )  /\  i  e.  f )  /\  c  e.  ~P ( f  \  {
i } ) )  ->  c  ~<_  ( ( g " c ) 
\  { j } ) )
9190adantlrr 704 . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
9291adantll 697 . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
93 df-ss 3089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c 
C_  ( f  \  { i } )  <-> 
( c  i^i  (
f  \  { i } ) )  =  c )
9466, 93sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  ~P ( f 
\  { i } )  ->  ( c  i^i  ( f  \  {
i } ) )  =  c )
9594imaeq2d 4919 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  ~P ( f 
\  { i } )  ->  ( g " ( c  i^i  ( f  \  {
i } ) ) )  =  ( g
" c ) )
9695ineq1d 3277 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  e.  ~P ( f 
\  { i } )  ->  ( (
g " ( c  i^i  ( f  \  { i } ) ) )  i^i  (
b  \  { j } ) )  =  ( ( g "
c )  i^i  (
b  \  { j } ) ) )
9796adantl 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 } ) ) )
98 indif2 3319 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( g " c )  i^i  ( b  \  { j } ) )  =  ( ( ( g " c
)  i^i  b )  \  { j } )
99 imassrn 4932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( g
" c )  C_  ran  g
100 elpwi 3538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( g  e.  ~P ( f  X.  b )  -> 
g  C_  ( f  X.  b ) )
101 rnss 4814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( g 
C_  ( f  X.  b )  ->  ran  g  C_  ran  (  f  X.  b ) )
102 rnxpss 5015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ran  ( 
f  X.  b ) 
C_  b
103101, 102syl6ss 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( g 
C_  ( f  X.  b )  ->  ran  g  C_  b )
104100, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( g  e.  ~P ( f  X.  b )  ->  ran  g  C_  b )
10599, 104syl5ss 3111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( g  e.  ~P ( f  X.  b )  -> 
( g " c
)  C_  b )
106 df-ss 3089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( g " c ) 
C_  b  <->  ( (
g " c )  i^i  b )  =  ( g " c
) )
107105, 106sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( g  e.  ~P ( f  X.  b )  -> 
( ( g "
c )  i^i  b
)  =  ( g
" c ) )
108107difeq1d 3210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( g  e.  ~P ( f  X.  b )  -> 
( ( ( g
" c )  i^i  b )  \  {
j } )  =  ( ( g "
c )  \  {
j } ) )
109108ad2antrl 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
11098, 109syl5eq 2297 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
111110ad2antrr 709 . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
11297, 111eqtrd 2285 . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
11392, 112breqtrrd 3946 . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
114113ralrimiva 2588 . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
115 id 21 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  d  ->  c  =  d )
116 imainrect 5026 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( g  i^i  ( ( f  \  { i } )  X.  (
b  \  { j } ) ) )
" c )  =  ( ( g "
( c  i^i  (
f  \  { i } ) ) )  i^i  ( b  \  { j } ) )
117 imaeq2 4915 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  d  ->  (
( g  i^i  (
( f  \  {
i } )  X.  ( b  \  {
j } ) ) ) " c )  =  ( ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) ) "
d ) )
118116, 117syl5eqr 2299 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  d  ->  (
( g " (
c  i^i  ( f  \  { i } ) ) )  i^i  (
b  \  { j } ) )  =  ( ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) " d
) )
119115, 118breq12d 3933 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  d  ->  (
c  ~<_  ( ( g
" ( c  i^i  ( f  \  {
i } ) ) )  i^i  ( b 
\  { j } ) )  <->  d  ~<_  ( ( g  i^i  ( ( f  \  { i } )  X.  (
b  \  { j } ) ) )
" d ) ) )
120119cbvralv 2708 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
121114, 120sylib 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
) )
122121adantllr 702 . . . . . . . . . . . . . . . . . . . . 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 ) )
123 inss2 3297 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  C_  ( ( f  \  { i } )  X.  ( b  \  { j } ) )
124 difss 3220 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( b 
\  { j } )  C_  b
125 xpss2 4703 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  \  { j } )  C_  b  ->  ( ( f  \  { i } )  X.  ( b  \  { j } ) )  C_  ( (
f  \  { i } )  X.  b
) )
126124, 125ax-mp 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f  \  { i } )  X.  (
b  \  { j } ) )  C_  ( ( f  \  { i } )  X.  b )
127123, 126sstri 3109 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  C_  ( ( f  \  { i } )  X.  b )
12845inex1 4052 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  e. 
_V
129128elpw 3536 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
130127, 129mpbir 202 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  e. 
~P ( ( f 
\  { i } )  X.  b )
131 simpllr 738 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
13272adantr 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  f  /\  j  e.  ( g " { i } ) )  ->  ( f  \  { i } ) 
C.  f )
133132ad2antll 712 . . . . . . . . . . . . . . . . . . . . . . 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 )
134 vex 2730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  f  e. 
_V
135 difexg 4058 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  e.  _V  ->  (
f  \  { i } )  e.  _V )
136134, 135ax-mp 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f 
\  { i } )  e.  _V
137 psseq1 3184 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  ( f  \  { i } )  ->  ( a  C.  f 
<->  ( f  \  {
i } )  C.  f ) )
138 xpeq1 4610 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f  \  { i } )  ->  ( a  X.  b )  =  ( ( f  \  {
i } )  X.  b ) )
139138pweqd 3535 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( f  \  { i } )  ->  ~P ( a  X.  b )  =  ~P ( ( f 
\  { i } )  X.  b ) )
140 pweq 3533 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  ( f  \  { i } )  ->  ~P a  =  ~P ( f  \  { i } ) )
141140raleqdv 2694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f  \  { i } )  ->  ( A. d  e.  ~P  a d  ~<_  ( c " d )  <->  A. d  e.  ~P  ( f  \  {
i } ) d  ~<_  ( c " d
) ) )
142 f1eq2 5290 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  ( f  \  { i } )  ->  ( e : a -1-1-> _V  <->  e : ( f  \  { i } ) -1-1-> _V )
)
143142rexbidv 2528 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
144141, 143imbi12d 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 )
) )
145139, 144raleqbidv 2699 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
146137, 145imbi12d 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 ) ) ) )
147136, 146cla4v 2811 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
148131, 133, 147sylc 58 . . . . . . . . . . . . . . . . . . . . . 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 ) )
149 imaeq1 4914 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) )  ->  (
c " d )  =  ( ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) ) "
d ) )
150149breq2d 3932 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) )  ->  (
d  ~<_  ( c "
d )  <->  d  ~<_  ( ( g  i^i  ( ( f  \  { i } )  X.  (
b  \  { j } ) ) )
" d ) ) )
151150ralbidv 2527 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
152 pweq 3533 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) )  ->  ~P c  =  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) )
153152rexeqdv 2695 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
154151, 153imbi12d 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 ) ) )
155154rcla4va 2819 . . . . . . . . . . . . . . . . . . . . . 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 )
)
156130, 148, 155sylancr 647 . . . . . . . . . . . . . . . . . . . . 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 )
)
157122, 156mpd 16 . . . . . . . . . . . . . . . . . . . 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 )
158 f1eq1 5289 . . . . . . . . . . . . . . . . . . . . 21  |-  ( e  =  k  ->  (
e : ( f 
\  { i } ) -1-1-> _V  <->  k : ( f  \  { i } ) -1-1-> _V )
)
159158cbvrexv 2709 . . . . . . . . . . . . . . . . . . . 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 )
160157, 159sylib 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 )
161 vex 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  j  e. 
_V
16238, 161elimasn 4945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( j  e.  ( g " { i } )  <->  <. i ,  j >.  e.  g )
163162biimpi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  e.  ( g " { i } )  ->  <. i ,  j
>.  e.  g )
164163snssd 3660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ( g " { i } )  ->  { <. i ,  j >. }  C_  g )
165164ad2antlr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  f  /\  j  e.  ( g " { i } ) )  /\  k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) )  ->  { <. i ,  j >. }  C_  g )
166 elpwi 3538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  -> 
k  C_  ( g  i^i  ( ( f  \  { i } )  X.  ( b  \  { j } ) ) ) )
167 inss1 3296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  C_  g
168166, 167syl6ss 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  -> 
k  C_  g )
169168adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  f  /\  j  e.  ( g " { i } ) )  /\  k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) )  ->  k  C_  g )
170165, 169unssd 3261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( i  e.  f  /\  j  e.  ( g " { i } ) )  /\  k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) ) )  ->  ( { <. i ,  j >. }  u.  k )  C_  g )
17145elpw2 4064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( { <. i ,  j
>. }  u.  k )  e.  ~P g  <->  ( { <. i ,  j >. }  u.  k )  C_  g )
172170, 171sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 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 )
173172ad2ant2lr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  e.  ~P g )
17438, 161f1osn 5370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  { <. i ,  j >. } : { i } -1-1-onto-> { j }
175174a1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) )  /\  k : ( f  \  { i } ) -1-1-> _V )  ->  { <. i ,  j
>. } : { i } -1-1-onto-> { j } )
176 f1f1orn 5340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k : ( f  \  { i } )
-1-1-> _V  ->  k :
( f  \  {
i } ) -1-1-onto-> ran  k
)
177176adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 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 )
178 disjdif 3432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( { i }  i^i  (
f  \  { i } ) )  =  (/)
179178a1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) )  /\  k : ( f  \  { i } ) -1-1-> _V )  ->  ( { i }  i^i  ( f  \  { i } ) )  =  (/) )
180 incom 3269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( { j }  i^i  ran  k )  =  ( ran  k  i^i  {
j } )
181166, 123syl6ss 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  -> 
k  C_  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) )
182 rnss 4814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k 
C_  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) )  ->  ran  k  C_  ran  ( ( f  \  { i } )  X.  (
b  \  { j } ) ) )
183 rnxpss 5015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ran  (
( f  \  {
i } )  X.  ( b  \  {
j } ) ) 
C_  ( b  \  { j } )
184182, 183syl6ss 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k 
C_  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) )  ->  ran  k  C_  ( b  \  { j } ) )
185181, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  ->  ran  k  C_  ( b 
\  { j } ) )
186 incom 3269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( b  \  { j } )  i^i  {
j } )  =  ( { j }  i^i  ( b  \  { j } ) )
187 disjdif 3432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( { j }  i^i  (
b  \  { j } ) )  =  (/)
188186, 187eqtri 2273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( b  \  { j } )  i^i  {
j } )  =  (/)
189 ssdisj 3411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ran  k  C_  (
b  \  { j } )  /\  (
( b  \  {
j } )  i^i 
{ j } )  =  (/) )  ->  ( ran  k  i^i  { j } )  =  (/) )
190185, 188, 189sylancl 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  -> 
( ran  k  i^i  { j } )  =  (/) )
191180, 190syl5eq 2297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  ~P ( g  i^i  ( ( f 
\  { i } )  X.  ( b 
\  { j } ) ) )  -> 
( { j }  i^i  ran  k )  =  (/) )
192191adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( k  e.  ~P (
g  i^i  ( (
f  \  { i } )  X.  (
b  \  { j } ) ) )  /\  k : ( f  \  { i } ) -1-1-> _V )  ->  ( { j }  i^i  ran  k )  =  (/) )
193 f1oun 5349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( { <. 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 ) )
194175, 177, 179, 192, 193syl22anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 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 ) )
195194adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 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 ) )
196 snssi 3659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  f  ->  { i }  C_  f )
197196ad2antrl 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( g  e.  ~P (
f  X.  b )  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  ->  { i }  C_  f )
198 undif 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( { i }  C_  f  <->  ( { i }  u.  ( f  \  {
i } ) )  =  f )
199197, 198sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( g  e.  ~P (
f  X.  b )  /\  ( i  e.  f  /\  j  e.  ( g " {
i } ) ) )  ->  ( {
i }  u.  (
f  \  { i } ) )  =  f )
200 f1oeq2 5321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( { 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 ) ) )
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 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 ) ) )
202201adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 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 ) ) )
203195, 202mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) : f -1-1-onto-> ( { j }  u.  ran  k ) )
204 f1of1 5328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( { <. i ,  j
>. }  u.  k ) : f -1-1-onto-> ( { j }  u.  ran  k )  ->  ( { <. i ,  j >. }  u.  k ) : f
-1-1-> ( { j }  u.  ran  k ) )
205 ssv 3119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( { j }  u.  ran  k )  C_  _V
206 f1ss 5299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( { <. 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 )
207204, 205, 206sylancl 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( { <. i ,  j
>. }  u.  k ) : f -1-1-onto-> ( { j }  u.  ran  k )  ->  ( { <. i ,  j >. }  u.  k ) : f
-1-1-> _V )
208203, 207syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 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-> _V )
209 f1eq1 5289 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( e  =  ( { <. i ,  j >. }  u.  k )  ->  (
e : f -1-1-> _V  <->  ( { <. i ,  j
>. }  u.  k ) : f -1-1-> _V )
)
210209rcla4ev 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( { <. 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 )
211173, 208, 210syl2anc 645 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  E. e  e.  ~P  g e : f
-1-1-> _V )
212211exp32 591 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
213212rexlimdv 2628 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
214213ex 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 ) ) )
215214adantr 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 ) ) )
216215ad2antlr 710 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
217216impr 605 . . . . . . . . . . . . . . . . . . . 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 ) )
218217adantllr 702 . . . . . . . . . . . . . . . . . . 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 ) )
219160, 218mpd 16 . . . . . . . . . . . . . . . . . 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 )
220219expr 601 . . . . . . . . . . . . . . . . 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 ) )
221220exp3a 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 ) ) )
222221impr 605 . . . . . . . . . . . . . . 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 ) )
223222exlimdv 1932 . . . . . . . . . . . . . 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 ) )
22457, 223mpd 16 . . . . . . . . . . . . 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 )
225224expr 601 . . . . . . . . . . . 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 ) )
226225exlimdv 1932 . . . . . . . . . . 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 ) )
22732, 226syl5bi 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 ) )
22831, 227pm2.61dne 2489 . . . . . . . . 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 )
229 exanali 1583 . . . . . . . . . 10  |-  ( E. h ( ( h 
C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g "
h ) )  <->  -.  A. h
( ( h  C.  f  /\  h  =/=  (/) )  ->  h  ~<  ( g "
h ) ) )
230 simprll 741 . . . . . . . . . . . . . . . . . . . 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
)
231 pssss 3192 . . . . . . . . . . . . . . . . . . . 20  |-  ( h 
C.  f  ->  h  C_  f )
232230, 231syl 17 . . . . . . . . . . . . . . . . . . 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
)
233 sspwb 4117 . . . . . . . . . . . . . . . . . . 19  |-  ( h 
C_  f  <->  ~P h  C_ 
~P f )
234232, 233sylib 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 )
235 simplrr 740 . . . . . . . . . . . . . . . . . 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 ) )
236 ssralv 3158 . . . . . . . . . . . . . . . . . 18  |-  ( ~P h  C_  ~P f  ->  ( A. d  e. 
~P  f d  ~<_  ( g " d )  ->  A. d  e.  ~P  h d  ~<_  ( g
" d ) ) )
237234, 235, 236sylc 58 . . . . . . . . . . . . . . . . 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 ) )
238 elpwi 3538 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  e.  ~P h  -> 
d  C_  h )
239 resima2 4895 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d 
C_  h  ->  (
( g  |`  h
) " d )  =  ( g "
d ) )
240238, 239syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  e.  ~P h  -> 
( ( g  |`  h ) " d
)  =  ( g
" d ) )
241240eqcomd 2258 . . . . . . . . . . . . . . . . . . 19  |-  ( d  e.  ~P h  -> 
( g " d
)  =  ( ( g  |`  h ) " d ) )
242241breq2d 3932 . . . . . . . . . . . . . . . . . 18  |-  ( d  e.  ~P h  -> 
( d  ~<_  ( g
" d )  <->  d  ~<_  ( ( g  |`  h ) " d ) ) )
243242ralbiia 2537 . . . . . . . . . . . . . . . . 17  |-  ( A. d  e.  ~P  h
d  ~<_  ( g "
d )  <->  A. d  e.  ~P  h d  ~<_  ( ( g  |`  h
) " d ) )
244237, 243sylib 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 ) )
245 simplrl 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 ) ) )  ->  g  e.  ~P ( f  X.  b
) )
246 ssres 4888 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g 
C_  ( f  X.  b )  ->  (
g  |`  h )  C_  ( ( f  X.  b )  |`  h
) )
247 df-res 4600 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f  X.  b )  |`  h )  =  ( ( f  X.  b
)  i^i  ( h  X.  _V ) )
248 inxp 4725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f  X.  b )  i^i  ( h  X.  _V ) )  =  ( ( f  i^i  h
)  X.  ( b  i^i  _V ) )
249 inss2 3297 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  i^i  h )  C_  h
250 inss1 3296 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  i^i  _V )  C_  b
251 xpss12 4699 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
252249, 250, 251mp2an 656 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f  i^i  h )  X.  ( b  i^i 
_V ) )  C_  ( h  X.  b
)
253248, 252eqsstri 3129 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f  X.  b )  i^i  ( h  X.  _V ) )  C_  (
h  X.  b )
254247, 253eqsstri 3129 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  X.  b )  |`  h )  C_  (
h  X.  b )
255246, 254syl6ss 3112 . . . . . . . . . . . . . . . . . . . 20  |-  ( g 
C_  ( f  X.  b )  ->  (
g  |`  h )  C_  ( h  X.  b
) )
256100, 255syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( g  e.  ~P ( f  X.  b )  -> 
( g  |`  h
)  C_  ( h  X.  b ) )
25745resex 4902 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  |`  h )  e.  _V
258257elpw 3536 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g  |`  h )  e.  ~P ( h  X.  b )  <->  ( g  |`  h )  C_  (
h  X.  b ) )
259256, 258sylibr 205 . . . . . . . . . . . . . . . . . 18  |-  ( g  e.  ~P ( f  X.  b )  -> 
( g  |`  h
)  e.  ~P (
h  X.  b ) )
260245, 259syl 17 . . . . . . . . . . . . . . . . 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
) )
261 simpllr 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 ) ) )  ->  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 ) ) )
262 psseq1 3184 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  h  ->  (
a  C.  f  <->  h  C.  f ) )
263 xpeq1 4610 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  h  ->  (
a  X.  b )  =  ( h  X.  b ) )
264263pweqd 3535 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  h  ->  ~P ( a  X.  b
)  =  ~P (
h  X.  b ) )
265 pweq 3533 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  h  ->  ~P a  =  ~P h
)
266265raleqdv 2694 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  h  ->  ( A. d  e.  ~P  a d  ~<_  ( c
" d )  <->  A. d  e.  ~P  h d  ~<_  ( c " d ) ) )
267 f1eq2 5290 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  h  ->  (
e : a -1-1-> _V  <->  e : h -1-1-> _V )
)
268267rexbidv 2528 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  h  ->  ( E. e  e.  ~P  c e : a
-1-1-> _V  <->  E. e  e.  ~P  c e : h
-1-1-> _V ) )
269266, 268imbi12d 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 ) ) )
270264, 269raleqbidv 2699 . . . . . . . . . . . . . . . . . . . 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 ) ) )
271262, 270imbi12d 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 ) ) ) )
272271a4v 1996 . . . . . . . . . . . . . . . . . 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 ) ) )
273261, 230, 272sylc 58 . . . . . . . . . . . . . . . . 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 ) )
274 imaeq1 4914 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  =  ( g  |`  h )  ->  (
c " d )  =  ( ( g  |`  h ) " d
) )
275274breq2d 3932 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  ( g  |`  h )  ->  (
d  ~<_  ( c "
d )  <->  d  ~<_  ( ( g  |`  h ) " d ) ) )
276275ralbidv 2527 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  ( g  |`  h )  ->  ( A. d  e.  ~P  h d  ~<_  ( c
" d )  <->  A. d  e.  ~P  h d  ~<_  ( ( g  |`  h
) " d ) ) )
277 pweq 3533 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  ( g  |`  h )  ->  ~P c  =  ~P (
g  |`  h ) )
278277rexeqdv 2695 . . . . . . . . . . . . . . . . . . 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 ) )
279276, 278imbi12d 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 ) ) )
280279rcla4va 2819 . . . . . . . . . . . . . . . . 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 ) )
281260, 273, 280syl2anc 645 . . . . . . . . . . . . . . . 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 ) )
282244, 281mpd 16 . . . . . . . . . . . . . . 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 )
283 f1eq1 5289 . . . . . . . . . . . . . . . 16  |-  ( e  =  i  ->  (
e : h -1-1-> _V  <->  i : h -1-1-> _V )
)
284283cbvrexv 2709 . . . . . . . . . . . . . . 15  |-  ( E. e  e.  ~P  (
g  |`  h ) e : h -1-1-> _V  <->  E. i  e.  ~P  ( g  |`  h ) i : h -1-1-> _V )
285282, 284sylib 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 )
286231ad2antrr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( h  C.  f  /\  h  =/=  (/) )  /\  -.  h  ~<  ( g
" h ) )  ->  h  C_  f
)
287286ad2antlr 710 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
288 elpwi 3538 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  ~P ( f 
\  h )  -> 
c  C_  ( f  \  h ) )
289 difss 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f 
\  h )  C_  f
290288, 289syl6ss 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  e.  ~P ( f 
\  h )  -> 
c  C_  f )
291290adantl 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 )
292287, 291unssd 3261 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
293134elpw2 4064 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  u.  c )  e.  ~P f  <->  ( h  u.  c )  C_  f
)
294292, 293sylibr 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
)
295 simprr 736 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
296295ad2antrr 709 . . . . . . . . . . . . . . . . . . . . . . . 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