Metamath Proof Explorer


Theorem poimirlem28

Description: Lemma for poimir , a variant of Sperner's lemma. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ⊢ φ → N ∈ ℕ
poimirlem28.1 ⊢ p = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 → B = C
poimirlem28.2 ⊢ φ ∧ p : 1 … N ⟶ 0 … K → B ∈ 0 … N
poimirlem28.3 ⊢ φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 → B < n
poimirlem28.4 ⊢ φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = K → B ≠ n − 1
poimirlem28.5 ⊢ φ → K ∈ ℕ
Assertion poimirlem28 ⊢ φ → ∃ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C

Proof

Step Hyp Ref Expression
1 poimir.0 ⊢ φ → N ∈ ℕ
2 poimirlem28.1 ⊢ p = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 → B = C
3 poimirlem28.2 ⊢ φ ∧ p : 1 … N ⟶ 0 … K → B ∈ 0 … N
4 poimirlem28.3 ⊢ φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 → B < n
5 poimirlem28.4 ⊢ φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = K → B ≠ n − 1
6 poimirlem28.5 ⊢ φ → K ∈ ℕ
7 1 nnnn0d ⊢ φ → N ∈ ℕ 0
8 1 nnred ⊢ φ → N ∈ ℝ
9 8 leidd ⊢ φ → N ≤ N
10 7 7 9 3jca ⊢ φ → N ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ N ≤ N
11 oveq2 ⊢ k = 0 → 1 … k = 1 … 0
12 fz10 ⊢ 1 … 0 = ∅
13 11 12 eqtrdi ⊢ k = 0 → 1 … k = ∅
14 13 oveq2d ⊢ k = 0 → 0 ..^ K 1 … k = 0 ..^ K ∅
15 fzofi ⊢ 0 ..^ K ∈ Fin
16 map0e ⊢ 0 ..^ K ∈ Fin → 0 ..^ K ∅ = 1 𝑜
17 15 16 ax-mp ⊢ 0 ..^ K ∅ = 1 𝑜
18 df1o2 ⊢ 1 𝑜 = ∅
19 17 18 eqtri ⊢ 0 ..^ K ∅ = ∅
20 14 19 eqtrdi ⊢ k = 0 → 0 ..^ K 1 … k = ∅
21 eqidd ⊢ k = 0 → f = f
22 21 13 13 f1oeq123d ⊢ k = 0 → f : 1 … k ⟶ 1-1 onto 1 … k ↔ f : ∅ ⟶ 1-1 onto ∅
23 eqid ⊢ ∅ = ∅
24 f1o00 ⊢ f : ∅ ⟶ 1-1 onto ∅ ↔ f = ∅ ∧ ∅ = ∅
25 23 24 mpbiran2 ⊢ f : ∅ ⟶ 1-1 onto ∅ ↔ f = ∅
26 22 25 bitrdi ⊢ k = 0 → f : 1 … k ⟶ 1-1 onto 1 … k ↔ f = ∅
27 26 abbidv ⊢ k = 0 → f | f : 1 … k ⟶ 1-1 onto 1 … k = f | f = ∅
28 df-sn ⊢ ∅ = f | f = ∅
29 27 28 eqtr4di ⊢ k = 0 → f | f : 1 … k ⟶ 1-1 onto 1 … k = ∅
30 20 29 xpeq12d ⊢ k = 0 → 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k = ∅ × ∅
31 0ex ⊢ ∅ ∈ V
32 31 31 xpsn ⊢ ∅ × ∅ = ∅ ∅
33 30 32 eqtr2di ⊢ k = 0 → ∅ ∅ = 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k
34 elsni ⊢ s ∈ ∅ ∅ → s = ∅ ∅
35 31 31 op1std ⊢ s = ∅ ∅ → 1 st ⁡ s = ∅
36 34 35 syl ⊢ s ∈ ∅ ∅ → 1 st ⁡ s = ∅
37 36 oveq1d ⊢ s ∈ ∅ ∅ → 1 st ⁡ s + f ∅ = ∅ + f ∅
38 f0 ⊢ ∅ : ∅ ⟶ ∅
39 ffn ⊢ ∅ : ∅ ⟶ ∅ → ∅ Fn ∅
40 38 39 mp1i ⊢ s ∈ ∅ ∅ → ∅ Fn ∅
41 31 a1i ⊢ s ∈ ∅ ∅ → ∅ ∈ V
42 inidm ⊢ ∅ ∩ ∅ = ∅
43 0fv ⊢ ∅ ⁡ n = ∅
44 43 a1i ⊢ s ∈ ∅ ∅ ∧ n ∈ ∅ → ∅ ⁡ n = ∅
45 40 40 41 41 42 44 44 offval ⊢ s ∈ ∅ ∅ → ∅ + f ∅ = n ∈ ∅ ⟼ ∅ + ∅
46 mpt0 ⊢ n ∈ ∅ ⟼ ∅ + ∅ = ∅
47 45 46 eqtrdi ⊢ s ∈ ∅ ∅ → ∅ + f ∅ = ∅
48 37 47 eqtrd ⊢ s ∈ ∅ ∅ → 1 st ⁡ s + f ∅ = ∅
49 48 uneq1d ⊢ s ∈ ∅ ∅ → 1 st ⁡ s + f ∅ ∪ 1 … N × 0 = ∅ ∪ 1 … N × 0
50 uncom ⊢ ∅ ∪ 1 … N × 0 = 1 … N × 0 ∪ ∅
51 un0 ⊢ 1 … N × 0 ∪ ∅ = 1 … N × 0
52 50 51 eqtri ⊢ ∅ ∪ 1 … N × 0 = 1 … N × 0
53 49 52 eqtr2di ⊢ s ∈ ∅ ∅ → 1 … N × 0 = 1 st ⁡ s + f ∅ ∪ 1 … N × 0
54 53 csbeq1d ⊢ s ∈ ∅ ∅ → ⦋ 1 … N × 0 / p⦌ B = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B
55 54 eqeq2d ⊢ s ∈ ∅ ∅ → 0 = ⦋ 1 … N × 0 / p⦌ B ↔ 0 = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B
56 oveq2 ⊢ k = 0 → 0 … k = 0 … 0
57 0z ⊢ 0 ∈ ℤ
58 fzsn ⊢ 0 ∈ ℤ → 0 … 0 = 0
59 57 58 ax-mp ⊢ 0 … 0 = 0
60 56 59 eqtrdi ⊢ k = 0 → 0 … k = 0
61 oveq2 ⊢ k = 0 → j + 1 … k = j + 1 … 0
62 61 imaeq2d ⊢ k = 0 → 2 nd ⁡ s j + 1 … k = 2 nd ⁡ s j + 1 … 0
63 62 xpeq1d ⊢ k = 0 → 2 nd ⁡ s j + 1 … k × 0 = 2 nd ⁡ s j + 1 … 0 × 0
64 63 uneq2d ⊢ k = 0 → 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 = 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0
65 64 oveq2d ⊢ k = 0 → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0
66 oveq1 ⊢ k = 0 → k + 1 = 0 + 1
67 0p1e1 ⊢ 0 + 1 = 1
68 66 67 eqtrdi ⊢ k = 0 → k + 1 = 1
69 68 oveq1d ⊢ k = 0 → k + 1 … N = 1 … N
70 69 xpeq1d ⊢ k = 0 → k + 1 … N × 0 = 1 … N × 0
71 65 70 uneq12d ⊢ k = 0 → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 ∪ 1 … N × 0
72 71 csbeq1d ⊢ k = 0 → ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 ∪ 1 … N × 0 / p⦌ B
73 72 eqeq2d ⊢ k = 0 → i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 ∪ 1 … N × 0 / p⦌ B
74 60 73 rexeqbidv ⊢ k = 0 → ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ∃ j ∈ 0 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 ∪ 1 … N × 0 / p⦌ B
75 c0ex ⊢ 0 ∈ V
76 oveq2 ⊢ j = 0 → 1 … j = 1 … 0
77 76 12 eqtrdi ⊢ j = 0 → 1 … j = ∅
78 77 imaeq2d ⊢ j = 0 → 2 nd ⁡ s 1 … j = 2 nd ⁡ s ∅
79 ima0 ⊢ 2 nd ⁡ s ∅ = ∅
80 78 79 eqtrdi ⊢ j = 0 → 2 nd ⁡ s 1 … j = ∅
81 80 xpeq1d ⊢ j = 0 → 2 nd ⁡ s 1 … j × 1 = ∅ × 1
82 0xp ⊢ ∅ × 1 = ∅
83 81 82 eqtrdi ⊢ j = 0 → 2 nd ⁡ s 1 … j × 1 = ∅
84 oveq1 ⊢ j = 0 → j + 1 = 0 + 1
85 84 67 eqtrdi ⊢ j = 0 → j + 1 = 1
86 85 oveq1d ⊢ j = 0 → j + 1 … 0 = 1 … 0
87 86 12 eqtrdi ⊢ j = 0 → j + 1 … 0 = ∅
88 87 imaeq2d ⊢ j = 0 → 2 nd ⁡ s j + 1 … 0 = 2 nd ⁡ s ∅
89 88 79 eqtrdi ⊢ j = 0 → 2 nd ⁡ s j + 1 … 0 = ∅
90 89 xpeq1d ⊢ j = 0 → 2 nd ⁡ s j + 1 … 0 × 0 = ∅ × 0
91 0xp ⊢ ∅ × 0 = ∅
92 90 91 eqtrdi ⊢ j = 0 → 2 nd ⁡ s j + 1 … 0 × 0 = ∅
93 83 92 uneq12d ⊢ j = 0 → 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 = ∅ ∪ ∅
94 un0 ⊢ ∅ ∪ ∅ = ∅
95 93 94 eqtrdi ⊢ j = 0 → 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 = ∅
96 95 oveq2d ⊢ j = 0 → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 = 1 st ⁡ s + f ∅
97 96 uneq1d ⊢ j = 0 → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 ∪ 1 … N × 0 = 1 st ⁡ s + f ∅ ∪ 1 … N × 0
98 97 csbeq1d ⊢ j = 0 → ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 ∪ 1 … N × 0 / p⦌ B = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B
99 98 eqeq2d ⊢ j = 0 → i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 ∪ 1 … N × 0 / p⦌ B ↔ i = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B
100 75 99 rexsn ⊢ ∃ j ∈ 0 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … 0 × 0 ∪ 1 … N × 0 / p⦌ B ↔ i = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B
101 74 100 bitrdi ⊢ k = 0 → ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ i = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B
102 60 101 raleqbidv ⊢ k = 0 → ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ∀ i ∈ 0 i = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B
103 eqeq1 ⊢ i = 0 → i = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B ↔ 0 = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B
104 75 103 ralsn ⊢ ∀ i ∈ 0 i = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B ↔ 0 = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B
105 102 104 bitr2di ⊢ k = 0 → 0 = ⦋ 1 st ⁡ s + f ∅ ∪ 1 … N × 0 / p⦌ B ↔ ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B
106 55 105 sylan9bbr ⊢ k = 0 ∧ s ∈ ∅ ∅ → 0 = ⦋ 1 … N × 0 / p⦌ B ↔ ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B
107 33 106 rabeqbidva ⊢ k = 0 → s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B
108 107 eqcomd ⊢ k = 0 → s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
109 108 fveq2d ⊢ k = 0 → s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
110 109 breq2d ⊢ k = 0 → 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ 2 ∥ s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
111 110 notbid ⊢ k = 0 → ¬ 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ¬ 2 ∥ s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
112 111 imbi2d ⊢ k = 0 → φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ φ → ¬ 2 ∥ s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
113 oveq2 ⊢ k = m → 1 … k = 1 … m
114 113 oveq2d ⊢ k = m → 0 ..^ K 1 … k = 0 ..^ K 1 … m
115 eqidd ⊢ k = m → f = f
116 115 113 113 f1oeq123d ⊢ k = m → f : 1 … k ⟶ 1-1 onto 1 … k ↔ f : 1 … m ⟶ 1-1 onto 1 … m
117 116 abbidv ⊢ k = m → f | f : 1 … k ⟶ 1-1 onto 1 … k = f | f : 1 … m ⟶ 1-1 onto 1 … m
118 114 117 xpeq12d ⊢ k = m → 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k = 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m
119 oveq2 ⊢ k = m → 0 … k = 0 … m
120 oveq2 ⊢ k = m → j + 1 … k = j + 1 … m
121 120 imaeq2d ⊢ k = m → 2 nd ⁡ s j + 1 … k = 2 nd ⁡ s j + 1 … m
122 121 xpeq1d ⊢ k = m → 2 nd ⁡ s j + 1 … k × 0 = 2 nd ⁡ s j + 1 … m × 0
123 122 uneq2d ⊢ k = m → 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 = 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0
124 123 oveq2d ⊢ k = m → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0
125 oveq1 ⊢ k = m → k + 1 = m + 1
126 125 oveq1d ⊢ k = m → k + 1 … N = m + 1 … N
127 126 xpeq1d ⊢ k = m → k + 1 … N × 0 = m + 1 … N × 0
128 124 127 uneq12d ⊢ k = m → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0
129 128 csbeq1d ⊢ k = m → ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
130 129 eqeq2d ⊢ k = m → i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
131 119 130 rexeqbidv ⊢ k = m → ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
132 119 131 raleqbidv ⊢ k = m → ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
133 118 132 rabeqbidv ⊢ k = m → s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
134 133 fveq2d ⊢ k = m → s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
135 134 breq2d ⊢ k = m → 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ 2 ∥ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
136 135 notbid ⊢ k = m → ¬ 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ¬ 2 ∥ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
137 136 imbi2d ⊢ k = m → φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
138 oveq2 ⊢ k = m + 1 → 1 … k = 1 … m + 1
139 138 oveq2d ⊢ k = m + 1 → 0 ..^ K 1 … k = 0 ..^ K 1 … m + 1
140 eqidd ⊢ k = m + 1 → f = f
141 140 138 138 f1oeq123d ⊢ k = m + 1 → f : 1 … k ⟶ 1-1 onto 1 … k ↔ f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1
142 141 abbidv ⊢ k = m + 1 → f | f : 1 … k ⟶ 1-1 onto 1 … k = f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1
143 139 142 xpeq12d ⊢ k = m + 1 → 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k = 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1
144 oveq2 ⊢ k = m + 1 → 0 … k = 0 … m + 1
145 oveq2 ⊢ k = m + 1 → j + 1 … k = j + 1 … m + 1
146 145 imaeq2d ⊢ k = m + 1 → 2 nd ⁡ s j + 1 … k = 2 nd ⁡ s j + 1 … m + 1
147 146 xpeq1d ⊢ k = m + 1 → 2 nd ⁡ s j + 1 … k × 0 = 2 nd ⁡ s j + 1 … m + 1 × 0
148 147 uneq2d ⊢ k = m + 1 → 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 = 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0
149 148 oveq2d ⊢ k = m + 1 → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0
150 oveq1 ⊢ k = m + 1 → k + 1 = m + 1 + 1
151 150 oveq1d ⊢ k = m + 1 → k + 1 … N = m + 1 + 1 … N
152 151 xpeq1d ⊢ k = m + 1 → k + 1 … N × 0 = m + 1 + 1 … N × 0
153 149 152 uneq12d ⊢ k = m + 1 → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0
154 153 csbeq1d ⊢ k = m + 1 → ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
155 154 eqeq2d ⊢ k = m + 1 → i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
156 144 155 rexeqbidv ⊢ k = m + 1 → ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
157 144 156 raleqbidv ⊢ k = m + 1 → ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
158 143 157 rabeqbidv ⊢ k = m + 1 → s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
159 158 fveq2d ⊢ k = m + 1 → s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
160 159 breq2d ⊢ k = m + 1 → 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
161 160 notbid ⊢ k = m + 1 → ¬ 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ¬ 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
162 161 imbi2d ⊢ k = m + 1 → φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
163 oveq2 ⊢ k = N → 1 … k = 1 … N
164 163 oveq2d ⊢ k = N → 0 ..^ K 1 … k = 0 ..^ K 1 … N
165 eqidd ⊢ k = N → f = f
166 165 163 163 f1oeq123d ⊢ k = N → f : 1 … k ⟶ 1-1 onto 1 … k ↔ f : 1 … N ⟶ 1-1 onto 1 … N
167 166 abbidv ⊢ k = N → f | f : 1 … k ⟶ 1-1 onto 1 … k = f | f : 1 … N ⟶ 1-1 onto 1 … N
168 164 167 xpeq12d ⊢ k = N → 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k = 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N
169 oveq2 ⊢ k = N → 0 … k = 0 … N
170 oveq2 ⊢ k = N → j + 1 … k = j + 1 … N
171 170 imaeq2d ⊢ k = N → 2 nd ⁡ s j + 1 … k = 2 nd ⁡ s j + 1 … N
172 171 xpeq1d ⊢ k = N → 2 nd ⁡ s j + 1 … k × 0 = 2 nd ⁡ s j + 1 … N × 0
173 172 uneq2d ⊢ k = N → 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 = 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0
174 173 oveq2d ⊢ k = N → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0
175 oveq1 ⊢ k = N → k + 1 = N + 1
176 175 oveq1d ⊢ k = N → k + 1 … N = N + 1 … N
177 176 xpeq1d ⊢ k = N → k + 1 … N × 0 = N + 1 … N × 0
178 174 177 uneq12d ⊢ k = N → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0
179 178 csbeq1d ⊢ k = N → ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
180 179 eqeq2d ⊢ k = N → i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
181 169 180 rexeqbidv ⊢ k = N → ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
182 169 181 raleqbidv ⊢ k = N → ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
183 168 182 rabeqbidv ⊢ k = N → s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
184 183 fveq2d ⊢ k = N → s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
185 184 breq2d ⊢ k = N → 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ 2 ∥ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
186 185 notbid ⊢ k = N → ¬ 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ ¬ 2 ∥ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
187 186 imbi2d ⊢ k = N → φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … k × f | f : 1 … k ⟶ 1-1 onto 1 … k | ∀ i ∈ 0 … k ∃ j ∈ 0 … k i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … k × 0 ∪ k + 1 … N × 0 / p⦌ B ↔ φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
188 n2dvds1 ⊢ ¬ 2 ∥ 1
189 opex ⊢ ∅ ∅ ∈ V
190 hashsng ⊢ ∅ ∅ ∈ V → ∅ ∅ = 1
191 189 190 ax-mp ⊢ ∅ ∅ = 1
192 nnuz ⊢ ℕ = ℤ ≥ 1
193 1 192 eleqtrdi ⊢ φ → N ∈ ℤ ≥ 1
194 eluzfz1 ⊢ N ∈ ℤ ≥ 1 → 1 ∈ 1 … N
195 193 194 syl ⊢ φ → 1 ∈ 1 … N
196 6 nnnn0d ⊢ φ → K ∈ ℕ 0
197 0elfz ⊢ K ∈ ℕ 0 → 0 ∈ 0 … K
198 fconst6g ⊢ 0 ∈ 0 … K → 1 … N × 0 : 1 … N ⟶ 0 … K
199 196 197 198 3syl ⊢ φ → 1 … N × 0 : 1 … N ⟶ 0 … K
200 75 fvconst2 ⊢ 1 ∈ 1 … N → 1 … N × 0 ⁡ 1 = 0
201 195 200 syl ⊢ φ → 1 … N × 0 ⁡ 1 = 0
202 195 199 201 3jca ⊢ φ → 1 ∈ 1 … N ∧ 1 … N × 0 : 1 … N ⟶ 0 … K ∧ 1 … N × 0 ⁡ 1 = 0
203 nfv ⊢ Ⅎ p φ ∧ 1 ∈ 1 … N ∧ 1 … N × 0 : 1 … N ⟶ 0 … K ∧ 1 … N × 0 ⁡ 1 = 0
204 nfcsb1v ⊢ Ⅎ _ p ⦋ 1 … N × 0 / p⦌ B
205 204 nfeq1 ⊢ Ⅎ p ⦋ 1 … N × 0 / p⦌ B = 0
206 203 205 nfim ⊢ Ⅎ p φ ∧ 1 ∈ 1 … N ∧ 1 … N × 0 : 1 … N ⟶ 0 … K ∧ 1 … N × 0 ⁡ 1 = 0 → ⦋ 1 … N × 0 / p⦌ B = 0
207 ovex ⊢ 1 … N ∈ V
208 snex ⊢ 0 ∈ V
209 207 208 xpex ⊢ 1 … N × 0 ∈ V
210 feq1 ⊢ p = 1 … N × 0 → p : 1 … N ⟶ 0 … K ↔ 1 … N × 0 : 1 … N ⟶ 0 … K
211 fveq1 ⊢ p = 1 … N × 0 → p ⁡ 1 = 1 … N × 0 ⁡ 1
212 211 eqeq1d ⊢ p = 1 … N × 0 → p ⁡ 1 = 0 ↔ 1 … N × 0 ⁡ 1 = 0
213 210 212 3anbi23d ⊢ p = 1 … N × 0 → 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ 1 = 0 ↔ 1 ∈ 1 … N ∧ 1 … N × 0 : 1 … N ⟶ 0 … K ∧ 1 … N × 0 ⁡ 1 = 0
214 213 anbi2d ⊢ p = 1 … N × 0 → φ ∧ 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ 1 = 0 ↔ φ ∧ 1 ∈ 1 … N ∧ 1 … N × 0 : 1 … N ⟶ 0 … K ∧ 1 … N × 0 ⁡ 1 = 0
215 csbeq1a ⊢ p = 1 … N × 0 → B = ⦋ 1 … N × 0 / p⦌ B
216 215 eqeq1d ⊢ p = 1 … N × 0 → B = 0 ↔ ⦋ 1 … N × 0 / p⦌ B = 0
217 214 216 imbi12d ⊢ p = 1 … N × 0 → φ ∧ 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ 1 = 0 → B = 0 ↔ φ ∧ 1 ∈ 1 … N ∧ 1 … N × 0 : 1 … N ⟶ 0 … K ∧ 1 … N × 0 ⁡ 1 = 0 → ⦋ 1 … N × 0 / p⦌ B = 0
218 1ex ⊢ 1 ∈ V
219 eleq1 ⊢ n = 1 → n ∈ 1 … N ↔ 1 ∈ 1 … N
220 fveqeq2 ⊢ n = 1 → p ⁡ n = 0 ↔ p ⁡ 1 = 0
221 219 220 3anbi13d ⊢ n = 1 → n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 ↔ 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ 1 = 0
222 221 anbi2d ⊢ n = 1 → φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 ↔ φ ∧ 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ 1 = 0
223 breq2 ⊢ n = 1 → B < n ↔ B < 1
224 222 223 imbi12d ⊢ n = 1 → φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 → B < n ↔ φ ∧ 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ 1 = 0 → B < 1
225 218 224 4 vtocl ⊢ φ ∧ 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ 1 = 0 → B < 1
226 elfznn0 ⊢ B ∈ 0 … N → B ∈ ℕ 0
227 nn0lt10b ⊢ B ∈ ℕ 0 → B < 1 ↔ B = 0
228 3 226 227 3syl ⊢ φ ∧ p : 1 … N ⟶ 0 … K → B < 1 ↔ B = 0
229 228 3ad2antr2 ⊢ φ ∧ 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ 1 = 0 → B < 1 ↔ B = 0
230 225 229 mpbid ⊢ φ ∧ 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ 1 = 0 → B = 0
231 206 209 217 230 vtoclf ⊢ φ ∧ 1 ∈ 1 … N ∧ 1 … N × 0 : 1 … N ⟶ 0 … K ∧ 1 … N × 0 ⁡ 1 = 0 → ⦋ 1 … N × 0 / p⦌ B = 0
232 202 231 mpdan ⊢ φ → ⦋ 1 … N × 0 / p⦌ B = 0
233 232 eqcomd ⊢ φ → 0 = ⦋ 1 … N × 0 / p⦌ B
234 233 ralrimivw ⊢ φ → ∀ s ∈ ∅ ∅ 0 = ⦋ 1 … N × 0 / p⦌ B
235 rabid2 ⊢ ∅ ∅ = s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B ↔ ∀ s ∈ ∅ ∅ 0 = ⦋ 1 … N × 0 / p⦌ B
236 234 235 sylibr ⊢ φ → ∅ ∅ = s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
237 236 fveq2d ⊢ φ → ∅ ∅ = s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
238 191 237 eqtr3id ⊢ φ → 1 = s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
239 238 breq2d ⊢ φ → 2 ∥ 1 ↔ 2 ∥ s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
240 188 239 mtbii ⊢ φ → ¬ 2 ∥ s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
241 240 a1i ⊢ N ∈ ℕ 0 → φ → ¬ 2 ∥ s ∈ ∅ ∅ | 0 = ⦋ 1 … N × 0 / p⦌ B
242 2z ⊢ 2 ∈ ℤ
243 fzfi ⊢ 1 … m + 1 ∈ Fin
244 mapfi ⊢ 0 ..^ K ∈ Fin ∧ 1 … m + 1 ∈ Fin → 0 ..^ K 1 … m + 1 ∈ Fin
245 15 243 244 mp2an ⊢ 0 ..^ K 1 … m + 1 ∈ Fin
246 ovex ⊢ 1 … m + 1 ∈ V
247 246 246 mapval ⊢ 1 … m + 1 1 … m + 1 = f | f : 1 … m + 1 ⟶ 1 … m + 1
248 mapfi ⊢ 1 … m + 1 ∈ Fin ∧ 1 … m + 1 ∈ Fin → 1 … m + 1 1 … m + 1 ∈ Fin
249 243 243 248 mp2an ⊢ 1 … m + 1 1 … m + 1 ∈ Fin
250 247 249 eqeltrri ⊢ f | f : 1 … m + 1 ⟶ 1 … m + 1 ∈ Fin
251 f1of ⊢ f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 → f : 1 … m + 1 ⟶ 1 … m + 1
252 251 ss2abi ⊢ f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ⊆ f | f : 1 … m + 1 ⟶ 1 … m + 1
253 ssfi ⊢ f | f : 1 … m + 1 ⟶ 1 … m + 1 ∈ Fin ∧ f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ⊆ f | f : 1 … m + 1 ⟶ 1 … m + 1 → f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ∈ Fin
254 250 252 253 mp2an ⊢ f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ∈ Fin
255 xpfi ⊢ 0 ..^ K 1 … m + 1 ∈ Fin ∧ f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ∈ Fin → 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ∈ Fin
256 245 254 255 mp2an ⊢ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ∈ Fin
257 rabfi ⊢ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ∈ Fin → s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ Fin
258 hashcl ⊢ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ Fin → s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℕ 0
259 256 257 258 mp2b ⊢ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℕ 0
260 259 nn0zi ⊢ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ
261 rabfi ⊢ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ∈ Fin → s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ Fin
262 hashcl ⊢ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ Fin → s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℕ 0
263 256 261 262 mp2b ⊢ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℕ 0
264 263 nn0zi ⊢ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℤ
265 242 260 264 3pm3.2i ⊢ 2 ∈ ℤ ∧ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ ∧ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℤ
266 nn0p1nn ⊢ m ∈ ℕ 0 → m + 1 ∈ ℕ
267 266 ad2antrl ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → m + 1 ∈ ℕ
268 uneq1 ⊢ q = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 → q ∪ m + 1 + 1 … N × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0
269 268 csbeq1d ⊢ q = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
270 75 fconst ⊢ m + 1 + 1 … N × 0 : m + 1 + 1 … N ⟶ 0
271 270 jctr ⊢ q : 1 … m + 1 ⟶ 0 … K → q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 + 1 … N × 0 : m + 1 + 1 … N ⟶ 0
272 266 nnred ⊢ m ∈ ℕ 0 → m + 1 ∈ ℝ
273 272 ltp1d ⊢ m ∈ ℕ 0 → m + 1 < m + 1 + 1
274 fzdisj ⊢ m + 1 < m + 1 + 1 → 1 … m + 1 ∩ m + 1 + 1 … N = ∅
275 273 274 syl ⊢ m ∈ ℕ 0 → 1 … m + 1 ∩ m + 1 + 1 … N = ∅
276 fun ⊢ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 + 1 … N × 0 : m + 1 + 1 … N ⟶ 0 ∧ 1 … m + 1 ∩ m + 1 + 1 … N = ∅ → q ∪ m + 1 + 1 … N × 0 : 1 … m + 1 ∪ m + 1 + 1 … N ⟶ 0 … K ∪ 0
277 271 275 276 syl2anr ⊢ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K → q ∪ m + 1 + 1 … N × 0 : 1 … m + 1 ∪ m + 1 + 1 … N ⟶ 0 … K ∪ 0
278 277 adantlr ⊢ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → q ∪ m + 1 + 1 … N × 0 : 1 … m + 1 ∪ m + 1 + 1 … N ⟶ 0 … K ∪ 0
279 278 adantl ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → q ∪ m + 1 + 1 … N × 0 : 1 … m + 1 ∪ m + 1 + 1 … N ⟶ 0 … K ∪ 0
280 266 peano2nnd ⊢ m ∈ ℕ 0 → m + 1 + 1 ∈ ℕ
281 280 192 eleqtrdi ⊢ m ∈ ℕ 0 → m + 1 + 1 ∈ ℤ ≥ 1
282 281 ad2antrl ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → m + 1 + 1 ∈ ℤ ≥ 1
283 nn0z ⊢ m ∈ ℕ 0 → m ∈ ℤ
284 1 nnzd ⊢ φ → N ∈ ℤ
285 zltp1le ⊢ m ∈ ℤ ∧ N ∈ ℤ → m < N ↔ m + 1 ≤ N
286 283 284 285 syl2anr ⊢ φ ∧ m ∈ ℕ 0 → m < N ↔ m + 1 ≤ N
287 286 biimpa ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → m + 1 ≤ N
288 287 anasss ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → m + 1 ≤ N
289 283 peano2zd ⊢ m ∈ ℕ 0 → m + 1 ∈ ℤ
290 289 adantr ⊢ m ∈ ℕ 0 ∧ m < N → m + 1 ∈ ℤ
291 eluz ⊢ m + 1 ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ ≥ m + 1 ↔ m + 1 ≤ N
292 290 284 291 syl2anr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → N ∈ ℤ ≥ m + 1 ↔ m + 1 ≤ N
293 288 292 mpbird ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → N ∈ ℤ ≥ m + 1
294 fzsplit2 ⊢ m + 1 + 1 ∈ ℤ ≥ 1 ∧ N ∈ ℤ ≥ m + 1 → 1 … N = 1 … m + 1 ∪ m + 1 + 1 … N
295 282 293 294 syl2anc ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 1 … N = 1 … m + 1 ∪ m + 1 + 1 … N
296 295 eqcomd ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 1 … m + 1 ∪ m + 1 + 1 … N = 1 … N
297 196 197 syl ⊢ φ → 0 ∈ 0 … K
298 297 snssd ⊢ φ → 0 ⊆ 0 … K
299 ssequn2 ⊢ 0 ⊆ 0 … K ↔ 0 … K ∪ 0 = 0 … K
300 298 299 sylib ⊢ φ → 0 … K ∪ 0 = 0 … K
301 300 adantr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 0 … K ∪ 0 = 0 … K
302 296 301 feq23d ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → q ∪ m + 1 + 1 … N × 0 : 1 … m + 1 ∪ m + 1 + 1 … N ⟶ 0 … K ∪ 0 ↔ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
303 302 adantrr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → q ∪ m + 1 + 1 … N × 0 : 1 … m + 1 ∪ m + 1 + 1 … N ⟶ 0 … K ∪ 0 ↔ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
304 279 303 mpbid ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
305 nfv ⊢ Ⅎ p φ ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
306 nfcsb1v ⊢ Ⅎ _ p ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B
307 306 nfel1 ⊢ Ⅎ p ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N
308 305 307 nfim ⊢ Ⅎ p φ ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N
309 vex ⊢ q ∈ V
310 ovex ⊢ m + 1 + 1 … N ∈ V
311 310 208 xpex ⊢ m + 1 + 1 … N × 0 ∈ V
312 309 311 unex ⊢ q ∪ m + 1 + 1 … N × 0 ∈ V
313 feq1 ⊢ p = q ∪ m + 1 + 1 … N × 0 → p : 1 … N ⟶ 0 … K ↔ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
314 313 anbi2d ⊢ p = q ∪ m + 1 + 1 … N × 0 → φ ∧ p : 1 … N ⟶ 0 … K ↔ φ ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
315 csbeq1a ⊢ p = q ∪ m + 1 + 1 … N × 0 → B = ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B
316 315 eleq1d ⊢ p = q ∪ m + 1 + 1 … N × 0 → B ∈ 0 … N ↔ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N
317 314 316 imbi12d ⊢ p = q ∪ m + 1 + 1 … N × 0 → φ ∧ p : 1 … N ⟶ 0 … K → B ∈ 0 … N ↔ φ ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N
318 308 312 317 3 vtoclf ⊢ φ ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N
319 304 318 syldan ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N
320 319 anassrs ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N
321 elfznn0 ⊢ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℕ 0
322 320 321 syl ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℕ 0
323 266 nnnn0d ⊢ m ∈ ℕ 0 → m + 1 ∈ ℕ 0
324 323 adantr ⊢ m ∈ ℕ 0 ∧ m < N → m + 1 ∈ ℕ 0
325 324 ad2antlr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → m + 1 ∈ ℕ 0
326 leloe ⊢ m + 1 ∈ ℝ ∧ N ∈ ℝ → m + 1 ≤ N ↔ m + 1 < N ∨ m + 1 = N
327 272 8 326 syl2anr ⊢ φ ∧ m ∈ ℕ 0 → m + 1 ≤ N ↔ m + 1 < N ∨ m + 1 = N
328 286 327 bitrd ⊢ φ ∧ m ∈ ℕ 0 → m < N ↔ m + 1 < N ∨ m + 1 = N
329 328 biimpd ⊢ φ ∧ m ∈ ℕ 0 → m < N → m + 1 < N ∨ m + 1 = N
330 329 imdistani ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → φ ∧ m ∈ ℕ 0 ∧ m + 1 < N ∨ m + 1 = N
331 330 anasss ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → φ ∧ m ∈ ℕ 0 ∧ m + 1 < N ∨ m + 1 = N
332 simplll ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → φ
333 280 nnge1d ⊢ m ∈ ℕ 0 → 1 ≤ m + 1 + 1
334 333 ad2antlr ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → 1 ≤ m + 1 + 1
335 zltp1le ⊢ m + 1 ∈ ℤ ∧ N ∈ ℤ → m + 1 < N ↔ m + 1 + 1 ≤ N
336 289 284 335 syl2anr ⊢ φ ∧ m ∈ ℕ 0 → m + 1 < N ↔ m + 1 + 1 ≤ N
337 336 biimpa ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → m + 1 + 1 ≤ N
338 289 peano2zd ⊢ m ∈ ℕ 0 → m + 1 + 1 ∈ ℤ
339 1z ⊢ 1 ∈ ℤ
340 elfz ⊢ m + 1 + 1 ∈ ℤ ∧ 1 ∈ ℤ ∧ N ∈ ℤ → m + 1 + 1 ∈ 1 … N ↔ 1 ≤ m + 1 + 1 ∧ m + 1 + 1 ≤ N
341 339 340 mp3an2 ⊢ m + 1 + 1 ∈ ℤ ∧ N ∈ ℤ → m + 1 + 1 ∈ 1 … N ↔ 1 ≤ m + 1 + 1 ∧ m + 1 + 1 ≤ N
342 338 284 341 syl2anr ⊢ φ ∧ m ∈ ℕ 0 → m + 1 + 1 ∈ 1 … N ↔ 1 ≤ m + 1 + 1 ∧ m + 1 + 1 ≤ N
343 342 adantr ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → m + 1 + 1 ∈ 1 … N ↔ 1 ≤ m + 1 + 1 ∧ m + 1 + 1 ≤ N
344 334 337 343 mpbir2and ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → m + 1 + 1 ∈ 1 … N
345 344 adantlr ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → m + 1 + 1 ∈ 1 … N
346 nn0re ⊢ m ∈ ℕ 0 → m ∈ ℝ
347 346 ad2antlr ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → m ∈ ℝ
348 272 ad2antlr ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → m + 1 ∈ ℝ
349 8 ad2antrr ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → N ∈ ℝ
350 346 ltp1d ⊢ m ∈ ℕ 0 → m < m + 1
351 350 ad2antlr ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → m < m + 1
352 simpr ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → m + 1 < N
353 347 348 349 351 352 lttrd ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → m < N
354 353 adantlr ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → m < N
355 anass ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ↔ φ ∧ m ∈ ℕ 0 ∧ m < N
356 304 anassrs ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
357 355 356 sylanb ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
358 357 an32s ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m < N → q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
359 354 358 syldan ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
360 ffn ⊢ q : 1 … m + 1 ⟶ 0 … K → q Fn 1 … m + 1
361 360 ad2antlr ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → q Fn 1 … m + 1
362 275 ad3antlr ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → 1 … m + 1 ∩ m + 1 + 1 … N = ∅
363 eluz ⊢ m + 1 + 1 ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ ≥ m + 1 + 1 ↔ m + 1 + 1 ≤ N
364 338 284 363 syl2anr ⊢ φ ∧ m ∈ ℕ 0 → N ∈ ℤ ≥ m + 1 + 1 ↔ m + 1 + 1 ≤ N
365 364 adantr ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → N ∈ ℤ ≥ m + 1 + 1 ↔ m + 1 + 1 ≤ N
366 337 365 mpbird ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → N ∈ ℤ ≥ m + 1 + 1
367 eluzfz1 ⊢ N ∈ ℤ ≥ m + 1 + 1 → m + 1 + 1 ∈ m + 1 + 1 … N
368 366 367 syl ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N → m + 1 + 1 ∈ m + 1 + 1 … N
369 368 adantlr ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → m + 1 + 1 ∈ m + 1 + 1 … N
370 fnconstg ⊢ 0 ∈ V → m + 1 + 1 … N × 0 Fn m + 1 + 1 … N
371 75 370 ax-mp ⊢ m + 1 + 1 … N × 0 Fn m + 1 + 1 … N
372 fvun2 ⊢ q Fn 1 … m + 1 ∧ m + 1 + 1 … N × 0 Fn m + 1 + 1 … N ∧ 1 … m + 1 ∩ m + 1 + 1 … N = ∅ ∧ m + 1 + 1 ∈ m + 1 + 1 … N → q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = m + 1 + 1 … N × 0 ⁡ m + 1 + 1
373 371 372 mp3an2 ⊢ q Fn 1 … m + 1 ∧ 1 … m + 1 ∩ m + 1 + 1 … N = ∅ ∧ m + 1 + 1 ∈ m + 1 + 1 … N → q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = m + 1 + 1 … N × 0 ⁡ m + 1 + 1
374 361 362 369 373 syl12anc ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = m + 1 + 1 … N × 0 ⁡ m + 1 + 1
375 75 fvconst2 ⊢ m + 1 + 1 ∈ m + 1 + 1 … N → m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = 0
376 369 375 syl ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = 0
377 374 376 eqtrd ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = 0
378 nfv ⊢ Ⅎ p φ ∧ m + 1 + 1 ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = 0
379 nfcv ⊢ Ⅎ _ p <
380 nfcv ⊢ Ⅎ _ p m + 1 + 1
381 306 379 380 nfbr ⊢ Ⅎ p ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < m + 1 + 1
382 378 381 nfim ⊢ Ⅎ p φ ∧ m + 1 + 1 ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = 0 → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < m + 1 + 1
383 fveq1 ⊢ p = q ∪ m + 1 + 1 … N × 0 → p ⁡ m + 1 + 1 = q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1
384 383 eqeq1d ⊢ p = q ∪ m + 1 + 1 … N × 0 → p ⁡ m + 1 + 1 = 0 ↔ q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = 0
385 313 384 3anbi23d ⊢ p = q ∪ m + 1 + 1 … N × 0 → m + 1 + 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ m + 1 + 1 = 0 ↔ m + 1 + 1 ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = 0
386 385 anbi2d ⊢ p = q ∪ m + 1 + 1 … N × 0 → φ ∧ m + 1 + 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ m + 1 + 1 = 0 ↔ φ ∧ m + 1 + 1 ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = 0
387 315 breq1d ⊢ p = q ∪ m + 1 + 1 … N × 0 → B < m + 1 + 1 ↔ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < m + 1 + 1
388 386 387 imbi12d ⊢ p = q ∪ m + 1 + 1 … N × 0 → φ ∧ m + 1 + 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ m + 1 + 1 = 0 → B < m + 1 + 1 ↔ φ ∧ m + 1 + 1 ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = 0 → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < m + 1 + 1
389 ovex ⊢ m + 1 + 1 ∈ V
390 eleq1 ⊢ n = m + 1 + 1 → n ∈ 1 … N ↔ m + 1 + 1 ∈ 1 … N
391 fveqeq2 ⊢ n = m + 1 + 1 → p ⁡ n = 0 ↔ p ⁡ m + 1 + 1 = 0
392 390 391 3anbi13d ⊢ n = m + 1 + 1 → n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 ↔ m + 1 + 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ m + 1 + 1 = 0
393 392 anbi2d ⊢ n = m + 1 + 1 → φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 ↔ φ ∧ m + 1 + 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ m + 1 + 1 = 0
394 breq2 ⊢ n = m + 1 + 1 → B < n ↔ B < m + 1 + 1
395 393 394 imbi12d ⊢ n = m + 1 + 1 → φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 → B < n ↔ φ ∧ m + 1 + 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ m + 1 + 1 = 0 → B < m + 1 + 1
396 389 395 4 vtocl ⊢ φ ∧ m + 1 + 1 ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ m + 1 + 1 = 0 → B < m + 1 + 1
397 382 312 388 396 vtoclf ⊢ φ ∧ m + 1 + 1 ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ m + 1 + 1 = 0 → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < m + 1 + 1
398 332 345 359 377 397 syl13anc ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < m + 1 + 1
399 355 320 sylanb ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N
400 399 an32s ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m < N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N
401 400 elfzelzd ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m < N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ
402 354 401 syldan ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ
403 289 ad3antlr ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → m + 1 ∈ ℤ
404 zleltp1 ⊢ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ ∧ m + 1 ∈ ℤ → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ m + 1 ↔ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < m + 1 + 1
405 402 403 404 syl2anc ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ m + 1 ↔ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < m + 1 + 1
406 398 405 mpbird ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ m + 1
407 350 ad2antlr ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K → m < m + 1
408 breq2 ⊢ m + 1 = N → m < m + 1 ↔ m < N
409 408 biimpac ⊢ m < m + 1 ∧ m + 1 = N → m < N
410 407 409 sylan ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 = N → m < N
411 elfzle2 ⊢ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ N
412 400 411 syl ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m < N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ N
413 410 412 syldan ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 = N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ N
414 simpr ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 = N → m + 1 = N
415 413 414 breqtrrd ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 = N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ m + 1
416 406 415 jaodan ⊢ φ ∧ m ∈ ℕ 0 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ m + 1 < N ∨ m + 1 = N → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ m + 1
417 416 an32s ⊢ φ ∧ m ∈ ℕ 0 ∧ m + 1 < N ∨ m + 1 = N ∧ q : 1 … m + 1 ⟶ 0 … K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ m + 1
418 331 417 sylan ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ m + 1
419 elfz2nn0 ⊢ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … m + 1 ↔ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℕ 0 ∧ m + 1 ∈ ℕ 0 ∧ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≤ m + 1
420 322 325 418 419 syl3anbrc ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ q : 1 … m + 1 ⟶ 0 … K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ 0 … m + 1
421 fzss2 ⊢ N ∈ ℤ ≥ m + 1 → 1 … m + 1 ⊆ 1 … N
422 293 421 syl ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 1 … m + 1 ⊆ 1 … N
423 422 sselda ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 → n ∈ 1 … N
424 423 3ad2antr1 ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = 0 → n ∈ 1 … N
425 356 3ad2antr2 ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = 0 → q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
426 360 ad2antll ⊢ φ ∧ m ∈ ℕ 0 ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K → q Fn 1 … m + 1
427 275 ad2antlr ⊢ φ ∧ m ∈ ℕ 0 ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K → 1 … m + 1 ∩ m + 1 + 1 … N = ∅
428 simprl ⊢ φ ∧ m ∈ ℕ 0 ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K → n ∈ 1 … m + 1
429 fvun1 ⊢ q Fn 1 … m + 1 ∧ m + 1 + 1 … N × 0 Fn m + 1 + 1 … N ∧ 1 … m + 1 ∩ m + 1 + 1 … N = ∅ ∧ n ∈ 1 … m + 1 → q ∪ m + 1 + 1 … N × 0 ⁡ n = q ⁡ n
430 371 429 mp3an2 ⊢ q Fn 1 … m + 1 ∧ 1 … m + 1 ∩ m + 1 + 1 … N = ∅ ∧ n ∈ 1 … m + 1 → q ∪ m + 1 + 1 … N × 0 ⁡ n = q ⁡ n
431 426 427 428 430 syl12anc ⊢ φ ∧ m ∈ ℕ 0 ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K → q ∪ m + 1 + 1 … N × 0 ⁡ n = q ⁡ n
432 431 adantlrr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K → q ∪ m + 1 + 1 … N × 0 ⁡ n = q ⁡ n
433 432 3adantr3 ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = 0 → q ∪ m + 1 + 1 … N × 0 ⁡ n = q ⁡ n
434 simpr3 ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = 0 → q ⁡ n = 0
435 433 434 eqtrd ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = 0 → q ∪ m + 1 + 1 … N × 0 ⁡ n = 0
436 424 425 435 3jca ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = 0 → n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = 0
437 nfv ⊢ Ⅎ p φ ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = 0
438 nfcv ⊢ Ⅎ _ p n
439 306 379 438 nfbr ⊢ Ⅎ p ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < n
440 437 439 nfim ⊢ Ⅎ p φ ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = 0 → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < n
441 fveq1 ⊢ p = q ∪ m + 1 + 1 … N × 0 → p ⁡ n = q ∪ m + 1 + 1 … N × 0 ⁡ n
442 441 eqeq1d ⊢ p = q ∪ m + 1 + 1 … N × 0 → p ⁡ n = 0 ↔ q ∪ m + 1 + 1 … N × 0 ⁡ n = 0
443 313 442 3anbi23d ⊢ p = q ∪ m + 1 + 1 … N × 0 → n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 ↔ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = 0
444 443 anbi2d ⊢ p = q ∪ m + 1 + 1 … N × 0 → φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 ↔ φ ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = 0
445 315 breq1d ⊢ p = q ∪ m + 1 + 1 … N × 0 → B < n ↔ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < n
446 444 445 imbi12d ⊢ p = q ∪ m + 1 + 1 … N × 0 → φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = 0 → B < n ↔ φ ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = 0 → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < n
447 440 312 446 4 vtoclf ⊢ φ ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = 0 → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < n
448 447 adantlr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = 0 → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < n
449 436 448 syldan ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = 0 → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B < n
450 simp1 ⊢ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → n ∈ 1 … m + 1
451 423 anasss ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 → n ∈ 1 … N
452 450 451 sylanr2 ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → n ∈ 1 … N
453 simp2 ⊢ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → q : 1 … m + 1 ⟶ 0 … K
454 453 304 sylanr2 ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K
455 431 3adantr3 ⊢ φ ∧ m ∈ ℕ 0 ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → q ∪ m + 1 + 1 … N × 0 ⁡ n = q ⁡ n
456 simpr3 ⊢ φ ∧ m ∈ ℕ 0 ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → q ⁡ n = K
457 455 456 eqtrd ⊢ φ ∧ m ∈ ℕ 0 ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → q ∪ m + 1 + 1 … N × 0 ⁡ n = K
458 457 anasss ⊢ φ ∧ m ∈ ℕ 0 ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → q ∪ m + 1 + 1 … N × 0 ⁡ n = K
459 458 adantrlr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → q ∪ m + 1 + 1 … N × 0 ⁡ n = K
460 452 454 459 3jca ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = K
461 nfv ⊢ Ⅎ p φ ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = K
462 nfcv ⊢ Ⅎ _ p n − 1
463 306 462 nfne ⊢ Ⅎ p ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≠ n − 1
464 461 463 nfim ⊢ Ⅎ p φ ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≠ n − 1
465 441 eqeq1d ⊢ p = q ∪ m + 1 + 1 … N × 0 → p ⁡ n = K ↔ q ∪ m + 1 + 1 … N × 0 ⁡ n = K
466 313 465 3anbi23d ⊢ p = q ∪ m + 1 + 1 … N × 0 → n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = K ↔ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = K
467 466 anbi2d ⊢ p = q ∪ m + 1 + 1 … N × 0 → φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = K ↔ φ ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = K
468 315 neeq1d ⊢ p = q ∪ m + 1 + 1 … N × 0 → B ≠ n − 1 ↔ ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≠ n − 1
469 467 468 imbi12d ⊢ p = q ∪ m + 1 + 1 … N × 0 → φ ∧ n ∈ 1 … N ∧ p : 1 … N ⟶ 0 … K ∧ p ⁡ n = K → B ≠ n − 1 ↔ φ ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≠ n − 1
470 464 312 469 5 vtoclf ⊢ φ ∧ n ∈ 1 … N ∧ q ∪ m + 1 + 1 … N × 0 : 1 … N ⟶ 0 … K ∧ q ∪ m + 1 + 1 … N × 0 ⁡ n = K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≠ n − 1
471 460 470 syldan ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≠ n − 1
472 471 anassrs ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N ∧ n ∈ 1 … m + 1 ∧ q : 1 … m + 1 ⟶ 0 … K ∧ q ⁡ n = K → ⦋ q ∪ m + 1 + 1 … N × 0 / p⦌ B ≠ n − 1
473 267 269 420 449 472 poimirlem27 ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 2 ∥ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
474 267 269 420 poimirlem26 ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 2 ∥ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
475 fzfi ⊢ 0 … m + 1 ∈ Fin
476 xpfi ⊢ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ∈ Fin ∧ 0 … m + 1 ∈ Fin → 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 ∈ Fin
477 256 475 476 mp2an ⊢ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 ∈ Fin
478 rabfi ⊢ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 ∈ Fin → t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ Fin
479 hashcl ⊢ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ Fin → t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℕ 0
480 477 478 479 mp2b ⊢ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℕ 0
481 480 nn0zi ⊢ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ
482 zsubcl ⊢ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ ∧ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℤ → t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℤ
483 481 264 482 mp2an ⊢ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℤ
484 zsubcl ⊢ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ ∧ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ → t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ
485 481 260 484 mp2an ⊢ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ
486 dvds2sub ⊢ 2 ∈ ℤ ∧ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℤ ∧ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ → 2 ∥ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∧ 2 ∥ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B → 2 ∥ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B - s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 - t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
487 242 483 485 486 mp3an ⊢ 2 ∥ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∧ 2 ∥ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B → 2 ∥ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B - s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 - t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
488 473 474 487 syl2anc ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 2 ∥ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B - s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 - t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
489 480 nn0cni ⊢ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℂ
490 263 nn0cni ⊢ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℂ
491 259 nn0cni ⊢ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℂ
492 nnncan1 ⊢ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℂ ∧ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℂ ∧ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℂ → t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B - s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 - t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
493 489 490 491 492 mp3an ⊢ t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B - s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 - t ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 × 0 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 ∖ 2 nd ⁡ t i = ⦋ 1 st ⁡ t / s⦌ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
494 488 493 breqtrdi ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
495 dvdssub2 ⊢ 2 ∈ ℤ ∧ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∈ ℤ ∧ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ ℤ ∧ 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B − s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 → 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ↔ 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
496 265 494 495 sylancr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ↔ 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
497 nn0cn ⊢ m ∈ ℕ 0 → m ∈ ℂ
498 pncan1 ⊢ m ∈ ℂ → m + 1 - 1 = m
499 497 498 syl ⊢ m ∈ ℕ 0 → m + 1 - 1 = m
500 499 oveq2d ⊢ m ∈ ℕ 0 → 0 … m + 1 - 1 = 0 … m
501 500 rexeqdv ⊢ m ∈ ℕ 0 → ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ↔ ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
502 500 501 raleqbidv ⊢ m ∈ ℕ 0 → ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ↔ ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
503 502 3anbi1d ⊢ m ∈ ℕ 0 → ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ↔ ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
504 503 rabbidv ⊢ m ∈ ℕ 0 → s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 = s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
505 504 fveq2d ⊢ m ∈ ℕ 0 → s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 = s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
506 505 ad2antrl ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 = s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
507 1 adantr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → N ∈ ℕ
508 6 adantr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → K ∈ ℕ
509 simprl ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → m ∈ ℕ 0
510 simprr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → m < N
511 507 508 509 510 poimirlem4 ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B ≈ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
512 fzfi ⊢ 1 … m ∈ Fin
513 mapfi ⊢ 0 ..^ K ∈ Fin ∧ 1 … m ∈ Fin → 0 ..^ K 1 … m ∈ Fin
514 15 512 513 mp2an ⊢ 0 ..^ K 1 … m ∈ Fin
515 ovex ⊢ 1 … m ∈ V
516 515 515 mapval ⊢ 1 … m 1 … m = f | f : 1 … m ⟶ 1 … m
517 mapfi ⊢ 1 … m ∈ Fin ∧ 1 … m ∈ Fin → 1 … m 1 … m ∈ Fin
518 512 512 517 mp2an ⊢ 1 … m 1 … m ∈ Fin
519 516 518 eqeltrri ⊢ f | f : 1 … m ⟶ 1 … m ∈ Fin
520 f1of ⊢ f : 1 … m ⟶ 1-1 onto 1 … m → f : 1 … m ⟶ 1 … m
521 520 ss2abi ⊢ f | f : 1 … m ⟶ 1-1 onto 1 … m ⊆ f | f : 1 … m ⟶ 1 … m
522 ssfi ⊢ f | f : 1 … m ⟶ 1 … m ∈ Fin ∧ f | f : 1 … m ⟶ 1-1 onto 1 … m ⊆ f | f : 1 … m ⟶ 1 … m → f | f : 1 … m ⟶ 1-1 onto 1 … m ∈ Fin
523 519 521 522 mp2an ⊢ f | f : 1 … m ⟶ 1-1 onto 1 … m ∈ Fin
524 xpfi ⊢ 0 ..^ K 1 … m ∈ Fin ∧ f | f : 1 … m ⟶ 1-1 onto 1 … m ∈ Fin → 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m ∈ Fin
525 514 523 524 mp2an ⊢ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m ∈ Fin
526 rabfi ⊢ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m ∈ Fin → s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B ∈ Fin
527 525 526 ax-mp ⊢ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B ∈ Fin
528 rabfi ⊢ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 ∈ Fin → s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ Fin
529 256 528 ax-mp ⊢ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ Fin
530 hashen ⊢ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B ∈ Fin ∧ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ∈ Fin → s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ↔ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B ≈ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
531 527 529 530 mp2an ⊢ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ↔ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B ≈ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
532 511 531 sylibr ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1
533 506 532 eqtr4d ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 = s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
534 533 breq2d ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 - 1 ∃ j ∈ 0 … m + 1 - 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ∧ 1 st ⁡ s ⁡ m + 1 = 0 ∧ 2 nd ⁡ s ⁡ m + 1 = m + 1 ↔ 2 ∥ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
535 496 534 bitrd ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B ↔ 2 ∥ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
536 535 biimpd ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B → 2 ∥ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B
537 536 con3d ⊢ φ ∧ m ∈ ℕ 0 ∧ m < N → ¬ 2 ∥ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B → ¬ 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
538 537 expcom ⊢ m ∈ ℕ 0 ∧ m < N → φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B → ¬ 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
539 538 a2d ⊢ m ∈ ℕ 0 ∧ m < N → φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B → φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
540 539 3adant1 ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ 0 ∧ m < N → φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … m × f | f : 1 … m ⟶ 1-1 onto 1 … m | ∀ i ∈ 0 … m ∃ j ∈ 0 … m i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m × 0 ∪ m + 1 … N × 0 / p⦌ B → φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … m + 1 × f | f : 1 … m + 1 ⟶ 1-1 onto 1 … m + 1 | ∀ i ∈ 0 … m + 1 ∃ j ∈ 0 … m + 1 i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … m + 1 × 0 ∪ m + 1 + 1 … N × 0 / p⦌ B
541 112 137 162 187 241 540 fnn0ind ⊢ N ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ N ≤ N → φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
542 10 541 mpcom ⊢ φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
543 dvds0 ⊢ 2 ∈ ℤ → 2 ∥ 0
544 242 543 ax-mp ⊢ 2 ∥ 0
545 hash0 ⊢ ∅ = 0
546 544 545 breqtrri ⊢ 2 ∥ ∅
547 fveq2 ⊢ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C = ∅ → s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C = ∅
548 546 547 breqtrrid ⊢ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C = ∅ → 2 ∥ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C
549 8 ltp1d ⊢ φ → N < N + 1
550 284 peano2zd ⊢ φ → N + 1 ∈ ℤ
551 fzn ⊢ N + 1 ∈ ℤ ∧ N ∈ ℤ → N < N + 1 ↔ N + 1 … N = ∅
552 550 284 551 syl2anc ⊢ φ → N < N + 1 ↔ N + 1 … N = ∅
553 549 552 mpbid ⊢ φ → N + 1 … N = ∅
554 553 xpeq1d ⊢ φ → N + 1 … N × 0 = ∅ × 0
555 554 91 eqtrdi ⊢ φ → N + 1 … N × 0 = ∅
556 555 uneq2d ⊢ φ → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ ∅
557 un0 ⊢ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ ∅ = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0
558 556 557 eqtrdi ⊢ φ → 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 = 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0
559 558 csbeq1d ⊢ φ → ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 / p⦌ B
560 ovex ⊢ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∈ V
561 560 2 csbie ⊢ ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 / p⦌ B = C
562 559 561 eqtrdi ⊢ φ → ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B = C
563 562 eqeq2d ⊢ φ → i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B ↔ i = C
564 563 rexbidv ⊢ φ → ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B ↔ ∃ j ∈ 0 … N i = C
565 564 ralbidv ⊢ φ → ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B ↔ ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C
566 565 rabbidv ⊢ φ → s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C
567 566 fveq2d ⊢ φ → s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B = s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C
568 567 breq2d ⊢ φ → 2 ∥ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B ↔ 2 ∥ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C
569 548 568 imbitrrid ⊢ φ → s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C = ∅ → 2 ∥ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B
570 569 necon3bd ⊢ φ → ¬ 2 ∥ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = ⦋ 1 st ⁡ s + f 2 nd ⁡ s 1 … j × 1 ∪ 2 nd ⁡ s j + 1 … N × 0 ∪ N + 1 … N × 0 / p⦌ B → s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C ≠ ∅
571 542 570 mpd ⊢ φ → s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C ≠ ∅
572 rabn0 ⊢ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N | ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C ≠ ∅ ↔ ∃ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C
573 571 572 sylib ⊢ φ → ∃ s ∈ 0 ..^ K 1 … N × f | f : 1 … N ⟶ 1-1 onto 1 … N ∀ i ∈ 0 … N ∃ j ∈ 0 … N i = C