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 syl6eq 
 |-  ( ( 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 syl5eq 
 |-  ( ( 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 incom 
 |-  ( ( F \ { x } ) i^i { x } ) = ( { x } i^i ( F \ { x } ) )
48 disjdif 
 |-  ( { x } i^i ( F \ { x } ) ) = (/)
49 47 48 eqtri 
 |-  ( ( F \ { x } ) i^i { x } ) = (/)
50 hashun 
 |-  ( ( ( F \ { x } ) e. Fin /\ { x } e. Fin /\ ( ( F \ { x } ) i^i { x } ) = (/) ) -> ( # ` ( ( F \ { x } ) u. { x } ) ) = ( ( # ` ( F \ { x } ) ) + ( # ` { x } ) ) )
51 46 49 50 mp3an23 
 |-  ( ( F \ { x } ) e. Fin -> ( # ` ( ( F \ { x } ) u. { x } ) ) = ( ( # ` ( F \ { x } ) ) + ( # ` { x } ) ) )
52 26 51 syl 
 |-  ( F e. Fin -> ( # ` ( ( F \ { x } ) u. { x } ) ) = ( ( # ` ( F \ { x } ) ) + ( # ` { x } ) ) )
53 hashsng 
 |-  ( x e. _V -> ( # ` { x } ) = 1 )
54 53 elv 
 |-  ( # ` { x } ) = 1
55 54 oveq2i 
 |-  ( ( # ` ( F \ { x } ) ) + ( # ` { x } ) ) = ( ( # ` ( F \ { x } ) ) + 1 )
56 52 55 eqtr2di 
 |-  ( F e. Fin -> ( ( # ` ( F \ { x } ) ) + 1 ) = ( # ` ( ( F \ { x } ) u. { x } ) ) )
57 56 3ad2ant1 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( ( # ` ( F \ { x } ) ) + 1 ) = ( # ` ( ( F \ { x } ) u. { x } ) ) )
58 45 57 breqtrd 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` dom ( ( F \ { x } ) u. { x } ) ) < ( # ` ( ( F \ { x } ) u. { x } ) ) )
59 difsnid 
 |-  ( x e. F -> ( ( F \ { x } ) u. { x } ) = F )
60 59 dmeqd 
 |-  ( x e. F -> dom ( ( F \ { x } ) u. { x } ) = dom F )
61 60 fveq2d 
 |-  ( x e. F -> ( # ` dom ( ( F \ { x } ) u. { x } ) ) = ( # ` dom F ) )
62 61 3ad2ant2 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` dom ( ( F \ { x } ) u. { x } ) ) = ( # ` dom F ) )
63 59 fveq2d 
 |-  ( x e. F -> ( # ` ( ( F \ { x } ) u. { x } ) ) = ( # ` F ) )
64 63 3ad2ant2 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` ( ( F \ { x } ) u. { x } ) ) = ( # ` F ) )
65 58 62 64 3brtr3d 
 |-  ( ( F e. Fin /\ x e. F /\ -. x e. ( _V X. _V ) ) -> ( # ` dom F ) < ( # ` F ) )
66 65 rexlimdv3a 
 |-  ( F e. Fin -> ( E. x e. F -. x e. ( _V X. _V ) -> ( # ` dom F ) < ( # ` F ) ) )
67 14 66 syl5bi 
 |-  ( F e. Fin -> ( -. Rel F -> ( # ` dom F ) < ( # ` F ) ) )
68 67 imp 
 |-  ( ( F e. Fin /\ -. Rel F ) -> ( # ` dom F ) < ( # ` F ) )
69 8 68 gtned 
 |-  ( ( F e. Fin /\ -. Rel F ) -> ( # ` F ) =/= ( # ` dom F ) )
70 69 ex 
 |-  ( F e. Fin -> ( -. Rel F -> ( # ` F ) =/= ( # ` dom F ) ) )
71 70 necon4bd 
 |-  ( F e. Fin -> ( ( # ` F ) = ( # ` dom F ) -> Rel F ) )
72 71 imp 
 |-  ( ( F e. Fin /\ ( # ` F ) = ( # ` dom F ) ) -> Rel F )
73 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 ) )
74 df-ne 
 |-  ( y =/= z <-> -. y = z )
75 74 anbi2i 
 |-  ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) <-> ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ -. y = z ) )
76 annim 
 |-  ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ -. y = z ) <-> -. ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
77 75 76 bitri 
 |-  ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) <-> -. ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
78 77 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 ) )
79 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 ) )
80 78 79 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 ) )
81 80 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 ) )
82 73 81 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 ) )
83 7 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom F ) e. RR )
84 2re 
 |-  2 e. RR
85 diffi 
 |-  ( F e. Fin -> ( F \ { <. x , y >. , <. x , z >. } ) e. Fin )
86 dmfi 
 |-  ( ( F \ { <. x , y >. , <. x , z >. } ) e. Fin -> dom ( F \ { <. x , y >. , <. x , z >. } ) e. Fin )
87 85 86 syl 
 |-  ( F e. Fin -> dom ( F \ { <. x , y >. , <. x , z >. } ) e. Fin )
88 hashcl 
 |-  ( dom ( F \ { <. x , y >. , <. x , z >. } ) e. Fin -> ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. NN0 )
89 87 88 syl 
 |-  ( F e. Fin -> ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. NN0 )
90 89 nn0red 
 |-  ( F e. Fin -> ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR )
91 90 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR )
92 readdcl 
 |-  ( ( 2 e. RR /\ ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR ) -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
93 84 91 92 sylancr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
94 hashcl 
 |-  ( F e. Fin -> ( # ` F ) e. NN0 )
95 94 nn0red 
 |-  ( F e. Fin -> ( # ` F ) e. RR )
96 95 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` F ) e. RR )
97 1re 
 |-  1 e. RR
98 readdcl 
 |-  ( ( 1 e. RR /\ ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR ) -> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
99 97 90 98 sylancr 
 |-  ( F e. Fin -> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
100 99 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
101 84 90 92 sylancr 
 |-  ( F e. Fin -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
102 101 adantr 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) e. RR )
103 dmun 
 |-  dom ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) = ( dom { <. x , y >. , <. x , z >. } u. dom ( F \ { <. x , y >. , <. x , z >. } ) )
104 opex 
 |-  <. x , y >. e. _V
105 opex 
 |-  <. x , z >. e. _V
106 104 105 prss 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) <-> { <. x , y >. , <. x , z >. } C_ F )
107 undif 
 |-  ( { <. x , y >. , <. x , z >. } C_ F <-> ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) = F )
108 106 107 sylbb 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) = F )
109 108 dmeqd 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> dom ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) = dom F )
110 103 109 syl5reqr 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> dom F = ( dom { <. x , y >. , <. x , z >. } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) )
111 vex 
 |-  y e. _V
112 vex 
 |-  z e. _V
113 111 112 dmprop 
 |-  dom { <. x , y >. , <. x , z >. } = { x , x }
114 dfsn2 
 |-  { x } = { x , x }
115 113 114 eqtr4i 
 |-  dom { <. x , y >. , <. x , z >. } = { x }
116 115 uneq1i 
 |-  ( dom { <. x , y >. , <. x , z >. } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) = ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) )
117 110 116 syl6eq 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> dom F = ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) )
118 117 fveq2d 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> ( # ` dom F ) = ( # ` ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
119 118 ad2antrl 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom F ) = ( # ` ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
120 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 >. } ) ) ) )
121 46 87 120 sylancr 
 |-  ( F e. Fin -> ( # ` ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( ( # ` { x } ) + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
122 54 oveq1i 
 |-  ( ( # ` { x } ) + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) )
123 121 122 breqtrdi 
 |-  ( F e. Fin -> ( # ` ( { x } u. dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
124 123 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 >. } ) ) ) )
125 119 124 eqbrtrd 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom F ) <_ ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
126 1lt2 
 |-  1 < 2
127 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 >. } ) ) ) ) )
128 97 84 90 127 mp3an12i 
 |-  ( F e. Fin -> ( 1 < 2 <-> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) < ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) ) )
129 126 128 mpbii 
 |-  ( F e. Fin -> ( 1 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) < ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
130 129 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 >. } ) ) ) )
131 83 100 102 125 130 lelttrd 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom F ) < ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
132 fidomdm 
 |-  ( ( F \ { <. x , y >. , <. x , z >. } ) e. Fin -> dom ( F \ { <. x , y >. , <. x , z >. } ) ~<_ ( F \ { <. x , y >. , <. x , z >. } ) )
133 85 132 syl 
 |-  ( F e. Fin -> dom ( F \ { <. x , y >. , <. x , z >. } ) ~<_ ( F \ { <. x , y >. , <. x , z >. } ) )
134 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 >. } ) ) )
135 87 85 134 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 >. } ) ) )
136 133 135 mpbird 
 |-  ( F e. Fin -> ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) <_ ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) )
