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-1B=B−A⁢f|f:A⟶1-1B

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