Metamath Proof Explorer


Theorem marypha1lem

Description: Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 xpeq1
 |-  ( a = f -> ( a X. b ) = ( f X. b ) )
2 1 pweqd
 |-  ( a = f -> ~P ( a X. b ) = ~P ( f X. b ) )
3 pweq
 |-  ( a = f -> ~P a = ~P f )
4 3 raleqdv
 |-  ( a = f -> ( A. d e. ~P a d ~<_ ( c " d ) <-> A. d e. ~P f d ~<_ ( c " d ) ) )
5 f1eq2
 |-  ( a = f -> ( e : a -1-1-> _V <-> e : f -1-1-> _V ) )
6 5 rexbidv
 |-  ( a = f -> ( E. e e. ~P c e : a -1-1-> _V <-> E. e e. ~P c e : f -1-1-> _V ) )
7 4 6 imbi12d
 |-  ( 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 ) ) )
8 2 7 raleqbidv
 |-  ( 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 ) ) )
9 8 imbi2d
 |-  ( 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
 |-  ( a = A -> ( a X. b ) = ( A X. b ) )
11 10 pweqd
 |-  ( a = A -> ~P ( a X. b ) = ~P ( A X. b ) )
12 pweq
 |-  ( a = A -> ~P a = ~P A )
13 12 raleqdv
 |-  ( a = A -> ( A. d e. ~P a d ~<_ ( c " d ) <-> A. d e. ~P A d ~<_ ( c " d ) ) )
14 f1eq2
 |-  ( a = A -> ( e : a -1-1-> _V <-> e : A -1-1-> _V ) )
15 14 rexbidv
 |-  ( a = A -> ( E. e e. ~P c e : a -1-1-> _V <-> E. e e. ~P c e : A -1-1-> _V ) )
16 13 15 imbi12d
 |-  ( 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 ) ) )
17 11 16 raleqbidv
 |-  ( 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 ) ) )
18 17 imbi2d
 |-  ( 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
 |-  ( ( 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 ) ) ) )
20 19 albii
 |-  ( 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
 |-  ( 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 ) ) ) )
