Metamath Proof Explorer

Theorem dff3

Description: Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007)

Ref Expression
Assertion dff3 
|- ( F : A --> B <-> ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) )

Proof

Step Hyp Ref Expression
1 fssxp 
 |-  ( F : A --> B -> F C_ ( A X. B ) )
2 ffun 
 |-  ( F : A --> B -> Fun F )
3 fdm 
 |-  ( F : A --> B -> dom F = A )
4 3 eleq2d 
 |-  ( F : A --> B -> ( x e. dom F <-> x e. A ) )
5 4 biimpar 
 |-  ( ( F : A --> B /\ x e. A ) -> x e. dom F )
6 funfvop 
 |-  ( ( Fun F /\ x e. dom F ) -> <. x , ( F ` x ) >. e. F )
7 2 5 6 syl2an2r 
 |-  ( ( F : A --> B /\ x e. A ) -> <. x , ( F ` x ) >. e. F )
8 df-br 
 |-  ( x F ( F ` x ) <-> <. x , ( F ` x ) >. e. F )
9 7 8 sylibr 
 |-  ( ( F : A --> B /\ x e. A ) -> x F ( F ` x ) )
10 fvex 
 |-  ( F ` x ) e. _V
11 breq2 
 |-  ( y = ( F ` x ) -> ( x F y <-> x F ( F ` x ) ) )
12 10 11 spcev 
 |-  ( x F ( F ` x ) -> E. y x F y )
13 9 12 syl 
 |-  ( ( F : A --> B /\ x e. A ) -> E. y x F y )
14 funmo 
 |-  ( Fun F -> E* y x F y )
15 2 14 syl 
 |-  ( F : A --> B -> E* y x F y )
16 15 adantr 
 |-  ( ( F : A --> B /\ x e. A ) -> E* y x F y )
17 df-eu 
 |-  ( E! y x F y <-> ( E. y x F y /\ E* y x F y ) )
18 13 16 17 sylanbrc 
 |-  ( ( F : A --> B /\ x e. A ) -> E! y x F y )
19 18 ralrimiva 
 |-  ( F : A --> B -> A. x e. A E! y x F y )
20 1 19 jca 
 |-  ( F : A --> B -> ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) )
21 xpss 
 |-  ( A X. B ) C_ ( _V X. _V )
22 sstr 
 |-  ( ( F C_ ( A X. B ) /\ ( A X. B ) C_ ( _V X. _V ) ) -> F C_ ( _V X. _V ) )
23 21 22 mpan2 
 |-  ( F C_ ( A X. B ) -> F C_ ( _V X. _V ) )
24 df-rel 
 |-  ( Rel F <-> F C_ ( _V X. _V ) )
25 23 24 sylibr 
 |-  ( F C_ ( A X. B ) -> Rel F )
26 25 adantr 
 |-  ( ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) -> Rel F )
27 df-ral 
 |-  ( A. x e. A E! y x F y <-> A. x ( x e. A -> E! y x F y ) )
28 eumo 
 |-  ( E! y x F y -> E* y x F y )
29 28 imim2i 
 |-  ( ( x e. A -> E! y x F y ) -> ( x e. A -> E* y x F y ) )
30 29 adantl 
 |-  ( ( F C_ ( A X. B ) /\ ( x e. A -> E! y x F y ) ) -> ( x e. A -> E* y x F y ) )
31 df-br 
 |-  ( x F y <-> <. x , y >. e. F )
32 ssel 
 |-  ( F C_ ( A X. B ) -> ( <. x , y >. e. F -> <. x , y >. e. ( A X. B ) ) )
33 31 32 syl5bi 
 |-  ( F C_ ( A X. B ) -> ( x F y -> <. x , y >. e. ( A X. B ) ) )
34 opelxp1 
 |-  ( <. x , y >. e. ( A X. B ) -> x e. A )
35 33 34 syl6 
 |-  ( F C_ ( A X. B ) -> ( x F y -> x e. A ) )
36 35 exlimdv 
 |-  ( F C_ ( A X. B ) -> ( E. y x F y -> x e. A ) )
37 36 con3d 
 |-  ( F C_ ( A X. B ) -> ( -. x e. A -> -. E. y x F y ) )
38 nexmo 
 |-  ( -. E. y x F y -> E* y x F y )
39 37 38 syl6 
 |-  ( F C_ ( A X. B ) -> ( -. x e. A -> E* y x F y ) )
40 39 adantr 
 |-  ( ( F C_ ( A X. B ) /\ ( x e. A -> E! y x F y ) ) -> ( -. x e. A -> E* y x F y ) )
41 30 40 pm2.61d 
 |-  ( ( F C_ ( A X. B ) /\ ( x e. A -> E! y x F y ) ) -> E* y x F y )
42 41 ex 
 |-  ( F C_ ( A X. B ) -> ( ( x e. A -> E! y x F y ) -> E* y x F y ) )
43 42 alimdv 
 |-  ( F C_ ( A X. B ) -> ( A. x ( x e. A -> E! y x F y ) -> A. x E* y x F y ) )
44 27 43 syl5bi 
 |-  ( F C_ ( A X. B ) -> ( A. x e. A E! y x F y -> A. x E* y x F y ) )
45 44 imp 
 |-  ( ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) -> A. x E* y x F y )
46 dffun6 
 |-  ( Fun F <-> ( Rel F /\ A. x E* y x F y ) )
47 26 45 46 sylanbrc 
 |-  ( ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) -> Fun F )
48 dmss 
 |-  ( F C_ ( A X. B ) -> dom F C_ dom ( A X. B ) )
49 dmxpss 
 |-  dom ( A X. B ) C_ A
50 48 49 sstrdi 
 |-  ( F C_ ( A X. B ) -> dom F C_ A )
51 breq1 
 |-  ( x = z -> ( x F y <-> z F y ) )
52 51 eubidv 
 |-  ( x = z -> ( E! y x F y <-> E! y z F y ) )
53 52 rspccv 
 |-  ( A. x e. A E! y x F y -> ( z e. A -> E! y z F y ) )
54 euex 
 |-  ( E! y z F y -> E. y z F y )
55 vex 
 |-  z e. _V
56 55 eldm 
 |-  ( z e. dom F <-> E. y z F y )
57 54 56 sylibr 
 |-  ( E! y z F y -> z e. dom F )
58 53 57 syl6 
 |-  ( A. x e. A E! y x F y -> ( z e. A -> z e. dom F ) )
59 58 ssrdv 
 |-  ( A. x e. A E! y x F y -> A C_ dom F )
60 50 59 anim12i 
 |-  ( ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) -> ( dom F C_ A /\ A C_ dom F ) )
61 eqss 
 |-  ( dom F = A <-> ( dom F C_ A /\ A C_ dom F ) )
62 60 61 sylibr 
 |-  ( ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) -> dom F = A )
63 df-fn 
 |-  ( F Fn A <-> ( Fun F /\ dom F = A ) )
64 47 62 63 sylanbrc 
 |-  ( ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) -> F Fn A )
65 rnss 
 |-  ( F C_ ( A X. B ) -> ran F C_ ran ( A X. B ) )
66 rnxpss 
 |-  ran ( A X. B ) C_ B
67 65 66 sstrdi 
 |-  ( F C_ ( A X. B ) -> ran F C_ B )
68 67 adantr 
 |-  ( ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) -> ran F C_ B )
69 df-f 
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
70 64 68 69 sylanbrc 
 |-  ( ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) -> F : A --> B )
71 20 70 impbii 
 |-  ( F : A --> B <-> ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) )