Metamath Proof Explorer

Theorem hashfun

Description: A finite set is a function iff it is equinumerous to its domain. (Contributed by Mario Carneiro, 26-Sep-2013) (Revised by Mario Carneiro, 12-Mar-2015)

Ref Expression
Assertion hashfun 
|- ( F e. Fin -> ( Fun F <-> ( # ` F ) = ( # ` dom F ) ) )

Proof

Step Hyp Ref Expression
1 funfn 
 |-  ( Fun F <-> F Fn dom F )
2 hashfn 
 |-  ( F Fn dom F -> ( # ` F ) = ( # ` dom F ) )
3 1 2 sylbi 
 |-  ( Fun F -> ( # ` F ) = ( # ` dom F ) )
4 dmfi 
 |-  ( F e. Fin -> dom F e. Fin )
5 hashcl 
 |-  ( dom F e. Fin -> ( # ` dom F ) e. NN0 )
6 4 5 syl 
 |-  ( F e. Fin -> ( # ` dom F ) e. NN0 )
7 6 nn0red 
 |-  ( F e. Fin -> ( # ` dom F ) e. RR )
8 7 adantr 
 |-  ( ( F e. Fin /\ -. Rel F ) -> ( # ` dom F ) e. RR )
9 df-rel 
 |-  ( Rel F <-> F C_ ( _V X. _V ) )
10 dfss3 
 |-  ( F C_ ( _V X. _V ) <-> A. x e. F x e. ( _V X. _V ) )
11 9 10 bitri 
 |-  ( Rel F <-> A. x e. F x e. ( _V X. _V ) )
12 11 notbii 
 |-  ( -. Rel F <-> -. A. x e. F x e. ( _V X. _V ) )
13 rexnal 
 |-  ( E. x e. F -. x e. ( _V X. _V ) <-> -. A. x e. F x e. ( _V X. _V ) )
14 12 13 bitr4i 
 |-  ( -. Rel F <-> E. x e. F -. x e. ( _V X. _V ) )
15 dmun 
 |-  dom ( ( F \ { x } ) u. { x } ) = ( dom ( F \ { x } ) u. dom { x } )
16 15 fveq2i 
 |-  ( # ` dom ( ( F \ { x } ) u. { x } ) ) = ( # ` ( dom ( F \ { x } ) u. dom { x } ) )
17 dmsnn0 
 |-  ( x e. ( _V X. _V ) <-> dom { x } =/= (/) )
18 17 biimpri 
 |-  ( dom { x } =/= (/) -> x e. ( _V X. _V ) )
19 18 necon1bi 
 |-  ( -. x e. ( _V X. _V ) -> dom { x } = (/) )
20 19 3ad2ant3 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> dom { x } = (/) )
21 20 uneq2d 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( dom ( F \ { x } ) u. dom { x } ) = ( dom ( F \ { x } ) u. (/) ) )
22 un0 
 |-  ( dom ( F \ { x } ) u. (/) ) = dom ( F \ { x } )
23 21 22 eqtrdi 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( dom ( F \ { x } ) u. dom { x } ) = dom ( F \ { x } ) )
24 23 fveq2d 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` ( dom ( F \ { x } ) u. dom { x } ) ) = ( # ` dom ( F \ { x } ) ) )
25 16 24 eqtrid 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` dom ( ( F \ { x } ) u. { x } ) ) = ( # ` dom ( F \ { x } ) ) )
26 diffi 
 |-  ( F e. Fin -> ( F \ { x } ) e. Fin )
27 dmfi 
 |-  ( ( F \ { x } ) e. Fin -> dom ( F \ { x } ) e. Fin )
28 26 27 syl 
 |-  ( F e. Fin -> dom ( F \ { x } ) e. Fin )
29 hashcl 
 |-  ( dom ( F \ { x } ) e. Fin -> ( # ` dom ( F \ { x } ) ) e. NN0 )
30 28 29 syl 
 |-  ( F e. Fin -> ( # ` dom ( F \ { x } ) ) e. NN0 )
31 30 nn0red 
 |-  ( F e. Fin -> ( # ` dom ( F \ { x } ) ) e. RR )
32 hashcl 
 |-  ( ( F \ { x } ) e. Fin -> ( # ` ( F \ { x } ) ) e. NN0 )
33 26 32 syl 
 |-  ( F e. Fin -> ( # ` ( F \ { x } ) ) e. NN0 )
34 33 nn0red 
 |-  ( F e. Fin -> ( # ` ( F \ { x } ) ) e. RR )
35 peano2re 
 |-  ( ( # ` ( F \ { x } ) ) e. RR -> ( ( # ` ( F \ { x } ) ) + 1 ) e. RR )
36 34 35 syl 
 |-  ( F e. Fin -> ( ( # ` ( F \ { x } ) ) + 1 ) e. RR )
37 fidomdm 
 |-  ( ( F \ { x } ) e. Fin -> dom ( F \ { x } ) ~<_ ( F \ { x } ) )
38 26 37 syl 
 |-  ( F e. Fin -> dom ( F \ { x } ) ~<_ ( F \ { x } ) )
39 hashdom 
 |-  ( ( dom ( F \ { x } ) e. Fin /\ ( F \ { x } ) e. Fin ) -> ( ( # ` dom ( F \ { x } ) ) <_ ( # ` ( F \ { x } ) ) <-> dom ( F \ { x } ) ~<_ ( F \ { x } ) ) )
40 28 26 39 syl2anc 
 |-  ( F e. Fin -> ( ( # ` dom ( F \ { x } ) ) <_ ( # ` ( F \ { x } ) ) <-> dom ( F \ { x } ) ~<_ ( F \ { x } ) ) )
41 38 40 mpbird 
 |-  ( F e. Fin -> ( # ` dom ( F \ { x } ) ) <_ ( # ` ( F \ { x } ) ) )
42 34 ltp1d 
 |-  ( F e. Fin -> ( # ` ( F \ { x } ) ) < ( ( # ` ( F \ { x } ) ) + 1 ) )
43 31 34 36 41 42 lelttrd 
 |-  ( F e. Fin -> ( # ` dom ( F \ { x } ) ) < ( ( # ` ( F \ { x } ) ) + 1 ) )
44 43 3ad2ant1 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` dom ( F \ { x } ) ) < ( ( # ` ( F \ { x } ) ) + 1 ) )
45 25 44 eqbrtrd 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` dom ( ( F \ { x } ) u. { x } ) ) < ( ( # ` ( F \ { x } ) ) + 1 ) )
46 snfi 
 |-  { x } e. Fin
47 disjdifr 
 |-  ( ( F \ { x } ) i^i { x } ) = (/)
48 hashun 
 |-  ( ( ( F \ { x } ) e. Fin /\ { x } e. Fin /\ ( ( F \ { x } ) i^i { x } ) = (/) ) -> ( # ` ( ( F \ { x } ) u. { x } ) ) = ( ( # ` ( F \ { x } ) ) + ( # ` { x } ) ) )
49 46 47 48 mp3an23 
 |-  ( ( F \ { x } ) e. Fin -> ( # ` ( ( F \ { x } ) u. { x } ) ) = ( ( # ` ( F \ { x } ) ) + ( # ` { x } ) ) )
50 26 49 syl 
 |-  ( F e. Fin -> ( # ` ( ( F \ { x } ) u. { x } ) ) = ( ( # ` ( F \ { x } ) ) + ( # ` { x } ) ) )
51 hashsng 
 |-  ( x e. _V -> ( # ` { x } ) = 1 )
52 51 elv 
 |-  ( # ` { x } ) = 1
53 52 oveq2i 
 |-  ( ( # ` ( F \ { x } ) ) + ( # ` { x } ) ) = ( ( # ` ( F \ { x } ) ) + 1 )
54 50 53 eqtr2di 
 |-  ( F e. Fin -> ( ( # ` ( F \ { x } ) ) + 1 ) = ( # ` ( ( F \ { x } ) u. { x } ) ) )
55 54 3ad2ant1 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( ( # ` ( F \ { x } ) ) + 1 ) = ( # ` ( ( F \ { x } ) u. { x } ) ) )
56 45 55 breqtrd 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` dom ( ( F \ { x } ) u. { x } ) ) < ( # ` ( ( F \ { x } ) u. { x } ) ) )
57 difsnid 
 |-  ( x e. F -> ( ( F \ { x } ) u. { x } ) = F )
58 57 dmeqd 
 |-  ( x e. F -> dom ( ( F \ { x } ) u. { x } ) = dom F )
59 58 fveq2d 
 |-  ( x e. F -> ( # ` dom ( ( F \ { x } ) u. { x } ) ) = ( # ` dom F ) )
60 59 3ad2ant2 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` dom ( ( F \ { x } ) u. { x } ) ) = ( # ` dom F ) )
61 57 fveq2d 
 |-  ( x e. F -> ( # ` ( ( F \ { x } ) u. { x } ) ) = ( # ` F ) )
62 61 3ad2ant2 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` ( ( F \ { x } ) u. { x } ) ) = ( # ` F ) )
63 56 60 62 3brtr3d 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` dom F ) < ( # ` F ) )
64 63 rexlimdv3a 
 |-  ( F e. Fin -> ( E. x e. F -. x e. ( _V X. _V ) -> ( # ` dom F ) < ( # ` F ) ) )
65 14 64 syl5bi 
 |-  ( F e. Fin -> ( -. Rel F -> ( # ` dom F ) < ( # ` F ) ) )
66 65 imp 
 |-  ( ( F e. Fin /\ -. Rel F ) -> ( # ` dom F ) < ( # ` F ) )
67 8 66 gtned 
 |-  ( ( F e. Fin /\ -. Rel F ) -> ( # ` F ) =/= ( # ` dom F ) )
68 67 ex 
 |-  ( F e. Fin -> ( -. Rel F -> ( # ` F ) =/= ( # ` dom F ) ) )
69 68 necon4bd 
 |-  ( F e. Fin -> ( ( # ` F ) = ( # ` dom F ) -> Rel F ) )
70 69 imp 
 |-  ( ( F e. Fin /\ ( # ` F ) = ( # ` dom F ) ) -> Rel F )
71 2nalexn 
 |-  ( -. A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> E. x E. y -. A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
72 df-ne 
 |-  ( y =/= z <-> -. y = z )
73 72 anbi2i 
 |-  ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) <-> ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ -. y = z ) )
74 annim 
 |-  ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ -. y = z ) <-> -. ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
75 73 74 bitri 
 |-  ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) <-> -. ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
76 75 exbii 
 |-  ( E. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) <-> E. z -. ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
77 exnal 
 |-  ( E. z -. ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> -. A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
78 76 77 bitr2i 
 |-  ( -. A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> E. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) )
79 78 2exbii 
 |-  ( E. x E. y -. A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> E. x E. y E. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) )
80 71 79 bitri 
 |-  ( -. A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> E. x E. y E. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) )
81 7 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom F ) e. RR )
82 2re 
 |-  2 e. RR
83 diffi 
 |-  ( F e. Fin -> ( F \ { <. x , y >. , <. x , z >. } ) e. Fin )
84 dmfi 
 |-  ( ( F \ { <. x , y >. , <. x , z >. } ) e. Fin -> dom ( F \ { <. x , y >. , <. x , z >. } ) e. Fin )
85 83 84 syl 
 |-  ( F e. Fin -> dom ( F \ { <. x , y >. , <. x , z >. } ) e. Fin )
86 hashcl 
 |-  ( dom ( F \ { <. x , y >. , <. x , z >. } ) e. Fin -> ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. NN0 )
87 85 86 syl 
 |-  ( F e. Fin -> ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. NN0 )
88 87 nn0red 
 |-  ( F e. Fin -> ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR )
89 88 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR )
90 readdcl 
 |-  ( ( 2 e. RR /\ ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR ) -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
91 82 89 90 sylancr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
92 hashcl 
 |-  ( F e. Fin -> ( # ` F ) e. NN0 )
93 92 nn0red 
 |-  ( F e. Fin -> ( # ` F ) e. RR )
94 93 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` F ) e. RR )
95 1re 
 |-  1 e. RR
96 readdcl 
 |-  ( ( 1 e. RR /\ ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR ) -> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
97 95 88 96 sylancr 
 |-  ( F e. Fin -> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
98 97 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
99 82 88 90 sylancr 
 |-  ( F e. Fin -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
100 99 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
101 opex 
 |-  <. x , y >. e. _V
102 opex 
 |-  <. x , z >. e. _V
103 101 102 prss 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) <-> { <. x , y >. , <. x , z >. } C_ F )
104 undif 
 |-  ( { <. x , y >. , <. x , z >. } C_ F <-> ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) = F )
105 103 104 sylbb 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) = F )
106 105 dmeqd 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> dom ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) = dom F )
107 dmun 
 |-  dom ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) = ( dom { <. x , y >. , <. x , z >. } u. dom ( F \ { <. x , y >. , <. x , z >. } ) )
108 106 107 eqtr3di 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> dom F = ( dom { <. x , y >. , <. x , z >. } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) )
109 vex 
 |-  y e. _V
110 vex 
 |-  z e. _V
111 109 110 dmprop 
 |-  dom { <. x , y >. , <. x , z >. } = { x , x }
112 dfsn2 
 |-  { x } = { x , x }
113 111 112 eqtr4i 
 |-  dom { <. x , y >. , <. x , z >. } = { x }
114 113 uneq1i 
 |-  ( dom { <. x , y >. , <. x , z >. } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) = ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) )
115 108 114 eqtrdi 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> dom F = ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) )
116 115 fveq2d 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> ( # ` dom F ) = ( # ` ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
117 116 ad2antrl 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom F ) = ( # ` ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
118 hashun2 
 |-  ( ( { x } e. Fin /\ dom ( F \ { <. x , y >. , <. x , z >. } ) e. Fin ) -> ( # ` ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( ( # ` { x } ) + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
119 46 85 118 sylancr 
 |-  ( F e. Fin -> ( # ` ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( ( # ` { x } ) + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
120 52 oveq1i 
 |-  ( ( # ` { x } ) + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) )
121 119 120 breqtrdi 
 |-  ( F e. Fin -> ( # ` ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
122 121 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
123 117 122 eqbrtrd 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom F ) <_ ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
124 1lt2 
 |-  1 < 2
125 ltadd1 
 |-  ( ( 1 e. RR /\ 2 e. RR /\ ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR ) -> ( 1 < 2 <-> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) < ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) ) )
126 95 82 88 125 mp3an12i 
 |-  ( F e. Fin -> ( 1 < 2 <-> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) < ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) ) )
127 124 126 mpbii 
 |-  ( F e. Fin -> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) < ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
128 127 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) < ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
129 81 98 100 123 128 lelttrd 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom F ) < ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
130 fidomdm 
 |-  ( ( F \ { <. x , y >. , <. x , z >. } ) e. Fin -> dom ( F \ { <. x , y >. , <. x , z >. } ) ~<_ ( F \ { <. x , y >. , <. x , z >. } ) )
131 83 130 syl 
 |-  ( F e. Fin -> dom ( F \ { <. x , y >. , <. x , z >. } ) ~<_ ( F \ { <. x , y >. , <. x , z >. } ) )
132 hashdom 
 |-  ( ( dom ( F \ { <. x , y >. , <. x , z >. } ) e. Fin /\ ( F \ { <. x , y >. , <. x , z >. } ) e. Fin ) -> ( ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) <_ ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) <-> dom ( F \ { <. x , y >. , <. x , z >. } ) ~<_ ( F \ { <. x , y >. , <. x , z >. } ) ) )
133 85 83 132 syl2anc 
 |-  ( F e. Fin -> ( ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) <_ ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) <-> dom ( F \ { <. x , y >. , <. x , z >. } ) ~<_ ( F \ { <. x , y >. , <. x , z >. } ) ) )
134 131 133 mpbird 
 |-  ( F e. Fin -> ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) <_ ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) )
135 hashcl 
 |-  ( ( F \ { <. x , y >. , <. x , z >. } ) e. Fin -> ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) e. NN0 )
136 83 135 syl 
 |-  ( F e. Fin -> ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) e. NN0 )
137 136 nn0red 
 |-  ( F e. Fin -> ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR )
138 leadd2 
 |-  ( ( ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR /\ ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR /\ 2 e. RR ) -> ( ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) <_ ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) <-> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) ) )
139 82 138 mp3an3 
 |-  ( ( ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR /\ ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR ) -> ( ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) <_ ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) <-> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) ) )
140 88 137 139 syl2anc 
 |-  ( F e. Fin -> ( ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) <_ ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) <-> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) ) )
141 134 140 mpbid 
 |-  ( F e. Fin -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
142 141 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
143 prfi 
 |-  { <. x , y >. , <. x , z >. } e. Fin
144 disjdif 
 |-  ( { <. x , y >. , <. x , z >. } i^i ( F \ { <. x , y >. , <. x , z >. } ) ) = (/)
145 hashun 
 |-  ( ( { <. x , y >. , <. x , z >. } e. Fin /\ ( F \ { <. x , y >. , <. x , z >. } ) e. Fin /\ ( { <. x , y >. , <. x , z >. } i^i ( F \ { <. x , y >. , <. x , z >. } ) ) = (/) ) -> ( # ` ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( ( # ` { <. x , y >. , <. x , z >. } ) + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
146 143 144 145 mp3an13 
 |-  ( ( F \ { <. x , y >. , <. x , z >. } ) e. Fin -> ( # ` ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( ( # ` { <. x , y >. , <. x , z >. } ) + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
147 83 146 syl 
 |-  ( F e. Fin -> ( # ` ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( ( # ` { <. x , y >. , <. x , z >. } ) + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
148 147 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( ( # ` { <. x , y >. , <. x , z >. } ) + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
149 105 fveq2d 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> ( # ` ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( # ` F ) )
150 149 ad2antrl 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( # ` F ) )
151 vex 
 |-  x e. _V
152 151 109 opth 
 |-  ( <. x , y >. = <. x , z >. <-> ( x = x /\ y = z ) )
153 152 simprbi 
 |-  ( <. x , y >. = <. x , z >. -> y = z )
154 153 necon3i 
 |-  ( y =/= z -> <. x , y >. =/= <. x , z >. )
155 hashprg 
 |-  ( ( <. x , y >. e. _V /\ <. x , z >. e. _V ) -> ( <. x , y >. =/= <. x , z >. <-> ( # ` { <. x , y >. , <. x , z >. } ) = 2 ) )
156 101 102 155 mp2an 
 |-  ( <. x , y >. =/= <. x , z >. <-> ( # ` { <. x , y >. , <. x , z >. } ) = 2 )
157 154 156 sylib 
 |-  ( y =/= z -> ( # ` { <. x , y >. , <. x , z >. } ) = 2 )
158 157 oveq1d 
 |-  ( y =/= z -> ( ( # ` { <. x , y >. , <. x , z >. } ) + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
159 158 ad2antll 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( ( # ` { <. x , y >. , <. x , z >. } ) + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
160 148 150 159 3eqtr3rd 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( # ` F ) )
161 142 160 breqtrd 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( # ` F ) )
162 81 91 94 129 161 ltletrd 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom F ) < ( # ` F ) )
163 81 162 gtned 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` F ) =/= ( # ` dom F ) )
164 163 ex 
 |-  ( F e. Fin -> ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) -> ( # ` F ) =/= ( # ` dom F ) ) )
165 164 exlimdv 
 |-  ( F e. Fin -> ( E. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) -> ( # ` F ) =/= ( # ` dom F ) ) )
166 165 exlimdvv 
 |-  ( F e. Fin -> ( E. x E. y E. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) -> ( # ` F ) =/= ( # ` dom F ) ) )
167 80 166 syl5bi 
 |-  ( F e. Fin -> ( -. A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) -> ( # ` F ) =/= ( # ` dom F ) ) )
168 167 necon4bd 
 |-  ( F e. Fin -> ( ( # ` F ) = ( # ` dom F ) -> A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) )
169 168 imp 
 |-  ( ( F e. Fin /\ ( # ` F ) = ( # ` dom F ) ) -> A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
170 dffun4 
 |-  ( Fun F <-> ( Rel F /\ A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) )
171 70 169 170 sylanbrc 
 |-  ( ( F e. Fin /\ ( # ` F ) = ( # ` dom F ) ) -> Fun F )
172 171 ex 
 |-  ( F e. Fin -> ( ( # ` F ) = ( # ` dom F ) -> Fun F ) )
173 3 172 impbid2 
 |-  ( F e. Fin -> ( Fun F <-> ( # ` F ) = ( # ` dom F ) ) )