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 vsnex 
 |-  { 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 dfss2 
 |-  ( 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 dfss2 
 |-  ( ( 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 biimtrid 
 |-  ( ( ( ( ( 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 dfss2 
 |-  ( 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 dfss2 
 |-  ( 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 biimtrid 
 |-  ( 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 ) ) )