Step |
Hyp |
Ref |
Expression |
1 |
|
foima |
|- ( F : A -onto-> B -> ( F " A ) = B ) |
2 |
1
|
adantl |
|- ( ( A e. Fin /\ F : A -onto-> B ) -> ( F " A ) = B ) |
3 |
|
imaeq2 |
|- ( x = (/) -> ( F " x ) = ( F " (/) ) ) |
4 |
|
ima0 |
|- ( F " (/) ) = (/) |
5 |
3 4
|
eqtrdi |
|- ( x = (/) -> ( F " x ) = (/) ) |
6 |
|
id |
|- ( x = (/) -> x = (/) ) |
7 |
5 6
|
breq12d |
|- ( x = (/) -> ( ( F " x ) ~<_ x <-> (/) ~<_ (/) ) ) |
8 |
7
|
imbi2d |
|- ( x = (/) -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> (/) ~<_ (/) ) ) ) |
9 |
|
imaeq2 |
|- ( x = y -> ( F " x ) = ( F " y ) ) |
10 |
|
id |
|- ( x = y -> x = y ) |
11 |
9 10
|
breq12d |
|- ( x = y -> ( ( F " x ) ~<_ x <-> ( F " y ) ~<_ y ) ) |
12 |
11
|
imbi2d |
|- ( x = y -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> ( F " y ) ~<_ y ) ) ) |
13 |
|
imaeq2 |
|- ( x = ( y u. { z } ) -> ( F " x ) = ( F " ( y u. { z } ) ) ) |
14 |
|
id |
|- ( x = ( y u. { z } ) -> x = ( y u. { z } ) ) |
15 |
13 14
|
breq12d |
|- ( x = ( y u. { z } ) -> ( ( F " x ) ~<_ x <-> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) |
16 |
15
|
imbi2d |
|- ( x = ( y u. { z } ) -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) ) |
17 |
|
imaeq2 |
|- ( x = A -> ( F " x ) = ( F " A ) ) |
18 |
|
id |
|- ( x = A -> x = A ) |
19 |
17 18
|
breq12d |
|- ( x = A -> ( ( F " x ) ~<_ x <-> ( F " A ) ~<_ A ) ) |
20 |
19
|
imbi2d |
|- ( x = A -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> ( F " A ) ~<_ A ) ) ) |
21 |
|
0ex |
|- (/) e. _V |
22 |
21
|
0dom |
|- (/) ~<_ (/) |
23 |
22
|
a1i |
|- ( F Fn A -> (/) ~<_ (/) ) |
24 |
|
fnfun |
|- ( F Fn A -> Fun F ) |
25 |
24
|
ad2antrl |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> Fun F ) |
26 |
|
funressn |
|- ( Fun F -> ( F |` { z } ) C_ { <. z , ( F ` z ) >. } ) |
27 |
|
rnss |
|- ( ( F |` { z } ) C_ { <. z , ( F ` z ) >. } -> ran ( F |` { z } ) C_ ran { <. z , ( F ` z ) >. } ) |
28 |
25 26 27
|
3syl |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ran ( F |` { z } ) C_ ran { <. z , ( F ` z ) >. } ) |
29 |
|
df-ima |
|- ( F " { z } ) = ran ( F |` { z } ) |
30 |
|
vex |
|- z e. _V |
31 |
30
|
rnsnop |
|- ran { <. z , ( F ` z ) >. } = { ( F ` z ) } |
32 |
31
|
eqcomi |
|- { ( F ` z ) } = ran { <. z , ( F ` z ) >. } |
33 |
28 29 32
|
3sstr4g |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) C_ { ( F ` z ) } ) |
34 |
|
snex |
|- { ( F ` z ) } e. _V |
35 |
|
ssexg |
|- ( ( ( F " { z } ) C_ { ( F ` z ) } /\ { ( F ` z ) } e. _V ) -> ( F " { z } ) e. _V ) |
36 |
33 34 35
|
sylancl |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) e. _V ) |
37 |
|
fvi |
|- ( ( F " { z } ) e. _V -> ( _I ` ( F " { z } ) ) = ( F " { z } ) ) |
38 |
36 37
|
syl |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( _I ` ( F " { z } ) ) = ( F " { z } ) ) |
39 |
38
|
uneq2d |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) = ( ( F " y ) u. ( F " { z } ) ) ) |
40 |
|
imaundi |
|- ( F " ( y u. { z } ) ) = ( ( F " y ) u. ( F " { z } ) ) |
41 |
39 40
|
eqtr4di |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) = ( F " ( y u. { z } ) ) ) |
42 |
|
simprr |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " y ) ~<_ y ) |
43 |
|
ssdomg |
|- ( { ( F ` z ) } e. _V -> ( ( F " { z } ) C_ { ( F ` z ) } -> ( F " { z } ) ~<_ { ( F ` z ) } ) ) |
44 |
34 33 43
|
mpsyl |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) ~<_ { ( F ` z ) } ) |
45 |
|
fvex |
|- ( F ` z ) e. _V |
46 |
45
|
ensn1 |
|- { ( F ` z ) } ~~ 1o |
47 |
30
|
ensn1 |
|- { z } ~~ 1o |
48 |
46 47
|
entr4i |
|- { ( F ` z ) } ~~ { z } |
49 |
|
domentr |
|- ( ( ( F " { z } ) ~<_ { ( F ` z ) } /\ { ( F ` z ) } ~~ { z } ) -> ( F " { z } ) ~<_ { z } ) |
50 |
44 48 49
|
sylancl |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) ~<_ { z } ) |
51 |
38 50
|
eqbrtrd |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( _I ` ( F " { z } ) ) ~<_ { z } ) |
52 |
|
simplr |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> -. z e. y ) |
53 |
|
disjsn |
|- ( ( y i^i { z } ) = (/) <-> -. z e. y ) |
54 |
52 53
|
sylibr |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( y i^i { z } ) = (/) ) |
55 |
|
undom |
|- ( ( ( ( F " y ) ~<_ y /\ ( _I ` ( F " { z } ) ) ~<_ { z } ) /\ ( y i^i { z } ) = (/) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) ~<_ ( y u. { z } ) ) |
56 |
42 51 54 55
|
syl21anc |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) ~<_ ( y u. { z } ) ) |
57 |
41 56
|
eqbrtrrd |
|- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) |
58 |
57
|
exp32 |
|- ( ( y e. Fin /\ -. z e. y ) -> ( F Fn A -> ( ( F " y ) ~<_ y -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) ) |
59 |
58
|
a2d |
|- ( ( y e. Fin /\ -. z e. y ) -> ( ( F Fn A -> ( F " y ) ~<_ y ) -> ( F Fn A -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) ) |
60 |
8 12 16 20 23 59
|
findcard2s |
|- ( A e. Fin -> ( F Fn A -> ( F " A ) ~<_ A ) ) |
61 |
|
fofn |
|- ( F : A -onto-> B -> F Fn A ) |
62 |
60 61
|
impel |
|- ( ( A e. Fin /\ F : A -onto-> B ) -> ( F " A ) ~<_ A ) |
63 |
2 62
|
eqbrtrrd |
|- ( ( A e. Fin /\ F : A -onto-> B ) -> B ~<_ A ) |