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 syl6eq ⊢ ( ( 𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ ( V × V ) ) → ( dom ( 𝐹 ∖ { 𝑥 } ) ∪ dom { 𝑥 } ) = dom ( 𝐹 ∖ { 𝑥 } ) )
24 23 fveq2d ⊢ ( ( 𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ ( V × V ) ) → ( ♯ ‘ ( dom ( 𝐹 ∖ { 𝑥 } ) ∪ dom { 𝑥 } ) ) = ( ♯ ‘ dom ( 𝐹 ∖ { 𝑥 } ) ) )
25 16 24 syl5eq ⊢ ( ( 𝐹 ∈ 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 incom ⊢ ( ( 𝐹 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ( { 𝑥 } ∩ ( 𝐹 ∖ { 𝑥 } ) )
48 disjdif ⊢ ( { 𝑥 } ∩ ( 𝐹 ∖ { 𝑥 } ) ) = ∅
49 47 48 eqtri ⊢ ( ( 𝐹 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅
50 hashun ⊢ ( ( ( 𝐹 ∖ { 𝑥 } ) ∈ Fin ∧ { 𝑥 } ∈ Fin ∧ ( ( 𝐹 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ ) → ( ♯ ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( ( ♯ ‘ ( 𝐹 ∖ { 𝑥 } ) ) + ( ♯ ‘ { 𝑥 } ) ) )
51 46 49 50 mp3an23 ⊢ ( ( 𝐹 ∖ { 𝑥 } ) ∈ Fin → ( ♯ ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( ( ♯ ‘ ( 𝐹 ∖ { 𝑥 } ) ) + ( ♯ ‘ { 𝑥 } ) ) )
52 26 51 syl ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( ( ♯ ‘ ( 𝐹 ∖ { 𝑥 } ) ) + ( ♯ ‘ { 𝑥 } ) ) )
53 hashsng ⊢ ( 𝑥 ∈ V → ( ♯ ‘ { 𝑥 } ) = 1 )
54 53 elv ⊢ ( ♯ ‘ { 𝑥 } ) = 1
55 54 oveq2i ⊢ ( ( ♯ ‘ ( 𝐹 ∖ { 𝑥 } ) ) + ( ♯ ‘ { 𝑥 } ) ) = ( ( ♯ ‘ ( 𝐹 ∖ { 𝑥 } ) ) + 1 )
56 52 55 syl6req ⊢ ( 𝐹 ∈ Fin → ( ( ♯ ‘ ( 𝐹 ∖ { 𝑥 } ) ) + 1 ) = ( ♯ ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) )
57 56 3ad2ant1 ⊢ ( ( 𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ ( V × V ) ) → ( ( ♯ ‘ ( 𝐹 ∖ { 𝑥 } ) ) + 1 ) = ( ♯ ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) )
58 45 57 breqtrd ⊢ ( ( 𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ ( V × V ) ) → ( ♯ ‘ dom ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) < ( ♯ ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) )
59 difsnid ⊢ ( 𝑥 ∈ 𝐹 → ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝐹 )
60 59 dmeqd ⊢ ( 𝑥 ∈ 𝐹 → dom ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = dom 𝐹 )
61 60 fveq2d ⊢ ( 𝑥 ∈ 𝐹 → ( ♯ ‘ dom ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( ♯ ‘ dom 𝐹 ) )
62 61 3ad2ant2 ⊢ ( ( 𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ ( V × V ) ) → ( ♯ ‘ dom ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( ♯ ‘ dom 𝐹 ) )
63 59 fveq2d ⊢ ( 𝑥 ∈ 𝐹 → ( ♯ ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( ♯ ‘ 𝐹 ) )
64 63 3ad2ant2 ⊢ ( ( 𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ ( V × V ) ) → ( ♯ ‘ ( ( 𝐹 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( ♯ ‘ 𝐹 ) )
65 58 62 64 3brtr3d ⊢ ( ( 𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ ( V × V ) ) → ( ♯ ‘ dom 𝐹 ) < ( ♯ ‘ 𝐹 ) )
66 65 rexlimdv3a ⊢ ( 𝐹 ∈ Fin → ( ∃ 𝑥 ∈ 𝐹 ¬ 𝑥 ∈ ( V × V ) → ( ♯ ‘ dom 𝐹 ) < ( ♯ ‘ 𝐹 ) ) )
67 14 66 syl5bi ⊢ ( 𝐹 ∈ Fin → ( ¬ Rel 𝐹 → ( ♯ ‘ dom 𝐹 ) < ( ♯ ‘ 𝐹 ) ) )
68 67 imp ⊢ ( ( 𝐹 ∈ Fin ∧ ¬ Rel 𝐹 ) → ( ♯ ‘ dom 𝐹 ) < ( ♯ ‘ 𝐹 ) )
69 8 68 gtned ⊢ ( ( 𝐹 ∈ Fin ∧ ¬ Rel 𝐹 ) → ( ♯ ‘ 𝐹 ) ≠ ( ♯ ‘ dom 𝐹 ) )
70 69 ex ⊢ ( 𝐹 ∈ Fin → ( ¬ Rel 𝐹 → ( ♯ ‘ 𝐹 ) ≠ ( ♯ ‘ dom 𝐹 ) ) )
71 70 necon4bd ⊢ ( 𝐹 ∈ Fin → ( ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) → Rel 𝐹 ) )
72 71 imp ⊢ ( ( 𝐹 ∈ Fin ∧ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) → Rel 𝐹 )
73 2nalexn ⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
74 df-ne ⊢ ( 𝑦 ≠ 𝑧 ↔ ¬ 𝑦 = 𝑧 )
75 74 anbi2i ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ↔ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) )
76 annim ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ ¬ 𝑦 = 𝑧 ) ↔ ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
77 75 76 bitri ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ↔ ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
78 77 exbii ⊢ ( ∃ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ↔ ∃ 𝑧 ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
79 exnal ⊢ ( ∃ 𝑧 ¬ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
80 78 79 bitr2i ⊢ ( ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ∃ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) )
81 80 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ¬ ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) )
82 73 81 bitri ⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) )
83 7 adantr ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ dom 𝐹 ) ∈ ℝ )
84 2re ⊢ 2 ∈ ℝ
85 diffi ⊢ ( 𝐹 ∈ Fin → ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin )
86 dmfi ⊢ ( ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin → dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin )
87 85 86 syl ⊢ ( 𝐹 ∈ Fin → dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin )
88 hashcl ⊢ ( dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin → ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℕ0 )
89 87 88 syl ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℕ0 )
90 89 nn0red ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℝ )
91 90 adantr ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℝ )
92 readdcl ⊢ ( ( 2 ∈ ℝ ∧ ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℝ ) → ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ∈ ℝ )
93 84 91 92 sylancr ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ∈ ℝ )
94 hashcl ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
95 94 nn0red ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ 𝐹 ) ∈ ℝ )
96 95 adantr ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℝ )
97 1re ⊢ 1 ∈ ℝ
98 readdcl ⊢ ( ( 1 ∈ ℝ ∧ ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℝ ) → ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ∈ ℝ )
99 97 90 98 sylancr ⊢ ( 𝐹 ∈ Fin → ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ∈ ℝ )
100 99 adantr ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ∈ ℝ )
101 84 90 92 sylancr ⊢ ( 𝐹 ∈ Fin → ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ∈ ℝ )
102 101 adantr ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ∈ ℝ )
103 dmun ⊢ dom ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) = ( dom { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) )
104 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
105 opex ⊢ ⟨ 𝑥 , 𝑧 ⟩ ∈ V
106 104 105 prss ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ↔ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ⊆ 𝐹 )
107 undif ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ⊆ 𝐹 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) = 𝐹 )
108 106 107 sylbb ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) = 𝐹 )
109 108 dmeqd ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → dom ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) = dom 𝐹 )
110 103 109 syl5reqr ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → dom 𝐹 = ( dom { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) )
111 vex ⊢ 𝑦 ∈ V
112 vex ⊢ 𝑧 ∈ V
113 111 112 dmprop ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } = { 𝑥 , 𝑥 }
114 dfsn2 ⊢ { 𝑥 } = { 𝑥 , 𝑥 }
115 113 114 eqtr4i ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } = { 𝑥 }
116 115 uneq1i ⊢ ( dom { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) = ( { 𝑥 } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) )
117 110 116 syl6eq ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → dom 𝐹 = ( { 𝑥 } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) )
118 117 fveq2d ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → ( ♯ ‘ dom 𝐹 ) = ( ♯ ‘ ( { 𝑥 } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
119 118 ad2antrl ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ dom 𝐹 ) = ( ♯ ‘ ( { 𝑥 } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
120 hashun2 ⊢ ( ( { 𝑥 } ∈ Fin ∧ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin ) → ( ♯ ‘ ( { 𝑥 } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ≤ ( ( ♯ ‘ { 𝑥 } ) + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
121 46 87 120 sylancr ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ ( { 𝑥 } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ≤ ( ( ♯ ‘ { 𝑥 } ) + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
122 54 oveq1i ⊢ ( ( ♯ ‘ { 𝑥 } ) + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) = ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) )
123 121 122 breqtrdi ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ ( { 𝑥 } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ≤ ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
124 123 adantr ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ ( { 𝑥 } ∪ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ≤ ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
125 119 124 eqbrtrd ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ dom 𝐹 ) ≤ ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
126 1lt2 ⊢ 1 < 2
127 ltadd1 ⊢ ( ( 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℝ ) → ( 1 < 2 ↔ ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) < ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ) )
128 97 84 90 127 mp3an12i ⊢ ( 𝐹 ∈ Fin → ( 1 < 2 ↔ ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) < ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ) )
129 126 128 mpbii ⊢ ( 𝐹 ∈ Fin → ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) < ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
130 129 adantr ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( 1 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) < ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
131 83 100 102 125 130 lelttrd ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ dom 𝐹 ) < ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
132 fidomdm ⊢ ( ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin → dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ≼ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) )
133 85 132 syl ⊢ ( 𝐹 ∈ Fin → dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ≼ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) )
134 hashdom ⊢ ( ( dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin ∧ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin ) → ( ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ≤ ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ↔ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ≼ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) )
135 87 85 134 syl2anc ⊢ ( 𝐹 ∈ Fin → ( ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ≤ ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ↔ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ≼ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) )
136 133 135 mpbird ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ≤ ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) )
137 hashcl ⊢ ( ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin → ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℕ0 )
138 85 137 syl ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℕ0 )
139 138 nn0red ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℝ )
140 leadd2 ⊢ ( ( ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℝ ∧ ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ≤ ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ↔ ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ≤ ( 2 + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ) )
141 84 140 mp3an3 ⊢ ( ( ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℝ ∧ ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ∈ ℝ ) → ( ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ≤ ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ↔ ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ≤ ( 2 + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ) )
142 90 139 141 syl2anc ⊢ ( 𝐹 ∈ Fin → ( ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ≤ ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ↔ ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ≤ ( 2 + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ) )
143 136 142 mpbid ⊢ ( 𝐹 ∈ Fin → ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ≤ ( 2 + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
144 143 adantr ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ≤ ( 2 + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
145 prfi ⊢ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∈ Fin
146 disjdif ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∩ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) = ∅
147 hashun ⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∈ Fin ∧ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin ∧ ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∩ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) = ∅ ) → ( ♯ ‘ ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) = ( ( ♯ ‘ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
148 145 146 147 mp3an13 ⊢ ( ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ∈ Fin → ( ♯ ‘ ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) = ( ( ♯ ‘ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
149 85 148 syl ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) = ( ( ♯ ‘ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
150 149 adantr ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) = ( ( ♯ ‘ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
151 108 fveq2d ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → ( ♯ ‘ ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) = ( ♯ ‘ 𝐹 ) )
152 151 ad2antrl ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ ( { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ∪ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) = ( ♯ ‘ 𝐹 ) )
153 vex ⊢ 𝑥 ∈ V
154 153 111 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑧 ⟩ ↔ ( 𝑥 = 𝑥 ∧ 𝑦 = 𝑧 ) )
155 154 simprbi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑧 ⟩ → 𝑦 = 𝑧 )
156 155 necon3i ⊢ ( 𝑦 ≠ 𝑧 → ⟨ 𝑥 , 𝑦 ⟩ ≠ ⟨ 𝑥 , 𝑧 ⟩ )
157 hashprg ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ V ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ V ) → ( ⟨ 𝑥 , 𝑦 ⟩ ≠ ⟨ 𝑥 , 𝑧 ⟩ ↔ ( ♯ ‘ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) = 2 ) )
158 104 105 157 mp2an ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ≠ ⟨ 𝑥 , 𝑧 ⟩ ↔ ( ♯ ‘ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) = 2 )
159 156 158 sylib ⊢ ( 𝑦 ≠ 𝑧 → ( ♯ ‘ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) = 2 )
160 159 oveq1d ⊢ ( 𝑦 ≠ 𝑧 → ( ( ♯ ‘ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) = ( 2 + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
161 160 ad2antll ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ( ♯ ‘ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) = ( 2 + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) )
162 150 152 161 3eqtr3rd ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( 2 + ( ♯ ‘ ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) = ( ♯ ‘ 𝐹 ) )
163 144 162 breqtrd ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( 2 + ( ♯ ‘ dom ( 𝐹 ∖ { ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑧 ⟩ } ) ) ) ≤ ( ♯ ‘ 𝐹 ) )
164 83 93 96 131 163 ltletrd ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ dom 𝐹 ) < ( ♯ ‘ 𝐹 ) )
165 83 164 gtned ⊢ ( ( 𝐹 ∈ Fin ∧ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) ) → ( ♯ ‘ 𝐹 ) ≠ ( ♯ ‘ dom 𝐹 ) )
166 165 ex ⊢ ( 𝐹 ∈ Fin → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) → ( ♯ ‘ 𝐹 ) ≠ ( ♯ ‘ dom 𝐹 ) ) )
167 166 exlimdv ⊢ ( 𝐹 ∈ Fin → ( ∃ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) → ( ♯ ‘ 𝐹 ) ≠ ( ♯ ‘ dom 𝐹 ) ) )
168 167 exlimdvv ⊢ ( 𝐹 ∈ Fin → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∧ 𝑦 ≠ 𝑧 ) → ( ♯ ‘ 𝐹 ) ≠ ( ♯ ‘ dom 𝐹 ) ) )
169 82 168 syl5bi ⊢ ( 𝐹 ∈ Fin → ( ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) → ( ♯ ‘ 𝐹 ) ≠ ( ♯ ‘ dom 𝐹 ) ) )
170 169 necon4bd ⊢ ( 𝐹 ∈ Fin → ( ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ) )
171 170 imp ⊢ ( ( 𝐹 ∈ Fin ∧ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
172 dffun4 ⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ) )
173 72 171 172 sylanbrc ⊢ ( ( 𝐹 ∈ Fin ∧ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) → Fun 𝐹 )
174 173 ex ⊢ ( 𝐹 ∈ Fin → ( ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) → Fun 𝐹 ) )
175 3 174 impbid2 ⊢ ( 𝐹 ∈ Fin → ( Fun 𝐹 ↔ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) )