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 ) ) ) |