Metamath Proof Explorer

Theorem exfo

Description: A relation equivalent to the existence of an onto mapping. The right-hand f is not necessarily a function. (Contributed by NM, 20-Mar-2007)

Ref Expression
Assertion exfo 
|- ( E. f f : A -onto-> B <-> E. f ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) )

Proof

Step Hyp Ref Expression
1 dffo4 
 |-  ( f : A -onto-> B <-> ( f : A --> B /\ A. x e. B E. y e. A y f x ) )
2 dff4 
 |-  ( f : A --> B <-> ( f C_ ( A X. B ) /\ A. x e. A E! y e. B x f y ) )
3 2 simprbi 
 |-  ( f : A --> B -> A. x e. A E! y e. B x f y )
4 3 anim1i 
 |-  ( ( f : A --> B /\ A. x e. B E. y e. A y f x ) -> ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) )
5 1 4 sylbi 
 |-  ( f : A -onto-> B -> ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) )
6 5 eximi 
 |-  ( E. f f : A -onto-> B -> E. f ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) )
7 brinxp 
 |-  ( ( x e. A /\ y e. B ) -> ( x f y <-> x ( f i^i ( A X. B ) ) y ) )
8 7 reubidva 
 |-  ( x e. A -> ( E! y e. B x f y <-> E! y e. B x ( f i^i ( A X. B ) ) y ) )
9 8 biimpd 
 |-  ( x e. A -> ( E! y e. B x f y -> E! y e. B x ( f i^i ( A X. B ) ) y ) )
10 9 ralimia 
 |-  ( A. x e. A E! y e. B x f y -> A. x e. A E! y e. B x ( f i^i ( A X. B ) ) y )
11 inss2 
 |-  ( f i^i ( A X. B ) ) C_ ( A X. B )
12 10 11 jctil 
 |-  ( A. x e. A E! y e. B x f y -> ( ( f i^i ( A X. B ) ) C_ ( A X. B ) /\ A. x e. A E! y e. B x ( f i^i ( A X. B ) ) y ) )
13 dff4 
 |-  ( ( f i^i ( A X. B ) ) : A --> B <-> ( ( f i^i ( A X. B ) ) C_ ( A X. B ) /\ A. x e. A E! y e. B x ( f i^i ( A X. B ) ) y ) )
14 12 13 sylibr 
 |-  ( A. x e. A E! y e. B x f y -> ( f i^i ( A X. B ) ) : A --> B )
15 rninxp 
 |-  ( ran ( f i^i ( A X. B ) ) = B <-> A. x e. B E. y e. A y f x )
16 15 biimpri 
 |-  ( A. x e. B E. y e. A y f x -> ran ( f i^i ( A X. B ) ) = B )
17 14 16 anim12i 
 |-  ( ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) -> ( ( f i^i ( A X. B ) ) : A --> B /\ ran ( f i^i ( A X. B ) ) = B ) )
18 dffo2 
 |-  ( ( f i^i ( A X. B ) ) : A -onto-> B <-> ( ( f i^i ( A X. B ) ) : A --> B /\ ran ( f i^i ( A X. B ) ) = B ) )
19 17 18 sylibr 
 |-  ( ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) -> ( f i^i ( A X. B ) ) : A -onto-> B )
20 vex 
 |-  f e. _V
21 20 inex1 
 |-  ( f i^i ( A X. B ) ) e. _V
22 foeq1 
 |-  ( g = ( f i^i ( A X. B ) ) -> ( g : A -onto-> B <-> ( f i^i ( A X. B ) ) : A -onto-> B ) )
23 21 22 spcev 
 |-  ( ( f i^i ( A X. B ) ) : A -onto-> B -> E. g g : A -onto-> B )
24 19 23 syl 
 |-  ( ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) -> E. g g : A -onto-> B )
25 24 exlimiv 
 |-  ( E. f ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) -> E. g g : A -onto-> B )
26 foeq1 
 |-  ( g = f -> ( g : A -onto-> B <-> f : A -onto-> B ) )
27 26 cbvexvw 
 |-  ( E. g g : A -onto-> B <-> E. f f : A -onto-> B )
28 25 27 sylib 
 |-  ( E. f ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) -> E. f f : A -onto-> B )
29 6 28 impbii 
 |-  ( E. f f : A -onto-> B <-> E. f ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) )