Metamath Proof Explorer

Theorem fundmen

Description: A function is equinumerous to its domain. Exercise 4 of Suppes p. 98. (Contributed by NM, 28-Jul-2004) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Hypothesis fundmen.1 
|- F e. _V
Assertion fundmen 
|- ( Fun F -> dom F ~~ F )

Proof

Step Hyp Ref Expression
1 fundmen.1 
 |-  F e. _V
2 1 dmex 
 |-  dom F e. _V
3 2 a1i 
 |-  ( Fun F -> dom F e. _V )
4 1 a1i 
 |-  ( Fun F -> F e. _V )
5 funfvop 
 |-  ( ( Fun F /\ x e. dom F ) -> <. x , ( F ` x ) >. e. F )
6 5 ex 
 |-  ( Fun F -> ( x e. dom F -> <. x , ( F ` x ) >. e. F ) )
7 funrel 
 |-  ( Fun F -> Rel F )
8 elreldm 
 |-  ( ( Rel F /\ y e. F ) -> |^| |^| y e. dom F )
9 8 ex 
 |-  ( Rel F -> ( y e. F -> |^| |^| y e. dom F ) )
10 7 9 syl 
 |-  ( Fun F -> ( y e. F -> |^| |^| y e. dom F ) )
11 df-rel 
 |-  ( Rel F <-> F C_ ( _V X. _V ) )
12 7 11 sylib 
 |-  ( Fun F -> F C_ ( _V X. _V ) )
13 12 sselda 
 |-  ( ( Fun F /\ y e. F ) -> y e. ( _V X. _V ) )
14 elvv 
 |-  ( y e. ( _V X. _V ) <-> E. z E. w y = <. z , w >. )
15 13 14 sylib 
 |-  ( ( Fun F /\ y e. F ) -> E. z E. w y = <. z , w >. )
16 inteq 
 |-  ( y = <. z , w >. -> |^| y = |^| <. z , w >. )
17 16 inteqd 
 |-  ( y = <. z , w >. -> |^| |^| y = |^| |^| <. z , w >. )
18 vex 
 |-  z e. _V
19 vex 
 |-  w e. _V
20 18 19 op1stb 
 |-  |^| |^| <. z , w >. = z
21 17 20 eqtrdi 
 |-  ( y = <. z , w >. -> |^| |^| y = z )
22 eqeq1 
 |-  ( x = |^| |^| y -> ( x = z <-> |^| |^| y = z ) )
23 21 22 syl5ibr 
 |-  ( x = |^| |^| y -> ( y = <. z , w >. -> x = z ) )
24 opeq1 
 |-  ( x = z -> <. x , w >. = <. z , w >. )
25 23 24 syl6 
 |-  ( x = |^| |^| y -> ( y = <. z , w >. -> <. x , w >. = <. z , w >. ) )
26 25 imp 
 |-  ( ( x = |^| |^| y /\ y = <. z , w >. ) -> <. x , w >. = <. z , w >. )
27 eqeq2 
 |-  ( <. x , w >. = <. z , w >. -> ( y = <. x , w >. <-> y = <. z , w >. ) )
28 27 biimprcd 
 |-  ( y = <. z , w >. -> ( <. x , w >. = <. z , w >. -> y = <. x , w >. ) )
29 28 adantl 
 |-  ( ( x = |^| |^| y /\ y = <. z , w >. ) -> ( <. x , w >. = <. z , w >. -> y = <. x , w >. ) )
30 26 29 mpd 
 |-  ( ( x = |^| |^| y /\ y = <. z , w >. ) -> y = <. x , w >. )
31 30 ancoms 
 |-  ( ( y = <. z , w >. /\ x = |^| |^| y ) -> y = <. x , w >. )
32 31 adantl 
 |-  ( ( ( Fun F /\ y e. F ) /\ ( y = <. z , w >. /\ x = |^| |^| y ) ) -> y = <. x , w >. )
33 30 eleq1d 
 |-  ( ( x = |^| |^| y /\ y = <. z , w >. ) -> ( y e. F <-> <. x , w >. e. F ) )
34 33 adantl 
 |-  ( ( Fun F /\ ( x = |^| |^| y /\ y = <. z , w >. ) ) -> ( y e. F <-> <. x , w >. e. F ) )
35 funopfv 
 |-  ( Fun F -> ( <. x , w >. e. F -> ( F ` x ) = w ) )
36 35 adantr 
 |-  ( ( Fun F /\ ( x = |^| |^| y /\ y = <. z , w >. ) ) -> ( <. x , w >. e. F -> ( F ` x ) = w ) )
37 34 36 sylbid 
 |-  ( ( Fun F /\ ( x = |^| |^| y /\ y = <. z , w >. ) ) -> ( y e. F -> ( F ` x ) = w ) )
38 37 exp32 
 |-  ( Fun F -> ( x = |^| |^| y -> ( y = <. z , w >. -> ( y e. F -> ( F ` x ) = w ) ) ) )
39 38 com24 
 |-  ( Fun F -> ( y e. F -> ( y = <. z , w >. -> ( x = |^| |^| y -> ( F ` x ) = w ) ) ) )
40 39 imp43 
 |-  ( ( ( Fun F /\ y e. F ) /\ ( y = <. z , w >. /\ x = |^| |^| y ) ) -> ( F ` x ) = w )
41 40 opeq2d 
 |-  ( ( ( Fun F /\ y e. F ) /\ ( y = <. z , w >. /\ x = |^| |^| y ) ) -> <. x , ( F ` x ) >. = <. x , w >. )
42 32 41 eqtr4d 
 |-  ( ( ( Fun F /\ y e. F ) /\ ( y = <. z , w >. /\ x = |^| |^| y ) ) -> y = <. x , ( F ` x ) >. )
43 42 exp32 
 |-  ( ( Fun F /\ y e. F ) -> ( y = <. z , w >. -> ( x = |^| |^| y -> y = <. x , ( F ` x ) >. ) ) )
44 43 exlimdvv 
 |-  ( ( Fun F /\ y e. F ) -> ( E. z E. w y = <. z , w >. -> ( x = |^| |^| y -> y = <. x , ( F ` x ) >. ) ) )
45 15 44 mpd 
 |-  ( ( Fun F /\ y e. F ) -> ( x = |^| |^| y -> y = <. x , ( F ` x ) >. ) )
46 45 adantrl 
 |-  ( ( Fun F /\ ( x e. dom F /\ y e. F ) ) -> ( x = |^| |^| y -> y = <. x , ( F ` x ) >. ) )
47 inteq 
 |-  ( y = <. x , ( F ` x ) >. -> |^| y = |^| <. x , ( F ` x ) >. )
48 47 inteqd 
 |-  ( y = <. x , ( F ` x ) >. -> |^| |^| y = |^| |^| <. x , ( F ` x ) >. )
49 vex 
 |-  x e. _V
50 fvex 
 |-  ( F ` x ) e. _V
51 49 50 op1stb 
 |-  |^| |^| <. x , ( F ` x ) >. = x
52 48 51 eqtr2di 
 |-  ( y = <. x , ( F ` x ) >. -> x = |^| |^| y )
53 46 52 impbid1 
 |-  ( ( Fun F /\ ( x e. dom F /\ y e. F ) ) -> ( x = |^| |^| y <-> y = <. x , ( F ` x ) >. ) )
54 53 ex 
 |-  ( Fun F -> ( ( x e. dom F /\ y e. F ) -> ( x = |^| |^| y <-> y = <. x , ( F ` x ) >. ) ) )
55 3 4 6 10 54 en3d 
 |-  ( Fun F -> dom F ~~ F )