Metamath Proof Explorer

Theorem hashf1lem2

Description: Lemma for hashf1 . (Contributed by Mario Carneiro, 17-Apr-2015)

Ref Expression
Hypotheses hashf1lem2.1 ⊢ φ → A ∈ Fin
hashf1lem2.2 ⊢ φ → B ∈ Fin
hashf1lem2.3 ⊢ φ → ¬ z ∈ A
hashf1lem2.4 ⊢ φ → A + 1 ≤ B
Assertion hashf1lem2 ⊢ φ → f | f : A ∪ z ⟶ 1-1 B = B − A ⁢ f | f : A ⟶ 1-1 B

Proof

Step Hyp Ref Expression
1 hashf1lem2.1 ⊢ φ → A ∈ Fin
2 hashf1lem2.2 ⊢ φ → B ∈ Fin
3 hashf1lem2.3 ⊢ φ → ¬ z ∈ A
4 hashf1lem2.4 ⊢ φ → A + 1 ≤ B
5 ssid ⊢ f | f : A ⟶ 1-1 B ⊆ f | f : A ⟶ 1-1 B
6 mapfi ⊢ B ∈ Fin ∧ A ∈ Fin → B A ∈ Fin
7 2 1 6 syl2anc ⊢ φ → B A ∈ Fin
8 f1f ⊢ f : A ⟶ 1-1 B → f : A ⟶ B
9 2 1 elmapd ⊢ φ → f ∈ B A ↔ f : A ⟶ B
10 8 9 imbitrrid ⊢ φ → f : A ⟶ 1-1 B → f ∈ B A
11 10 abssdv ⊢ φ → f | f : A ⟶ 1-1 B ⊆ B A
12 7 11 ssfid ⊢ φ → f | f : A ⟶ 1-1 B ∈ Fin
13 sseq1 ⊢ x = ∅ → x ⊆ f | f : A ⟶ 1-1 B ↔ ∅ ⊆ f | f : A ⟶ 1-1 B
14 eleq2 ⊢ x = ∅ → f ↾ A ∈ x ↔ f ↾ A ∈ ∅
15 noel ⊢ ¬ f ↾ A ∈ ∅
16 15 pm2.21i ⊢ f ↾ A ∈ ∅ → f ∈ ∅
17 14 16 biimtrdi ⊢ x = ∅ → f ↾ A ∈ x → f ∈ ∅
18 17 adantrd ⊢ x = ∅ → f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B → f ∈ ∅
19 18 abssdv ⊢ x = ∅ → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B ⊆ ∅
20 ss0 ⊢ f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B ⊆ ∅ → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = ∅
21 19 20 syl ⊢ x = ∅ → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = ∅
22 21 fveq2d ⊢ x = ∅ → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = ∅
23 hash0 ⊢ ∅ = 0
24 22 23 eqtrdi ⊢ x = ∅ → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = 0
25 fveq2 ⊢ x = ∅ → x = ∅
26 25 23 eqtrdi ⊢ x = ∅ → x = 0
27 26 oveq2d ⊢ x = ∅ → B − A ⁢ x = B − A ⋅ 0
28 24 27 eqeq12d ⊢ x = ∅ → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ 0 = B − A ⋅ 0
29 13 28 imbi12d ⊢ x = ∅ → x ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ ∅ ⊆ f | f : A ⟶ 1-1 B → 0 = B − A ⋅ 0
30 29 imbi2d ⊢ x = ∅ → φ → x ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ φ → ∅ ⊆ f | f : A ⟶ 1-1 B → 0 = B − A ⋅ 0
31 sseq1 ⊢ x = y → x ⊆ f | f : A ⟶ 1-1 B ↔ y ⊆ f | f : A ⟶ 1-1 B
32 eleq2 ⊢ x = y → f ↾ A ∈ x ↔ f ↾ A ∈ y
33 32 anbi1d ⊢ x = y → f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B ↔ f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B
34 33 abbidv ⊢ x = y → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B
35 34 fveq2d ⊢ x = y → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B
36 fveq2 ⊢ x = y → x = y
37 36 oveq2d ⊢ x = y → B − A ⁢ x = B − A ⁢ y
38 35 37 eqeq12d ⊢ x = y → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y
39 31 38 imbi12d ⊢ x = y → x ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ y ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y
40 39 imbi2d ⊢ x = y → φ → x ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ φ → y ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y
41 sseq1 ⊢ x = y ∪ a → x ⊆ f | f : A ⟶ 1-1 B ↔ y ∪ a ⊆ f | f : A ⟶ 1-1 B
42 eleq2 ⊢ x = y ∪ a → f ↾ A ∈ x ↔ f ↾ A ∈ y ∪ a
43 42 anbi1d ⊢ x = y ∪ a → f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B ↔ f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B
44 43 abbidv ⊢ x = y ∪ a → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B
45 44 fveq2d ⊢ x = y ∪ a → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B
46 fveq2 ⊢ x = y ∪ a → x = y ∪ a
47 46 oveq2d ⊢ x = y ∪ a → B − A ⁢ x = B − A ⁢ y ∪ a
48 45 47 eqeq12d ⊢ x = y ∪ a → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y ∪ a
49 41 48 imbi12d ⊢ x = y ∪ a → x ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y ∪ a
50 49 imbi2d ⊢ x = y ∪ a → φ → x ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ φ → y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y ∪ a
51 sseq1 ⊢ x = f | f : A ⟶ 1-1 B → x ⊆ f | f : A ⟶ 1-1 B ↔ f | f : A ⟶ 1-1 B ⊆ f | f : A ⟶ 1-1 B
52 f1eq1 ⊢ f = y → f : A ⟶ 1-1 B ↔ y : A ⟶ 1-1 B
53 52 cbvabv ⊢ f | f : A ⟶ 1-1 B = y | y : A ⟶ 1-1 B
54 53 eqeq2i ⊢ x = f | f : A ⟶ 1-1 B ↔ x = y | y : A ⟶ 1-1 B
55 ssun1 ⊢ A ⊆ A ∪ z
56 f1ssres ⊢ f : A ∪ z ⟶ 1-1 B ∧ A ⊆ A ∪ z → f ↾ A : A ⟶ 1-1 B
57 55 56 mpan2 ⊢ f : A ∪ z ⟶ 1-1 B → f ↾ A : A ⟶ 1-1 B
58 vex ⊢ f ∈ V
59 58 resex ⊢ f ↾ A ∈ V
60 f1eq1 ⊢ y = f ↾ A → y : A ⟶ 1-1 B ↔ f ↾ A : A ⟶ 1-1 B
61 59 60 elab ⊢ f ↾ A ∈ y | y : A ⟶ 1-1 B ↔ f ↾ A : A ⟶ 1-1 B
62 57 61 sylibr ⊢ f : A ∪ z ⟶ 1-1 B → f ↾ A ∈ y | y : A ⟶ 1-1 B
63 eleq2 ⊢ x = y | y : A ⟶ 1-1 B → f ↾ A ∈ x ↔ f ↾ A ∈ y | y : A ⟶ 1-1 B
64 62 63 imbitrrid ⊢ x = y | y : A ⟶ 1-1 B → f : A ∪ z ⟶ 1-1 B → f ↾ A ∈ x
65 64 pm4.71rd ⊢ x = y | y : A ⟶ 1-1 B → f : A ∪ z ⟶ 1-1 B ↔ f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B
66 65 bicomd ⊢ x = y | y : A ⟶ 1-1 B → f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B ↔ f : A ∪ z ⟶ 1-1 B
67 66 abbidv ⊢ x = y | y : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = f | f : A ∪ z ⟶ 1-1 B
68 54 67 sylbi ⊢ x = f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = f | f : A ∪ z ⟶ 1-1 B
69 68 fveq2d ⊢ x = f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = f | f : A ∪ z ⟶ 1-1 B
70 fveq2 ⊢ x = f | f : A ⟶ 1-1 B → x = f | f : A ⟶ 1-1 B
71 70 oveq2d ⊢ x = f | f : A ⟶ 1-1 B → B − A ⁢ x = B − A ⁢ f | f : A ⟶ 1-1 B
72 69 71 eqeq12d ⊢ x = f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ f | f : A ∪ z ⟶ 1-1 B = B − A ⁢ f | f : A ⟶ 1-1 B
73 51 72 imbi12d ⊢ x = f | f : A ⟶ 1-1 B → x ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ f | f : A ⟶ 1-1 B ⊆ f | f : A ⟶ 1-1 B → f | f : A ∪ z ⟶ 1-1 B = B − A ⁢ f | f : A ⟶ 1-1 B
74 73 imbi2d ⊢ x = f | f : A ⟶ 1-1 B → φ → x ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ x ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ x ↔ φ → f | f : A ⟶ 1-1 B ⊆ f | f : A ⟶ 1-1 B → f | f : A ∪ z ⟶ 1-1 B = B − A ⁢ f | f : A ⟶ 1-1 B
75 hashcl ⊢ B ∈ Fin → B ∈ ℕ 0
76 2 75 syl ⊢ φ → B ∈ ℕ 0
77 76 nn0cnd ⊢ φ → B ∈ ℂ
78 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
79 1 78 syl ⊢ φ → A ∈ ℕ 0
80 79 nn0cnd ⊢ φ → A ∈ ℂ
81 77 80 subcld ⊢ φ → B − A ∈ ℂ
82 81 mul01d ⊢ φ → B − A ⋅ 0 = 0
83 82 eqcomd ⊢ φ → 0 = B − A ⋅ 0
84 83 a1d ⊢ φ → ∅ ⊆ f | f : A ⟶ 1-1 B → 0 = B − A ⋅ 0
85 ssun1 ⊢ y ⊆ y ∪ a
86 sstr ⊢ y ⊆ y ∪ a ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → y ⊆ f | f : A ⟶ 1-1 B
87 85 86 mpan ⊢ y ∪ a ⊆ f | f : A ⟶ 1-1 B → y ⊆ f | f : A ⟶ 1-1 B
88 87 imim1i ⊢ y ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y → y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y
89 oveq1 ⊢ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B + B - A = B − A ⁢ y + B - A
90 elun ⊢ f ↾ A ∈ y ∪ a ↔ f ↾ A ∈ y ∨ f ↾ A ∈ a
91 59 elsn ⊢ f ↾ A ∈ a ↔ f ↾ A = a
92 91 orbi2i ⊢ f ↾ A ∈ y ∨ f ↾ A ∈ a ↔ f ↾ A ∈ y ∨ f ↾ A = a
93 90 92 bitri ⊢ f ↾ A ∈ y ∪ a ↔ f ↾ A ∈ y ∨ f ↾ A = a
94 93 anbi1i ⊢ f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B ↔ f ↾ A ∈ y ∨ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
95 andir ⊢ f ↾ A ∈ y ∨ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ↔ f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∨ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
96 94 95 bitri ⊢ f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B ↔ f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∨ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
97 96 abbii ⊢ f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∨ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
98 unab ⊢ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∪ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∨ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
99 97 98 eqtr4i ⊢ f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∪ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
100 99 fveq2i ⊢ f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∪ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
101 snfi ⊢ z ∈ Fin
102 unfi ⊢ A ∈ Fin ∧ z ∈ Fin → A ∪ z ∈ Fin
103 1 101 102 sylancl ⊢ φ → A ∪ z ∈ Fin
104 mapvalg ⊢ B ∈ Fin ∧ A ∪ z ∈ Fin → B A ∪ z = f | f : A ∪ z ⟶ B
105 2 103 104 syl2anc ⊢ φ → B A ∪ z = f | f : A ∪ z ⟶ B
106 mapfi ⊢ B ∈ Fin ∧ A ∪ z ∈ Fin → B A ∪ z ∈ Fin
107 2 103 106 syl2anc ⊢ φ → B A ∪ z ∈ Fin
108 105 107 eqeltrrd ⊢ φ → f | f : A ∪ z ⟶ B ∈ Fin
109 f1f ⊢ f : A ∪ z ⟶ 1-1 B → f : A ∪ z ⟶ B
110 109 adantl ⊢ f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B → f : A ∪ z ⟶ B
111 110 ss2abi ⊢ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ⊆ f | f : A ∪ z ⟶ B
112 ssfi ⊢ f | f : A ∪ z ⟶ B ∈ Fin ∧ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ⊆ f | f : A ∪ z ⟶ B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∈ Fin
113 108 111 112 sylancl ⊢ φ → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∈ Fin
114 113 adantr ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∈ Fin
115 109 adantl ⊢ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B → f : A ∪ z ⟶ B
116 115 ss2abi ⊢ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ⊆ f | f : A ∪ z ⟶ B
117 ssfi ⊢ f | f : A ∪ z ⟶ B ∈ Fin ∧ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ⊆ f | f : A ∪ z ⟶ B → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ∈ Fin
118 108 116 117 sylancl ⊢ φ → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ∈ Fin
119 118 adantr ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ∈ Fin
120 inab ⊢ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∩ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∧ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
121 simprlr ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → ¬ a ∈ y
122 abn0 ⊢ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∧ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ≠ ∅ ↔ ∃ f f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∧ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
123 simprl ⊢ f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∧ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B → f ↾ A = a
124 simpll ⊢ f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∧ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B → f ↾ A ∈ y
125 123 124 eqeltrrd ⊢ f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∧ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B → a ∈ y
126 125 exlimiv ⊢ ∃ f f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∧ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B → a ∈ y
127 122 126 sylbi ⊢ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∧ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ≠ ∅ → a ∈ y
128 127 necon1bi ⊢ ¬ a ∈ y → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∧ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = ∅
129 121 128 syl ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∧ f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = ∅
130 120 129 eqtrid ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∩ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = ∅
131 hashun ⊢ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∈ Fin ∧ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ∈ Fin ∧ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∩ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = ∅ → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∪ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B + f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
132 114 119 130 131 syl3anc ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B ∪ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B + f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
133 100 132 eqtrid ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B + f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
134 simpr ⊢ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → y ∪ a ⊆ f | f : A ⟶ 1-1 B
135 134 unssbd ⊢ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → a ⊆ f | f : A ⟶ 1-1 B
136 vex ⊢ a ∈ V
137 136 snss ⊢ a ∈ f | f : A ⟶ 1-1 B ↔ a ⊆ f | f : A ⟶ 1-1 B
138 135 137 sylibr ⊢ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → a ∈ f | f : A ⟶ 1-1 B
139 f1eq1 ⊢ f = a → f : A ⟶ 1-1 B ↔ a : A ⟶ 1-1 B
140 136 139 elab ⊢ a ∈ f | f : A ⟶ 1-1 B ↔ a : A ⟶ 1-1 B
141 138 140 sylib ⊢ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → a : A ⟶ 1-1 B
142 80 adantr ⊢ φ ∧ a : A ⟶ 1-1 B → A ∈ ℂ
143 118 adantr ⊢ φ ∧ a : A ⟶ 1-1 B → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ∈ Fin
144 hashcl ⊢ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ∈ Fin → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ∈ ℕ 0
145 143 144 syl ⊢ φ ∧ a : A ⟶ 1-1 B → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ∈ ℕ 0
146 145 nn0cnd ⊢ φ ∧ a : A ⟶ 1-1 B → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ∈ ℂ
147 142 146 pncan2d ⊢ φ ∧ a : A ⟶ 1-1 B → A + f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B - A = f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B
148 f1f1orn ⊢ a : A ⟶ 1-1 B → a : A ⟶ 1-1 onto ran ⁡ a
149 148 adantl ⊢ φ ∧ a : A ⟶ 1-1 B → a : A ⟶ 1-1 onto ran ⁡ a
150 f1oen3g ⊢ a ∈ V ∧ a : A ⟶ 1-1 onto ran ⁡ a → A ≈ ran ⁡ a
151 136 149 150 sylancr ⊢ φ ∧ a : A ⟶ 1-1 B → A ≈ ran ⁡ a
152 hasheni ⊢ A ≈ ran ⁡ a → A = ran ⁡ a
153 151 152 syl ⊢ φ ∧ a : A ⟶ 1-1 B → A = ran ⁡ a
154 1 adantr ⊢ φ ∧ a : A ⟶ 1-1 B → A ∈ Fin
155 2 adantr ⊢ φ ∧ a : A ⟶ 1-1 B → B ∈ Fin
156 3 adantr ⊢ φ ∧ a : A ⟶ 1-1 B → ¬ z ∈ A
157 4 adantr ⊢ φ ∧ a : A ⟶ 1-1 B → A + 1 ≤ B
158 simpr ⊢ φ ∧ a : A ⟶ 1-1 B → a : A ⟶ 1-1 B
159 154 155 156 157 158 hashf1lem1 ⊢ φ ∧ a : A ⟶ 1-1 B → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ≈ B ∖ ran ⁡ a
160 hasheni ⊢ f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B ≈ B ∖ ran ⁡ a → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = B ∖ ran ⁡ a
161 159 160 syl ⊢ φ ∧ a : A ⟶ 1-1 B → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = B ∖ ran ⁡ a
162 153 161 oveq12d ⊢ φ ∧ a : A ⟶ 1-1 B → A + f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = ran ⁡ a + B ∖ ran ⁡ a
163 f1f ⊢ a : A ⟶ 1-1 B → a : A ⟶ B
164 163 frnd ⊢ a : A ⟶ 1-1 B → ran ⁡ a ⊆ B
165 164 adantl ⊢ φ ∧ a : A ⟶ 1-1 B → ran ⁡ a ⊆ B
166 155 165 ssfid ⊢ φ ∧ a : A ⟶ 1-1 B → ran ⁡ a ∈ Fin
167 diffi ⊢ B ∈ Fin → B ∖ ran ⁡ a ∈ Fin
168 155 167 syl ⊢ φ ∧ a : A ⟶ 1-1 B → B ∖ ran ⁡ a ∈ Fin
169 disjdif ⊢ ran ⁡ a ∩ B ∖ ran ⁡ a = ∅
170 169 a1i ⊢ φ ∧ a : A ⟶ 1-1 B → ran ⁡ a ∩ B ∖ ran ⁡ a = ∅
171 hashun ⊢ ran ⁡ a ∈ Fin ∧ B ∖ ran ⁡ a ∈ Fin ∧ ran ⁡ a ∩ B ∖ ran ⁡ a = ∅ → ran ⁡ a ∪ B ∖ ran ⁡ a = ran ⁡ a + B ∖ ran ⁡ a
172 166 168 170 171 syl3anc ⊢ φ ∧ a : A ⟶ 1-1 B → ran ⁡ a ∪ B ∖ ran ⁡ a = ran ⁡ a + B ∖ ran ⁡ a
173 undif ⊢ ran ⁡ a ⊆ B ↔ ran ⁡ a ∪ B ∖ ran ⁡ a = B
174 165 173 sylib ⊢ φ ∧ a : A ⟶ 1-1 B → ran ⁡ a ∪ B ∖ ran ⁡ a = B
175 174 fveq2d ⊢ φ ∧ a : A ⟶ 1-1 B → ran ⁡ a ∪ B ∖ ran ⁡ a = B
176 162 172 175 3eqtr2d ⊢ φ ∧ a : A ⟶ 1-1 B → A + f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = B
177 176 oveq1d ⊢ φ ∧ a : A ⟶ 1-1 B → A + f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B - A = B − A
178 147 177 eqtr3d ⊢ φ ∧ a : A ⟶ 1-1 B → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = B − A
179 141 178 sylan2 ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = B − A
180 179 oveq2d ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B + f | f ↾ A = a ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B + B - A
181 133 180 eqtrd ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B + B - A
182 hashunsng ⊢ a ∈ V → y ∈ Fin ∧ ¬ a ∈ y → y ∪ a = y + 1
183 182 elv ⊢ y ∈ Fin ∧ ¬ a ∈ y → y ∪ a = y + 1
184 183 ad2antrl ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → y ∪ a = y + 1
185 184 oveq2d ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → B − A ⁢ y ∪ a = B − A ⁢ y + 1
186 81 adantr ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → B − A ∈ ℂ
187 simprll ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → y ∈ Fin
188 hashcl ⊢ y ∈ Fin → y ∈ ℕ 0
189 187 188 syl ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → y ∈ ℕ 0
190 189 nn0cnd ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → y ∈ ℂ
191 1cnd ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → 1 ∈ ℂ
192 186 190 191 adddid ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → B − A ⁢ y + 1 = B − A ⁢ y + B − A ⋅ 1
193 186 mulridd ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → B − A ⋅ 1 = B − A
194 193 oveq2d ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → B − A ⁢ y + B − A ⋅ 1 = B − A ⁢ y + B - A
195 185 192 194 3eqtrd ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → B − A ⁢ y ∪ a = B − A ⁢ y + B - A
196 181 195 eqeq12d ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y ∪ a ↔ f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B + B - A = B − A ⁢ y + B - A
197 89 196 imbitrrid ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y ∧ y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y ∪ a
198 197 expr ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y → y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y ∪ a
199 198 a2d ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y → y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y → y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y ∪ a
200 88 199 syl5 ⊢ φ ∧ y ∈ Fin ∧ ¬ a ∈ y → y ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y → y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y ∪ a
201 200 expcom ⊢ y ∈ Fin ∧ ¬ a ∈ y → φ → y ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y → y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y ∪ a
202 201 a2d ⊢ y ∈ Fin ∧ ¬ a ∈ y → φ → y ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y → φ → y ∪ a ⊆ f | f : A ⟶ 1-1 B → f | f ↾ A ∈ y ∪ a ∧ f : A ∪ z ⟶ 1-1 B = B − A ⁢ y ∪ a
203 30 40 50 74 84 202 findcard2s ⊢ f | f : A ⟶ 1-1 B ∈ Fin → φ → f | f : A ⟶ 1-1 B ⊆ f | f : A ⟶ 1-1 B → f | f : A ∪ z ⟶ 1-1 B = B − A ⁢ f | f : A ⟶ 1-1 B
204 12 203 mpcom ⊢ φ → f | f : A ⟶ 1-1 B ⊆ f | f : A ⟶ 1-1 B → f | f : A ∪ z ⟶ 1-1 B = B − A ⁢ f | f : A ⟶ 1-1 B
205 5 204 mpi ⊢ φ → f | f : A ∪ z ⟶ 1-1 B = B − A ⁢ f | f : A ⟶ 1-1 B