22 20 21 bitri
 |-  ( 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
 |-  (/) e. ~P g
24 f10
 |-  (/) : (/) -1-1-> _V
25 f1eq1
 |-  ( e = (/) -> ( e : (/) -1-1-> _V <-> (/) : (/) -1-1-> _V ) )
26 25 rspcev
 |-  ( ( (/) e. ~P g /\ (/) : (/) -1-1-> _V ) -> E. e e. ~P g e : (/) -1-1-> _V )
27 23 24 26 mp2an
 |-  E. e e. ~P g e : (/) -1-1-> _V
28 f1eq2
 |-  ( f = (/) -> ( e : f -1-1-> _V <-> e : (/) -1-1-> _V ) )
29 28 rexbidv
 |-  ( f = (/) -> ( E. e e. ~P g e : f -1-1-> _V <-> E. e e. ~P g e : (/) -1-1-> _V ) )
30 27 29 mpbiri
 |-  ( f = (/) -> E. e e. ~P g e : f -1-1-> _V )
31 30 a1i
 |-  ( ( ( ( ( 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
 |-  ( f =/= (/) <-> E. i i e. f )
33 snelpwi
 |-  ( i e. f -> { i } e. ~P f )
34 id
 |-  ( d = { i } -> d = { i } )
35 imaeq2
 |-  ( d = { i } -> ( g " d ) = ( g " { i } ) )
36 34 35 breq12d
 |-  ( d = { i } -> ( d ~<_ ( g " d ) <-> { i } ~<_ ( g " { i } ) ) )
37 36 rspcva
 |-  ( ( { i } e. ~P f /\ A. d e. ~P f d ~<_ ( g " d ) ) -> { i } ~<_ ( g " { i } ) )
38 vex
 |-  i e. _V
39 38 snnz
 |-  { i } =/= (/)
40 snex
 |-  { i } e. _V
41 40 0sdom
 |-  ( (/) ~< { i } <-> { i } =/= (/) )
42 39 41 mpbir
 |-  (/) ~< { i }
43 sdomdomtr
 |-  ( ( (/) ~< { i } /\ { i } ~<_ ( g " { i } ) ) -> (/) ~< ( g " { i } ) )
44 42 43 mpan
 |-  ( { i } ~<_ ( g " { i } ) -> (/) ~< ( g " { i } ) )
45 vex
 |-  g e. _V
46 45 imaex
 |-  ( g " { i } ) e. _V
47 46 0sdom
 |-  ( (/) ~< ( g " { i } ) <-> ( g " { i } ) =/= (/) )
48 44 47 sylib
 |-  ( { i } ~<_ ( g " { i } ) -> ( g " { i } ) =/= (/) )
49 37 48 syl
 |-  ( ( { i } e. ~P f /\ A. d e. ~P f d ~<_ ( g " d ) ) -> ( g " { i } ) =/= (/) )
50 49 expcom
 |-  ( A. d e. ~P f d ~<_ ( g " d ) -> ( { i } e. ~P f -> ( g " { i } ) =/= (/) ) )
51 33 50 syl5
 |-  ( A. d e. ~P f d ~<_ ( g " d ) -> ( i e. f -> ( g " { i } ) =/= (/) ) )
52 51 adantl
 |-  ( ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) -> ( i e. f -> ( g " { i } ) =/= (/) ) )
53 52 ad2antlr
 |-  ( ( ( ( ( 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 } ) =/= (/) ) )
54 53 impr
 |-  ( ( ( ( ( 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 } ) =/= (/) )
55 n0
 |-  ( ( g " { i } ) =/= (/) <-> E. j j e. ( g " { i } ) )
56 54 55 sylib
 |-  ( ( ( ( ( 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 } ) )
57 45 imaex
 |-  ( g " c ) e. _V
58 57 difexi
 |-  ( ( g " c ) \ { j } ) e. _V
59 58 0dom
 |-  (/) ~<_ ( ( g " c ) \ { j } )
60 breq1
 |-  ( c = (/) -> ( c ~<_ ( ( g " c ) \ { j } ) <-> (/) ~<_ ( ( g " c ) \ { j } ) ) )
61 59 60 mpbiri
 |-  ( c = (/) -> c ~<_ ( ( g " c ) \ { j } ) )
62 61 a1i
 |-  ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ c e. ~P ( f \ { i } ) ) -> ( c = (/) -> c ~<_ ( ( g " c ) \ { j } ) ) )
63 simpll
 |-  ( ( ( 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 ) ) )
64 elpwi
 |-  ( c e. ~P ( f \ { i } ) -> c C_ ( f \ { i } ) )
65 64 ad2antrl
 |-  ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> c C_ ( f \ { i } ) )
66 difsnpss
 |-  ( i e. f <-> ( f \ { i } ) C. f )
67 66 biimpi
 |-  ( i e. f -> ( f \ { i } ) C. f )
68 67 ad2antlr
 |-  ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> ( f \ { i } ) C. f )
69 65 68 sspsstrd
 |-  ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> c C. f )
70 simprr
 |-  ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> c =/= (/) )
71 69 70 jca
 |-  ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> ( c C. f /\ c =/= (/) ) )
72 psseq1
 |-  ( h = c -> ( h C. f <-> c C. f ) )
73 neeq1
 |-  ( h = c -> ( h =/= (/) <-> c =/= (/) ) )
74 72 73 anbi12d
 |-  ( h = c -> ( ( h C. f /\ h =/= (/) ) <-> ( c C. f /\ c =/= (/) ) ) )
75 id
 |-  ( h = c -> h = c )
76 imaeq2
 |-  ( h = c -> ( g " h ) = ( g " c ) )
77 75 76 breq12d
 |-  ( h = c -> ( h ~< ( g " h ) <-> c ~< ( g " c ) ) )
78 74 77 imbi12d
 |-  ( h = c -> ( ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) <-> ( ( c C. f /\ c =/= (/) ) -> c ~< ( g " c ) ) ) )
79 78 spvv
 |-  ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) -> ( ( c C. f /\ c =/= (/) ) -> c ~< ( g " c ) ) )
80 63 71 79 sylc
 |-  ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> c ~< ( g " c ) )
81 domdifsn
 |-  ( c ~< ( g " c ) -> c ~<_ ( ( g " c ) \ { j } ) )
82 80 81 syl
 |-  ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> c ~<_ ( ( g " c ) \ { j } ) )
83 82 expr
 |-  ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ c e. ~P ( f \ { i } ) ) -> ( c =/= (/) -> c ~<_ ( ( g " c ) \ { j } ) ) )
84 62 83 pm2.61dne
 |-  ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ c e. ~P ( f \ { i } ) ) -> c ~<_ ( ( g " c ) \ { j } ) )
85 84 adantlrr
 |-  ( ( ( 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 } ) )
86 85 adantll
 |-  ( ( ( ( ( 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 } ) )
87 df-ss
 |-  ( c C_ ( f \ { i } ) <-> ( c i^i ( f \ { i } ) ) = c )
88 64 87 sylib
 |-  ( c e. ~P ( f \ { i } ) -> ( c i^i ( f \ { i } ) ) = c )
89 88 imaeq2d
 |-  ( c e. ~P ( f \ { i } ) -> ( g " ( c i^i ( f \ { i } ) ) ) = ( g " c ) )
90 89 ineq1d
 |-  ( c e. ~P ( f \ { i } ) -> ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) = ( ( g " c ) i^i ( b \ { j } ) ) )
91 90 adantl
 |-  ( ( ( ( ( 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 } ) ) )
92 indif2
 |-  ( ( g " c ) i^i ( b \ { j } ) ) = ( ( ( g " c ) i^i b ) \ { j } )
93 imassrn
 |-  ( g " c ) C_ ran g
94 elpwi
 |-  ( g e. ~P ( f X. b ) -> g C_ ( f X. b ) )
95 rnss
 |-  ( g C_ ( f X. b ) -> ran g C_ ran ( f X. b ) )
96 rnxpss
 |-  ran ( f X. b ) C_ b
97 95 96 sstrdi
 |-  ( g C_ ( f X. b ) -> ran g C_ b )
98 94 97 syl
 |-  ( g e. ~P ( f X. b ) -> ran g C_ b )
99 93 98 sstrid
 |-  ( g e. ~P ( f X. b ) -> ( g " c ) C_ b )
100 df-ss
 |-  ( ( g " c ) C_ b <-> ( ( g " c ) i^i b ) = ( g " c ) )
101 99 100 sylib
 |-  ( g e. ~P ( f X. b ) -> ( ( g " c ) i^i b ) = ( g " c ) )
102 101 difeq1d
 |-  ( g e. ~P ( f X. b ) -> ( ( ( g " c ) i^i b ) \ { j } ) = ( ( g " c ) \ { j } ) )
103 102 ad2antrl
 |-  ( ( ( 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 } ) )
104 92 103 eqtrid
 |-  ( ( ( 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 } ) )
105 104 ad2antrr
 |-  ( ( ( ( ( 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 } ) )
106 91 105 eqtrd
 |-  ( ( ( ( ( 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 } ) )
107 86 106 breqtrrd
 |-  ( ( ( ( ( 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 } ) ) )
108 107 ralrimiva
 |-  ( ( ( ( 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 } ) ) )
109 id
 |-  ( c = d -> c = d )
110 imainrect
 |-  ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " c ) = ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) )
111 imaeq2
 |-  ( c = d -> ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " c ) = ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) )
112 110 111 eqtr3id
 |-  ( c = d -> ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) = ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) )
113 109 112 breq12d
 |-  ( c = d -> ( c ~<_ ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) <-> d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) ) )
114 113 cbvralvw
 |-  ( 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 ) )
115 108 114 sylib
 |-  ( ( ( ( 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 ) )
116 115 adantllr
 |-  ( ( ( ( ( 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 ) )
117 inss2
 |-  ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) C_ ( ( f \ { i } ) X. ( b \ { j } ) )
118 difss
 |-  ( b \ { j } ) C_ b
119 xpss2
 |-  ( ( b \ { j } ) C_ b -> ( ( f \ { i } ) X. ( b \ { j } ) ) C_ ( ( f \ { i } ) X. b ) )
120 118 119 ax-mp
 |-  ( ( f \ { i } ) X. ( b \ { j } ) ) C_ ( ( f \ { i } ) X. b )
121 117 120 sstri
 |-  ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) C_ ( ( f \ { i } ) X. b )
122 45 inex1
 |-  ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e. _V
123 122 elpw
 |-  ( ( 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 ) )
124 121 123 mpbir
 |-  ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e. ~P ( ( f \ { i } ) X. b )
125 simpllr
 |-  ( ( ( ( ( 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 ) ) )
126 67 adantr
 |-  ( ( i e. f /\ j e. ( g " { i } ) ) -> ( f \ { i } ) C. f )
127 126 ad2antll
 |-  ( ( ( ( ( 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 )
128 vex
 |-  f e. _V
129 128 difexi
 |-  ( f \ { i } ) e. _V
130 psseq1
 |-  ( a = ( f \ { i } ) -> ( a C. f <-> ( f \ { i } ) C. f ) )
131 xpeq1
 |-  ( a = ( f \ { i } ) -> ( a X. b ) = ( ( f \ { i } ) X. b ) )
132 131 pweqd
 |-  ( a = ( f \ { i } ) -> ~P ( a X. b ) = ~P ( ( f \ { i } ) X. b ) )
133 pweq
 |-  ( a = ( f \ { i } ) -> ~P a = ~P ( f \ { i } ) )
134 133 raleqdv
 |-  ( a = ( f \ { i } ) -> ( A. d e. ~P a d ~<_ ( c " d ) <-> A. d e. ~P ( f \ { i } ) d ~<_ ( c " d ) ) )
135 f1eq2
 |-  ( a = ( f \ { i } ) -> ( e : a -1-1-> _V <-> e : ( f \ { i } ) -1-1-> _V ) )
136 135 rexbidv
 |-  ( a = ( f \ { i } ) -> ( E. e e. ~P c e : a -1-1-> _V <-> E. e e. ~P c e : ( f \ { i } ) -1-1-> _V ) )
137 134 136 imbi12d
 |-  ( 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 ) ) )
138 132 137 raleqbidv
 |-  ( 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 ) ) )
139 130 138 imbi12d
 |-  ( 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 ) ) ) )
140 129 139 spcv
 |-  ( 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 ) ) )
141 125 127 140 sylc
 |-  ( ( ( ( ( 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 ) )
142 imaeq1
 |-  ( c = ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( c " d ) = ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) )
143 142 breq2d
 |-  ( c = ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( d ~<_ ( c " d ) <-> d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) ) )
144 143 ralbidv
 |-  ( 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 ) ) )
145 pweq
 |-  ( c = ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ~P c = ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) )
146 145 rexeqdv
 |-  ( 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 ) )
147 144 146 imbi12d
 |-  ( 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 ) ) )
148 147 rspcva
 |-  ( ( ( 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 ) )
149 124 141 148 sylancr
 |-  ( ( ( ( ( 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 ) )
150 116 149 mpd
 |-  ( ( ( ( ( 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 )
151 f1eq1
 |-  ( e = k -> ( e : ( f \ { i } ) -1-1-> _V <-> k : ( f \ { i } ) -1-1-> _V ) )
152 151 cbvrexvw
 |-  ( 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 )
153 150 152 sylib
 |-  ( ( ( ( ( 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 )
154 vex
 |-  j e. _V
155 38 154 elimasn
 |-  ( j e. ( g " { i } ) <-> <. i , j >. e. g )
156 155 biimpi
 |-  ( j e. ( g " { i } ) -> <. i , j >. e. g )
157 156 snssd
 |-  ( j e. ( g " { i } ) -> { <. i , j >. } C_ g )
158 157 ad2antlr
 |-  ( ( ( i e. f /\ j e. ( g " { i } ) ) /\ k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) ) -> { <. i , j >. } C_ g )
159 elpwi
 |-  ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> k C_ ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) )
160 inss1
 |-  ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) C_ g
161 159 160 sstrdi
 |-  ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> k C_ g )
162 161 adantl
 |-  ( ( ( i e. f /\ j e. ( g " { i } ) ) /\ k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) ) -> k C_ g )
163 158 162 unssd
 |-  ( ( ( i e. f /\ j e. ( g " { i } ) ) /\ k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) ) -> ( { <. i , j >. } u. k ) C_ g )
164 45 elpw2
 |-  ( ( { <. i , j >. } u. k ) e. ~P g <-> ( { <. i , j >. } u. k ) C_ g )
165 163 164 sylibr
 |-  ( ( ( 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 )
166 165 ad2ant2lr
 |-  ( ( ( 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 )
167 38 154 f1osn
 |-  { <. i , j >. } : { i } -1-1-onto-> { j }
168 167 a1i
 |-  ( ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) -> { <. i , j >. } : { i } -1-1-onto-> { j } )
169 f1f1orn
 |-  ( k : ( f \ { i } ) -1-1-> _V -> k : ( f \ { i } ) -1-1-onto-> ran k )
170 169 adantl
 |-  ( ( 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 )
171 disjdif
 |-  ( { i } i^i ( f \ { i } ) ) = (/)
172 171 a1i
 |-  ( ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) -> ( { i } i^i ( f \ { i } ) ) = (/) )
173 incom
 |-  ( { j } i^i ran k ) = ( ran k i^i { j } )
174 159 117 sstrdi
 |-  ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> k C_ ( ( f \ { i } ) X. ( b \ { j } ) ) )
175 rnss
 |-  ( k C_ ( ( f \ { i } ) X. ( b \ { j } ) ) -> ran k C_ ran ( ( f \ { i } ) X. ( b \ { j } ) ) )
176 rnxpss
 |-  ran ( ( f \ { i } ) X. ( b \ { j } ) ) C_ ( b \ { j } )
177 175 176 sstrdi
 |-  ( k C_ ( ( f \ { i } ) X. ( b \ { j } ) ) -> ran k C_ ( b \ { j } ) )
178 174 177 syl
 |-  ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ran k C_ ( b \ { j } ) )
179 disjdifr
 |-  ( ( b \ { j } ) i^i { j } ) = (/)
180 ssdisj
 |-  ( ( ran k C_ ( b \ { j } ) /\ ( ( b \ { j } ) i^i { j } ) = (/) ) -> ( ran k i^i { j } ) = (/) )
181 178 179 180 sylancl
 |-  ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( ran k i^i { j } ) = (/) )
182 173 181 eqtrid
 |-  ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( { j } i^i ran k ) = (/) )
183 182 adantr
 |-  ( ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) -> ( { j } i^i ran k ) = (/) )
184 f1oun
 |-  ( ( ( { <. 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 ) )
185 168 170 172 183 184 syl22anc
 |-  ( ( 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 ) )
186 185 adantl
 |-  ( ( ( 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 ) )
187 snssi
 |-  ( i e. f -> { i } C_ f )
188 187 ad2antrl
 |-  ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) -> { i } C_ f )
189 undif
 |-  ( { i } C_ f <-> ( { i } u. ( f \ { i } ) ) = f )
190 188 189 sylib
 |-  ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) -> ( { i } u. ( f \ { i } ) ) = f )
191 190 f1oeq2d
 |-  ( ( 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 ) ) )
192 191 adantr
 |-  ( ( ( 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 ) ) )
193 186 192 mpbid
 |-  ( ( ( 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 ) )
194 f1of1
 |-  ( ( { <. i , j >. } u. k ) : f -1-1-onto-> ( { j } u. ran k ) -> ( { <. i , j >. } u. k ) : f -1-1-> ( { j } u. ran k ) )
195 ssv
 |-  ( { j } u. ran k ) C_ _V
196 f1ss
 |-  ( ( ( { <. 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 )
197 194 195 196 sylancl
 |-  ( ( { <. i , j >. } u. k ) : f -1-1-onto-> ( { j } u. ran k ) -> ( { <. i , j >. } u. k ) : f -1-1-> _V )
198 193 197 syl
 |-  ( ( ( 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 )
199 f1eq1
 |-  ( e = ( { <. i , j >. } u. k ) -> ( e : f -1-1-> _V <-> ( { <. i , j >. } u. k ) : f -1-1-> _V ) )
200 199 rspcev
 |-  ( ( ( { <. 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 )
201 166 198 200 syl2anc
 |-  ( ( ( 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 )
202 201 rexlimdvaa
 |-  ( ( 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 ) )
203 202 ex
 |-  ( 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 ) ) )
204 203 adantr
 |-  ( ( 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 ) ) )
205 204 ad2antlr
 |-  ( ( ( ( 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 ) ) )
206 205 impr
 |-  ( ( ( ( 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 ) )
207 206 adantllr
 |-  ( ( ( ( ( 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 ) )
208 153 207 mpd
 |-  ( ( ( ( ( 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 )
209 208 expr
 |-  ( ( ( ( ( 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 ) )
210 209 expd
 |-  ( ( ( ( ( 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 ) ) )
211 210 impr
 |-  ( ( ( ( ( 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 ) )
212 211 exlimdv
 |-  ( ( ( ( ( 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 ) )
213 56 212 mpd
 |-  ( ( ( ( ( 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 )
214 213 expr
 |-  ( ( ( ( ( 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 ) )
215 214 exlimdv
 |-  ( ( ( ( ( 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 ) )
216 32 215 syl5bi
 |-  ( ( ( ( ( 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 ) )
217 31 216 pm2.61dne
 |-  ( ( ( ( ( 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 )
218 exanali
 |-  ( E. h ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) <-> -. A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) )
219 simprll
 |-  ( ( ( ( ( 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 )
220 pssss
 |-  ( h C. f -> h C_ f )
221 219 220 syl
 |-  ( ( ( ( ( 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 )
222 221 sspwd
 |-  ( ( ( ( ( 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 )
223 simplrr
 |-  ( ( ( ( ( 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 ) )
224 ssralv
 |-  ( ~P h C_ ~P f -> ( A. d e. ~P f d ~<_ ( g " d ) -> A. d e. ~P h d ~<_ ( g " d ) ) )
225 222 223 224 sylc
 |-  ( ( ( ( ( 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 ) )
226 elpwi
 |-  ( d e. ~P h -> d C_ h )
227 resima2
 |-  ( d C_ h -> ( ( g |` h ) " d ) = ( g " d ) )
228 226 227 syl
 |-  ( d e. ~P h -> ( ( g |` h ) " d ) = ( g " d ) )
229 228 eqcomd
 |-  ( d e. ~P h -> ( g " d ) = ( ( g |` h ) " d ) )
230 229 breq2d
 |-  ( d e. ~P h -> ( d ~<_ ( g " d ) <-> d ~<_ ( ( g |` h ) " d ) ) )
231 230 ralbiia
 |-  ( A. d e. ~P h d ~<_ ( g " d ) <-> A. d e. ~P h d ~<_ ( ( g |` h ) " d ) )
232 225 231 sylib
 |-  ( ( ( ( ( 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 ) )
233 imaeq1
 |-  ( c = ( g |` h ) -> ( c " d ) = ( ( g |` h ) " d ) )
234 233 breq2d
 |-  ( c = ( g |` h ) -> ( d ~<_ ( c " d ) <-> d ~<_ ( ( g |` h ) " d ) ) )
235 234 ralbidv
 |-  ( c = ( g |` h ) -> ( A. d e. ~P h d ~<_ ( c " d ) <-> A. d e. ~P h d ~<_ ( ( g |` h ) " d ) ) )
236 pweq
 |-  ( c = ( g |` h ) -> ~P c = ~P ( g |` h ) )
237 236 rexeqdv
 |-  ( c = ( g |` h ) -> ( E. e e. ~P c e : h -1-1-> _V <-> E. e e. ~P ( g |` h ) e : h -1-1-> _V ) )
238 235 237 imbi12d
 |-  ( 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 ) ) )
239 simpllr
 |-  ( ( ( ( ( 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 ) ) )
240 psseq1
 |-  ( a = h -> ( a C. f <-> h C. f ) )
241 xpeq1
 |-  ( a = h -> ( a X. b ) = ( h X. b ) )
242 241 pweqd
 |-  ( a = h -> ~P ( a X. b ) = ~P ( h X. b ) )
243 pweq
 |-  ( a = h -> ~P a = ~P h )
244 243 raleqdv
 |-  ( a = h -> ( A. d e. ~P a d ~<_ ( c " d ) <-> A. d e. ~P h d ~<_ ( c " d ) ) )
245 f1eq2
 |-  ( a = h -> ( e : a -1-1-> _V <-> e : h -1-1-> _V ) )
246 245 rexbidv
 |-  ( a = h -> ( E. e e. ~P c e : a -1-1-> _V <-> E. e e. ~P c e : h -1-1-> _V ) )
247 244 246 imbi12d
 |-  ( 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 ) ) )
248 242 247 raleqbidv
 |-  ( 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 ) ) )
249 240 248 imbi12d
 |-  ( 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 ) ) ) )
250 249 spvv
 |-  ( 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 ) ) )
251 239 219 250 sylc
 |-  ( ( ( ( ( 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 ) )
252 simplrl
 |-  ( ( ( ( ( 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 ) )
253 ssres
 |-  ( g C_ ( f X. b ) -> ( g |` h ) C_ ( ( f X. b ) |` h ) )
254 df-res
 |-  ( ( f X. b ) |` h ) = ( ( f X. b ) i^i ( h X. _V ) )
255 inxp
 |-  ( ( f X. b ) i^i ( h X. _V ) ) = ( ( f i^i h ) X. ( b i^i _V ) )
256 inss2
 |-  ( f i^i h ) C_ h
257 inss1
 |-  ( b i^i _V ) C_ b
258 xpss12
 |-  ( ( ( 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 ) )
259 256 257 258 mp2an
 |-  ( ( f i^i h ) X. ( b i^i _V ) ) C_ ( h X. b )
260 255 259 eqsstri
 |-  ( ( f X. b ) i^i ( h X. _V ) ) C_ ( h X. b )
261 254 260 eqsstri
 |-  ( ( f X. b ) |` h ) C_ ( h X. b )
262 253 261 sstrdi
 |-  ( g C_ ( f X. b ) -> ( g |` h ) C_ ( h X. b ) )
263 94 262 syl
 |-  ( g e. ~P ( f X. b ) -> ( g |` h ) C_ ( h X. b ) )
264 45 resex
 |-  ( g |` h ) e. _V
265 264 elpw
 |-  ( ( g |` h ) e. ~P ( h X. b ) <-> ( g |` h ) C_ ( h X. b ) )
266 263 265 sylibr
 |-  ( g e. ~P ( f X. b ) -> ( g |` h ) e. ~P ( h X. b ) )
267 252 266 syl
 |-  ( ( ( ( ( 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 ) )
268 238 251 267 rspcdva
 |-  ( ( ( ( ( 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 ) )
269 232 268 mpd
 |-  ( ( ( ( ( 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 )
270 f1eq1
 |-  ( e = i -> ( e : h -1-1-> _V <-> i : h -1-1-> _V ) )
271 270 cbvrexvw
 |-  ( E. e e. ~P ( g |` h ) e : h -1-1-> _V <-> E. i e. ~P ( g |` h ) i : h -1-1-> _V )
272 269 271 sylib
 |-  ( ( ( ( ( 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 )
273 id
 |-  ( d = ( h u. c ) -> d = ( h u. c ) )
274 imaeq2
 |-  ( d = ( h u. c ) -> ( g " d ) = ( g " ( h u. c ) ) )
275 273 274 breq12d
 |-  ( d = ( h u. c ) -> ( d ~<_ ( g " d ) <-> ( h u. c ) ~<_ ( g " ( h u. c ) ) ) )
276 simprr
 |-  ( ( ( 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 ) )
277 276 ad2antrr
 |-  ( ( ( ( ( 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 ) )
278 220 ad2antrr
 |-  ( ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) -> h C_ f )
279 278 ad2antlr
 |-  ( ( ( ( ( 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 )
280 elpwi
 |-  ( c e. ~P ( f \ h ) -> c C_ ( f \ h ) )
281 difss
 |-  ( f \ h ) C_ f
282 280 281 sstrdi
 |-  ( c e. ~P ( f \ h ) -> c C_ f )
283 282 adantl
 |-  ( ( ( ( ( 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 )
284 279 283 unssd
 |-  ( ( ( ( ( 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 )
285 128 elpw2
 |-  ( ( h u. c ) e. ~P f <-> ( h u. c ) C_ f )
286 284 285 sylibr
 |-  ( ( ( ( ( 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 )
287 275 277 286 rspcdva
 |-  ( ( ( ( ( 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 ) ) )
288 imaundi
 |-  ( g " ( h u. c ) ) = ( ( g " h ) u. ( g " c ) )
289 undif2
 |-  ( ( g " h ) u. ( ( g " c ) \ ( g " h ) ) ) = ( ( g " h ) u. ( g " c ) )
290 288 289 eqtr4i
 |-  ( g " ( h u. c ) ) = ( ( g " h ) u. ( ( g " c ) \ ( g " h ) ) )
291 287 290 breqtrdi
 |-  ( ( ( ( ( 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. ( ( g " c ) \ ( g " h ) ) ) )
292 simp-4l
 |-  ( ( ( ( ( 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 ) ) -> f e. Fin )
293 292 279 ssfid
 |-  ( ( ( ( ( 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 e. Fin )
294 id
 |-  ( d = h -> d = h )
295 imaeq2
 |-  ( d = h -> ( g " d ) = ( g " h ) )
296 294 295 breq12d
 |-  ( d = h -> ( d ~<_ ( g " d ) <-> h ~<_ ( g " h ) ) )
297 vex
 |-  h e. _V
298 297 elpw
 |-  ( h e. ~P f <-> h C_ f )
299 279 298 sylibr
 |-  ( ( ( ( ( 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 e. ~P f )
300 296 277 299 rspcdva
 |-  ( ( ( ( ( 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 ~<_ ( g " h ) )
301 simplrr
 |-  ( ( ( ( ( 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 ~< ( g " h ) )
302 bren2
 |-  ( h ~~ ( g " h ) <-> ( h ~<_ ( g " h ) /\ -. h ~< ( g " h ) ) )
303 300 301 302 sylanbrc
 |-  ( ( ( ( ( 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 ~~ ( g " h ) )
304 303 ensymd
 |-  ( ( ( ( ( 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 ) ) -> ( g " h ) ~~ h )
305 incom
 |-  ( h i^i c ) = ( c i^i h )
306 ssdifin0
 |-  ( c C_ ( f \ h ) -> ( c i^i h ) = (/) )
307 305 306 eqtrid
 |-  ( c C_ ( f \ h ) -> ( h i^i c ) = (/) )
308 280 307 syl
 |-  ( c e. ~P ( f \ h ) -> ( h i^i c ) = (/) )
309 308 adantl
 |-  ( ( ( ( ( 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 i^i c ) = (/) )
310 disjdif
 |-  ( ( g " h ) i^i ( ( g " c ) \ ( g " h ) ) ) = (/)
311 310 a1i
 |-  ( ( ( ( ( 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 ) ) -> ( ( g " h ) i^i ( ( g " c ) \ ( g " h ) ) ) = (/) )
312 domunfican
 |-  ( ( ( h e. Fin /\ ( g " h ) ~~ h ) /\ ( ( h i^i c ) = (/) /\ ( ( g " h ) i^i ( ( g " c ) \ ( g " h ) ) ) = (/) ) ) -> ( ( h u. c ) ~<_ ( ( g " h ) u. ( ( g " c ) \ ( g " h ) ) ) <-> c ~<_ ( ( g " c ) \ ( g " h ) ) ) )
313 293 304 309 311 312 syl22anc
 |-  ( ( ( ( ( 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. ( ( g " c ) \ ( g " h ) ) ) <-> c ~<_ ( ( g " c ) \ ( g " h ) ) ) )
314 291 313 mpbid
 |-  ( ( ( ( ( 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 ~<_ ( ( g " c ) \ ( g " h ) ) )
315 101 difeq1d
 |-  ( g e. ~P ( f X. b ) -> ( ( ( g " c ) i^i b ) \ ( g " h ) ) = ( ( g " c ) \ ( g " h ) ) )
316 315 ad2antrl
 |-  ( ( ( 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 ) \ ( g " h ) ) = ( ( g " c ) \ ( g " h ) ) )
317 316 ad2antrr
 |-  ( ( ( ( ( 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 ) ) -> ( ( ( g " c ) i^i b ) \ ( g " h ) ) = ( ( g " c ) \ ( g " h ) ) )
318 314 317 breqtrrd
 |-  ( ( ( ( ( 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 ~<_ ( ( ( g " c ) i^i b ) \ ( g " h ) ) )
319 df-ss
 |-  ( c C_ ( f \ h ) <-> ( c i^i ( f \ h ) ) = c )
320 280 319 sylib
 |-  ( c e. ~P ( f \ h ) -> ( c i^i ( f \ h ) ) = c )
321 320 imaeq2d
 |-  ( c e. ~P ( f \ h ) -> ( g " ( c i^i ( f \ h ) ) ) = ( g " c ) )
322 321 ineq1d
 |-  ( c e. ~P ( f \ h ) -> ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) = ( ( g " c ) i^i ( b \ ( g " h ) ) ) )
323 indif2
 |-  ( ( g " c ) i^i ( b \ ( g " h ) ) ) = ( ( ( g " c ) i^i b ) \ ( g " h ) )
324 322 323 eqtrdi
 |-  ( c e. ~P ( f \ h ) -> ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) = ( ( ( g " c ) i^i b ) \ ( g " h ) ) )
325 324 adantl
 |-  ( ( ( ( ( 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 ) ) -> ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) = ( ( ( g " c ) i^i b ) \ ( g " h ) ) )
326 318 325 breqtrrd
 |-  ( ( ( ( ( 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 ~<_ ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) )
327 326 ralrimiva
 |-  ( ( ( ( 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 ) ) ) -> A. c e. ~P ( f \ h ) c ~<_ ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) )
328 imainrect
 |-  ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " c ) = ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) )
329 imaeq2
 |-  ( c = d -> ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " c ) = ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
330 328 329 eqtr3id
 |-  ( c = d -> ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) = ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
331 109 330 breq12d
 |-  ( c = d -> ( c ~<_ ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) <-> d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) ) )
332 331 cbvralvw
 |-  ( A. c e. ~P ( f \ h ) c ~<_ ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) <-> A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
333 327 332 sylib
 |-  ( ( ( ( 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 ) ) ) -> A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
334 333 adantllr
 |-  ( ( ( ( ( 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 \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
335 inss2
 |-  ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) C_ ( ( f \ h ) X. ( b \ ( g " h ) ) )
336 difss
 |-  ( b \ ( g " h ) ) C_ b
337 xpss2
 |-  ( ( b \ ( g " h ) ) C_ b -> ( ( f \ h ) X. ( b \ ( g " h ) ) ) C_ ( ( f \ h ) X. b ) )
338 336 337 ax-mp
 |-  ( ( f \ h ) X. ( b \ ( g " h ) ) ) C_ ( ( f \ h ) X. b )
339 335 338 sstri
 |-  ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) C_ ( ( f \ h ) X. b )
340 45 inex1
 |-  ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e. _V
341 340 elpw
 |-  ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e. ~P ( ( f \ h ) X. b ) <-> ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) C_ ( ( f \ h ) X. b ) )
342 339 341 mpbir
 |-  ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e. ~P ( ( f \ h ) X. b )
343 incom
 |-  ( f i^i h ) = ( h i^i f )
344 df-ss
 |-  ( h C_ f <-> ( h i^i f ) = h )
345 220 344 sylib
 |-  ( h C. f -> ( h i^i f ) = h )
346 343 345 eqtrid
 |-  ( h C. f -> ( f i^i h ) = h )
347 346 neeq1d
 |-  ( h C. f -> ( ( f i^i h ) =/= (/) <-> h =/= (/) ) )
348 347 biimpar
 |-  ( ( h C. f /\ h =/= (/) ) -> ( f i^i h ) =/= (/) )
349 disj4
 |-  ( ( f i^i h ) = (/) <-> -. ( f \ h ) C. f )
350 349 bicomi
 |-  ( -. ( f \ h ) C. f <-> ( f i^i h ) = (/) )
351 350 necon1abii
 |-  ( ( f i^i h ) =/= (/) <-> ( f \ h ) C. f )
352 348 351 sylib
 |-  ( ( h C. f /\ h =/= (/) ) -> ( f \ h ) C. f )
353 352 ad2antrl
 |-  ( ( ( ( ( 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 ) ) ) -> ( f \ h ) C. f )
354 128 difexi
 |-  ( f \ h ) e. _V
355 psseq1
 |-  ( a = ( f \ h ) -> ( a C. f <-> ( f \ h ) C. f ) )
356 xpeq1
 |-  ( a = ( f \ h ) -> ( a X. b ) = ( ( f \ h ) X. b ) )
357 356 pweqd
 |-  ( a = ( f \ h ) -> ~P ( a X. b ) = ~P ( ( f \ h ) X. b ) )
358 pweq
 |-  ( a = ( f \ h ) -> ~P a = ~P ( f \ h ) )
359 358 raleqdv
 |-  ( a = ( f \ h ) -> ( A. d e. ~P a d ~<_ ( c " d ) <-> A. d e. ~P ( f \ h ) d ~<_ ( c " d ) ) )
360 f1eq2
 |-  ( a = ( f \ h ) -> ( e : a -1-1-> _V <-> e : ( f \ h ) -1-1-> _V ) )
361 360 rexbidv
 |-  ( a = ( f \ h ) -> ( E. e e. ~P c e : a -1-1-> _V <-> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) )
362 359 361 imbi12d
 |-  ( a = ( f \ h ) -> ( ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) ) )
363 357 362 raleqbidv
 |-  ( a = ( f \ 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 ( ( f \ h ) X. b ) ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) ) )
364 355 363 imbi12d
 |-  ( a = ( f \ 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 ) ) <-> ( ( f \ h ) C. f -> A. c e. ~P ( ( f \ h ) X. b ) ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) ) ) )
365 354 364 spcv
 |-  ( 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 \ h ) C. f -> A. c e. ~P ( ( f \ h ) X. b ) ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) ) )
366 239 353 365 sylc
 |-  ( ( ( ( ( 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 ( ( f \ h ) X. b ) ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) )
367 imaeq1
 |-  ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ( c " d ) = ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
368 367 breq2d
 |-  ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ( d ~<_ ( c " d ) <-> d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) ) )
369 368 ralbidv
 |-  ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) <-> A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) ) )
370 pweq
 |-  ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ~P c = ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) )
371 370 rexeqdv
 |-  ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ( E. e e. ~P c e : ( f \ h ) -1-1-> _V <-> E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V ) )
372 369 371 imbi12d
 |-  ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ( ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) <-> ( A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) -> E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V ) ) )
373 372 rspcva
 |-  ( ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e. ~P ( ( f \ h ) X. b ) /\ A. c e. ~P ( ( f \ h ) X. b ) ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) ) -> ( A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) -> E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V ) )
374 342 366 373 sylancr
 |-  ( ( ( ( ( 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 \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) -> E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V ) )
375 334 374 mpd
 |-  ( ( ( ( ( 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 i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V )
376 f1eq1
 |-  ( e = j -> ( e : ( f \ h ) -1-1-> _V <-> j : ( f \ h ) -1-1-> _V ) )
377 376 cbvrexvw
 |-  ( E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V <-> E. j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) j : ( f \ h ) -1-1-> _V )
378 375 377 sylib
 |-  ( ( ( ( ( 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. j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) j : ( f \ h ) -1-1-> _V )
379 elpwi
 |-  ( i e. ~P ( g |` h ) -> i C_ ( g |` h ) )
380 resss
 |-  ( g |` h ) C_ g
381 379 380 sstrdi
 |-  ( i e. ~P ( g |` h ) -> i C_ g )
382 381 adantr
 |-  ( ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) -> i C_ g )
383 382 ad2antlr
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> i C_ g )
384 elpwi
 |-  ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> j C_ ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) )
385 inss1
 |-  ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) C_ g
386 384 385 sstrdi
 |-  ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> j C_ g )
387 386 ad2antrl
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> j C_ g )
388 383 387 unssd
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) C_ g )
389 45 elpw2
 |-  ( ( i u. j ) e. ~P g <-> ( i u. j ) C_ g )
390 388 389 sylibr
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) e. ~P g )
391 f1f1orn
 |-  ( i : h -1-1-> _V -> i : h -1-1-onto-> ran i )
392 391 adantl
 |-  ( ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) -> i : h -1-1-onto-> ran i )
393 392 ad2antlr
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> i : h -1-1-onto-> ran i )
394 f1f1orn
 |-  ( j : ( f \ h ) -1-1-> _V -> j : ( f \ h ) -1-1-onto-> ran j )
395 394 ad2antll
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> j : ( f \ h ) -1-1-onto-> ran j )
396 disjdif
 |-  ( h i^i ( f \ h ) ) = (/)
397 396 a1i
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( h i^i ( f \ h ) ) = (/) )
398 rnss
 |-  ( i C_ ( g |` h ) -> ran i C_ ran ( g |` h ) )
399 379 398 syl
 |-  ( i e. ~P ( g |` h ) -> ran i C_ ran ( g |` h ) )
400 df-ima
 |-  ( g " h ) = ran ( g |` h )
401 399 400 sseqtrrdi
 |-  ( i e. ~P ( g |` h ) -> ran i C_ ( g " h ) )
402 401 adantr
 |-  ( ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) -> ran i C_ ( g " h ) )
403 402 ad2antlr
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ran i C_ ( g " h ) )
404 incom
 |-  ( ( g " h ) i^i ran j ) = ( ran j i^i ( g " h ) )
405 384 335 sstrdi
 |-  ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> j C_ ( ( f \ h ) X. ( b \ ( g " h ) ) ) )
406 rnss
 |-  ( j C_ ( ( f \ h ) X. ( b \ ( g " h ) ) ) -> ran j C_ ran ( ( f \ h ) X. ( b \ ( g " h ) ) ) )
407 405 406 syl
 |-  ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ran j C_ ran ( ( f \ h ) X. ( b \ ( g " h ) ) ) )
408 rnxpss
 |-  ran ( ( f \ h ) X. ( b \ ( g " h ) ) ) C_ ( b \ ( g " h ) )
409 407 408 sstrdi
 |-  ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ran j C_ ( b \ ( g " h ) ) )
410 409 ad2antrl
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ran j C_ ( b \ ( g " h ) ) )
411 disjdifr
 |-  ( ( b \ ( g " h ) ) i^i ( g " h ) ) = (/)
412 ssdisj
 |-  ( ( ran j C_ ( b \ ( g " h ) ) /\ ( ( b \ ( g " h ) ) i^i ( g " h ) ) = (/) ) -> ( ran j i^i ( g " h ) ) = (/) )
413 410 411 412 sylancl
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( ran j i^i ( g " h ) ) = (/) )
414 404 413 eqtrid
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( ( g " h ) i^i ran j ) = (/) )
415 ssdisj
 |-  ( ( ran i C_ ( g " h ) /\ ( ( g " h ) i^i ran j ) = (/) ) -> ( ran i i^i ran j ) = (/) )
416 403 414 415 syl2anc
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( ran i i^i ran j ) = (/) )
417 f1oun
 |-  ( ( ( i : h -1-1-onto-> ran i /\ j : ( f \ h ) -1-1-onto-> ran j ) /\ ( ( h i^i ( f \ h ) ) = (/) /\ ( ran i i^i ran j ) = (/) ) ) -> ( i u. j ) : ( h u. ( f \ h ) ) -1-1-onto-> ( ran i u. ran j ) )
418 393 395 397 416 417 syl22anc
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) : ( h u. ( f \ h ) ) -1-1-onto-> ( ran i u. ran j ) )
419 undif
 |-  ( h C_ f <-> ( h u. ( f \ h ) ) = f )
420 419 biimpi
 |-  ( h C_ f -> ( h u. ( f \ h ) ) = f )
421 420 adantl
 |-  ( ( g e. ~P ( f X. b ) /\ h C_ f ) -> ( h u. ( f \ h ) ) = f )
422 421 ad2antrr
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( h u. ( f \ h ) ) = f )
423 422 f1oeq2d
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( ( i u. j ) : ( h u. ( f \ h ) ) -1-1-onto-> ( ran i u. ran j ) <-> ( i u. j ) : f -1-1-onto-> ( ran i u. ran j ) ) )
424 418 423 mpbid
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) : f -1-1-onto-> ( ran i u. ran j ) )
425 f1of1
 |-  ( ( i u. j ) : f -1-1-onto-> ( ran i u. ran j ) -> ( i u. j ) : f -1-1-> ( ran i u. ran j ) )
426 424 425 syl
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) : f -1-1-> ( ran i u. ran j ) )
427 ssv
 |-  ( ran i u. ran j ) C_ _V
428 f1ss
 |-  ( ( ( i u. j ) : f -1-1-> ( ran i u. ran j ) /\ ( ran i u. ran j ) C_ _V ) -> ( i u. j ) : f -1-1-> _V )
429 426 427 428 sylancl
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) : f -1-1-> _V )
430 f1eq1
 |-  ( e = ( i u. j ) -> ( e : f -1-1-> _V <-> ( i u. j ) : f -1-1-> _V ) )
431 430 rspcev
 |-  ( ( ( i u. j ) e. ~P g /\ ( i u. j ) : f -1-1-> _V ) -> E. e e. ~P g e : f -1-1-> _V )
432 390 429 431 syl2anc
 |-  ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> E. e e. ~P g e : f -1-1-> _V )
433 432 rexlimdvaa
 |-  ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g |` h ) /\ i : h -1-1-> _V ) ) -> ( E. j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) j : ( f \ h ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) )
434 433 rexlimdvaa
 |-  ( ( g e. ~P ( f X. b ) /\ h C_ f ) -> ( E. i e. ~P ( g |` h ) i : h -1-1-> _V -> ( E. j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) j : ( f \ h ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) ) )
435 252 221 434 syl2anc
 |-  ( ( ( ( ( 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 -> ( E. j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) j : ( f \ h ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) ) )
436 272 378 435 mp2d
 |-  ( ( ( ( ( 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 e : f -1-1-> _V )
437 436 ex
 |-  ( ( ( ( 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 e : f -1-1-> _V ) )
438 437 exlimdv
 |-  ( ( ( ( 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 ) ) ) -> ( E. h ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) -> E. e e. ~P g e : f -1-1-> _V ) )
439 438 imp
 |-  ( ( ( ( ( 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 ) ) ) /\ E. h ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> E. e e. ~P g e : f -1-1-> _V )
440 218 439 sylan2br
 |-  ( ( ( ( ( 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 )
441 217 440 pm2.61dan
 |-  ( ( ( ( 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 ) ) ) -> E. e e. ~P g e : f -1-1-> _V )
442 441 exp32
 |-  ( ( ( 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 ) -> E. e e. ~P g e : f -1-1-> _V ) ) )
443 442 ralrimiv
 |-  ( ( ( 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 ) ) ) -> A. g e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( g " d ) -> E. e e. ~P g e : f -1-1-> _V ) )
444 imaeq1
 |-  ( g = c -> ( g " d ) = ( c " d ) )
445 444 breq2d
 |-  ( g = c -> ( d ~<_ ( g " d ) <-> d ~<_ ( c " d ) ) )
446 445 ralbidv
 |-  ( g = c -> ( A. d e. ~P f d ~<_ ( g " d ) <-> A. d e. ~P f d ~<_ ( c " d ) ) )
447 pweq
 |-  ( g = c -> ~P g = ~P c )
448 447 rexeqdv
 |-  ( g = c -> ( E. e e. ~P g e : f -1-1-> _V <-> E. e e. ~P c e : f -1-1-> _V ) )
449 446 448 imbi12d
 |-  ( g = c -> ( ( A. d e. ~P f d ~<_ ( g " d ) -> E. e e. ~P g e : f -1-1-> _V ) <-> ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) ) )
450 449 cbvralvw
 |-  ( A. g e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( g " d ) -> E. e e. ~P g e : f -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 ) )
451 443 450 sylib
 |-  ( ( ( 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 ) ) ) -> 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 ) )
452 451 exp31
 |-  ( 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 ) ) -> 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 ) ) ) )
453 452 a2d
 |-  ( 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 ) ) ) -> ( 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 ) ) ) )
454 22 453 syl5bi
 |-  ( f e. Fin -> ( 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. c e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) ) ) )
455 9 18 454 findcard3
 |-  ( 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 ) ) )