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 ( 𝐹 ∈ Fin → ( Fun 𝐹 ↔ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) )

Proof

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