137 hashcl 
 |-  ( ( F \ { <. x , y >. , <. x , z >. } ) e. Fin -> ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) e. NN0 )
138 85 137 syl 
 |-  ( F e. Fin -> ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) e. NN0 )
139 138 nn0red 
 |-  ( F e. Fin -> ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) e. RR )
140 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 >. } ) ) ) ) )
141 84 140 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 >. } ) ) ) ) )
142 90 139 141 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 >. } ) ) ) ) )
143 136 142 mpbid 
 |-  ( F e. Fin -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
144 143 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 >. } ) ) ) )
145 prfi 
 |-  { <. x , y >. , <. x , z >. } e. Fin
146 disjdif 
 |-  ( { <. x , y >. , <. x , z >. } i^i ( F \ { <. x , y >. , <. x , z >. } ) ) = (/)
147 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 >. } ) ) ) )
148 145 146 147 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 >. } ) ) ) )
149 85 148 syl 
 |-  ( F e. Fin -> ( # ` ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( ( # ` { <. x , y >. , <. x , z >. } ) + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
150 149 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 >. } ) ) ) )
151 108 fveq2d 
 |-  ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> ( # ` ( { <. x , y >. , <. x , z >. } u. ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( # ` F ) )
152 151 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 ) )
153 vex 
 |-  x e. _V
