Step |
Hyp |
Ref |
Expression |
1 |
|
foelrn |
|- ( ( F : A -onto-> B /\ x e. B ) -> E. y e. A x = ( F ` y ) ) |
2 |
1
|
ralrimiva |
|- ( F : A -onto-> B -> A. x e. B E. y e. A x = ( F ` y ) ) |
3 |
|
fveq2 |
|- ( y = ( f ` x ) -> ( F ` y ) = ( F ` ( f ` x ) ) ) |
4 |
3
|
eqeq2d |
|- ( y = ( f ` x ) -> ( x = ( F ` y ) <-> x = ( F ` ( f ` x ) ) ) ) |
5 |
4
|
acni3 |
|- ( ( A e. AC_ B /\ A. x e. B E. y e. A x = ( F ` y ) ) -> E. f ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) |
6 |
2 5
|
sylan2 |
|- ( ( A e. AC_ B /\ F : A -onto-> B ) -> E. f ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) |
7 |
|
simpll |
|- ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> A e. AC_ B ) |
8 |
|
acnrcl |
|- ( A e. AC_ B -> B e. _V ) |
9 |
7 8
|
syl |
|- ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> B e. _V ) |
10 |
|
simprl |
|- ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> f : B --> A ) |
11 |
|
fveq2 |
|- ( ( f ` y ) = ( f ` z ) -> ( F ` ( f ` y ) ) = ( F ` ( f ` z ) ) ) |
12 |
|
simprr |
|- ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> A. x e. B x = ( F ` ( f ` x ) ) ) |
13 |
|
id |
|- ( x = y -> x = y ) |
14 |
|
2fveq3 |
|- ( x = y -> ( F ` ( f ` x ) ) = ( F ` ( f ` y ) ) ) |
15 |
13 14
|
eqeq12d |
|- ( x = y -> ( x = ( F ` ( f ` x ) ) <-> y = ( F ` ( f ` y ) ) ) ) |
16 |
15
|
rspccva |
|- ( ( A. x e. B x = ( F ` ( f ` x ) ) /\ y e. B ) -> y = ( F ` ( f ` y ) ) ) |
17 |
|
id |
|- ( x = z -> x = z ) |
18 |
|
2fveq3 |
|- ( x = z -> ( F ` ( f ` x ) ) = ( F ` ( f ` z ) ) ) |
19 |
17 18
|
eqeq12d |
|- ( x = z -> ( x = ( F ` ( f ` x ) ) <-> z = ( F ` ( f ` z ) ) ) ) |
20 |
19
|
rspccva |
|- ( ( A. x e. B x = ( F ` ( f ` x ) ) /\ z e. B ) -> z = ( F ` ( f ` z ) ) ) |
21 |
16 20
|
eqeqan12d |
|- ( ( ( A. x e. B x = ( F ` ( f ` x ) ) /\ y e. B ) /\ ( A. x e. B x = ( F ` ( f ` x ) ) /\ z e. B ) ) -> ( y = z <-> ( F ` ( f ` y ) ) = ( F ` ( f ` z ) ) ) ) |
22 |
21
|
anandis |
|- ( ( A. x e. B x = ( F ` ( f ` x ) ) /\ ( y e. B /\ z e. B ) ) -> ( y = z <-> ( F ` ( f ` y ) ) = ( F ` ( f ` z ) ) ) ) |
23 |
12 22
|
sylan |
|- ( ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) /\ ( y e. B /\ z e. B ) ) -> ( y = z <-> ( F ` ( f ` y ) ) = ( F ` ( f ` z ) ) ) ) |
24 |
11 23
|
syl5ibr |
|- ( ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) /\ ( y e. B /\ z e. B ) ) -> ( ( f ` y ) = ( f ` z ) -> y = z ) ) |
25 |
24
|
ralrimivva |
|- ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> A. y e. B A. z e. B ( ( f ` y ) = ( f ` z ) -> y = z ) ) |
26 |
|
dff13 |
|- ( f : B -1-1-> A <-> ( f : B --> A /\ A. y e. B A. z e. B ( ( f ` y ) = ( f ` z ) -> y = z ) ) ) |
27 |
10 25 26
|
sylanbrc |
|- ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> f : B -1-1-> A ) |
28 |
|
f1dom2g |
|- ( ( B e. _V /\ A e. AC_ B /\ f : B -1-1-> A ) -> B ~<_ A ) |
29 |
9 7 27 28
|
syl3anc |
|- ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> B ~<_ A ) |
30 |
6 29
|
exlimddv |
|- ( ( A e. AC_ B /\ F : A -onto-> B ) -> B ~<_ A ) |
31 |
30
|
ex |
|- ( A e. AC_ B -> ( F : A -onto-> B -> B ~<_ A ) ) |