154 153 111 opth 
 |-  ( <. x , y >. = <. x , z >. <-> ( x = x /\ y = z ) )
155 154 simprbi 
 |-  ( <. x , y >. = <. x , z >. -> y = z )
156 155 necon3i 
 |-  ( y =/= z -> <. x , y >. =/= <. x , z >. )
157 hashprg 
 |-  ( ( <. x , y >. e. _V /\ <. x , z >. e. _V ) -> ( <. x , y >. =/= <. x , z >. <-> ( # ` { <. x , y >. , <. x , z >. } ) = 2 ) )
158 104 105 157 mp2an 
 |-  ( <. x , y >. =/= <. x , z >. <-> ( # ` { <. x , y >. , <. x , z >. } ) = 2 )
159 156 158 sylib 
 |-  ( y =/= z -> ( # ` { <. x , y >. , <. x , z >. } ) = 2 )
160 159 oveq1d 
 |-  ( y =/= z -> ( ( # ` { <. x , y >. , <. x , z >. } ) + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) )
161 160 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 >. } ) ) ) )
162 150 152 161 3eqtr3rd 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 2 + ( # ` ( F \ { <. x , y >. , <. x , z >. } ) ) ) = ( # ` F ) )
163 144 162 breqtrd 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( 2 + ( # ` dom ( F \ { <. x , y >. , <. x , z >. } ) ) ) <_ ( # ` F ) )
164 83 93 96 131 163 ltletrd 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` dom F ) < ( # ` F ) )
165 83 164 gtned 
 |-  ( ( F e. Fin /\ ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) ) -> ( # ` F ) =/= ( # ` dom F ) )
166 165 ex 
 |-  ( F e. Fin -> ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) -> ( # ` F ) =/= ( # ` dom F ) ) )
167 166 exlimdv 
 |-  ( F e. Fin -> ( E. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) -> ( # ` F ) =/= ( # ` dom F ) ) )
168 167 exlimdvv 
 |-  ( F e. Fin -> ( E. x E. y E. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ y =/= z ) -> ( # ` F ) =/= ( # ` dom F ) ) )
169 82 168 syl5bi 
 |-  ( F e. Fin -> ( -. A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) -> ( # ` F ) =/= ( # ` dom F ) ) )
170 169 necon4bd 
 |-  ( F e. Fin -> ( ( # ` F ) = ( # ` dom F ) -> A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) )
171 170 imp 
 |-  ( ( F e. Fin /\ ( # ` F ) = ( # ` dom F ) ) -> A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
172 dffun4 
 |-  ( Fun F <-> ( Rel F /\ A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) )
173 72 171 172 sylanbrc 
 |-  ( ( F e. Fin /\ ( # ` F ) = ( # ` dom F ) ) -> Fun F )
174 173 ex 
 |-  ( F e. Fin -> ( ( # ` F ) = ( # ` dom F ) -> Fun F ) )
175 3 174 impbid2 
 |-  ( F e. Fin -> ( Fun F <-> ( # ` F ) = ( # ` dom F ) ) )