Step | Hyp | Ref
| Expression |
1 | | sticksstones11.1 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | | sticksstones11.2 |
. . . 4
⊢ (𝜑 → 𝐾 = 0) |
3 | | 0nn0 12258 |
. . . . 5
⊢ 0 ∈
ℕ0 |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
ℕ0) |
5 | 2, 4 | eqeltrd 2839 |
. . 3
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
6 | | sticksstones11.3 |
. . 3
⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) |
7 | | sticksstones11.5 |
. . 3
⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} |
8 | | sticksstones11.6 |
. . 3
⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} |
9 | 1, 5, 6, 7, 8 | sticksstones8 40117 |
. 2
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
10 | | sticksstones11.4 |
. . 3
⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) −
1)))))) |
11 | 1, 2, 10, 7, 8 | sticksstones9 40118 |
. 2
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
12 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) |
13 | | nfv 1917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢𝜑 |
14 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢{𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} |
15 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢{{〈1, 𝑁〉}} |
16 | | ffn 6592 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢:{1}⟶ℕ0
→ 𝑢 Fn
{1}) |
17 | 16 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢 Fn {1}) |
18 | | 1nn 11994 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℕ |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 1 ∈ ℕ) |
20 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑁 ∈
ℕ0) |
21 | | fnsng 6478 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℕ ∧ 𝑁
∈ ℕ0) → {〈1, 𝑁〉} Fn {1}) |
22 | 19, 20, 21 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → {〈1, 𝑁〉} Fn {1}) |
23 | | elsni 4578 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 ∈ {1} → 𝑝 = 1) |
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → 𝑝 = 1) |
25 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → 𝑝 = 1) |
26 | 25 | fveq2d 6770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → (𝑢‘𝑝) = (𝑢‘1)) |
27 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢:{1}⟶ℕ0) |
28 | | 1ex 10981 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 1 ∈
V |
29 | 28 | snid 4597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 1 ∈
{1} |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 1 ∈ {1}) |
31 | 27, 30 | ffvelrnd 6954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → (𝑢‘1) ∈
ℕ0) |
32 | 31 | nn0cnd 12305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → (𝑢‘1) ∈ ℂ) |
33 | | fveq2 6766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = 1 → (𝑢‘𝑖) = (𝑢‘1)) |
34 | 33 | sumsn 15468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((1
∈ ℕ ∧ (𝑢‘1) ∈ ℂ) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) |
35 | 19, 32, 34 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) |
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) |
37 | 36 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) → (𝑢‘1) = Σ𝑖 ∈ {1} (𝑢‘𝑖)) |
38 | | simplrr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁) |
39 | 37, 38 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) → (𝑢‘1) = 𝑁) |
40 | 39 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → (Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1) → (𝑢‘1) = 𝑁)) |
41 | 35, 40 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → (𝑢‘1) = 𝑁) |
42 | 41 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → (𝑢‘1) = 𝑁) |
43 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → 1 ∈
ℕ) |
44 | 20 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → 𝑁 ∈
ℕ0) |
45 | | fvsng 7044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((1
∈ ℕ ∧ 𝑁
∈ ℕ0) → ({〈1, 𝑁〉}‘1) = 𝑁) |
46 | 43, 44, 45 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → ({〈1, 𝑁〉}‘1) = 𝑁) |
47 | 46 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → 𝑁 = ({〈1, 𝑁〉}‘1)) |
48 | 42, 47 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → (𝑢‘1) = ({〈1, 𝑁〉}‘1)) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → (𝑢‘1) = ({〈1, 𝑁〉}‘1)) |
50 | 25 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → 1 = 𝑝) |
51 | 50 | fveq2d 6770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → ({〈1, 𝑁〉}‘1) = ({〈1, 𝑁〉}‘𝑝)) |
52 | 26, 49, 51 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → (𝑢‘𝑝) = ({〈1, 𝑁〉}‘𝑝)) |
53 | 24, 52 | mpdan 684 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → (𝑢‘𝑝) = ({〈1, 𝑁〉}‘𝑝)) |
54 | 17, 22, 53 | eqfnfvd 6904 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢 = {〈1, 𝑁〉}) |
55 | | fsng 7001 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℕ ∧ 𝑁
∈ ℕ0) → (𝑢:{1}⟶{𝑁} ↔ 𝑢 = {〈1, 𝑁〉})) |
56 | 19, 20, 55 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → (𝑢:{1}⟶{𝑁} ↔ 𝑢 = {〈1, 𝑁〉})) |
57 | 54, 56 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢:{1}⟶{𝑁}) |
58 | | ssidd 3943 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → {𝑁} ⊆ {𝑁}) |
59 | | fss 6609 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢:{1}⟶{𝑁} ∧ {𝑁} ⊆ {𝑁}) → 𝑢:{1}⟶{𝑁}) |
60 | 57, 58, 59 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢:{1}⟶{𝑁}) |
61 | 60, 58, 59 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢:{1}⟶{𝑁}) |
62 | 61, 56 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢 = {〈1, 𝑁〉}) |
63 | | vex 3433 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑢 ∈ V |
64 | 63 | elsn 4576 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ {{〈1, 𝑁〉}} ↔ 𝑢 = {〈1, 𝑁〉}) |
65 | 62, 64 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢 ∈ {{〈1, 𝑁〉}}) |
66 | 65 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁) → 𝑢 ∈ {{〈1, 𝑁〉}})) |
67 | | 1zzd 12361 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 ∈
ℤ) |
68 | | fzsn 13308 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
ℤ → (1...1) = {1}) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1...1) =
{1}) |
70 | 69 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → {1} =
(1...1)) |
71 | | 1e0p1 12489 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 = (0 +
1) |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 = (0 +
1)) |
73 | 72 | oveq2d 7283 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...1) = (1...(0 +
1))) |
74 | 70, 73 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {1} = (1...(0 +
1))) |
75 | 2 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 = 𝐾) |
76 | 75 | oveq1d 7282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0 + 1) = (𝐾 + 1)) |
77 | 76 | oveq2d 7283 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1...(0 + 1)) =
(1...(𝐾 +
1))) |
78 | 74, 77 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {1} = (1...(𝐾 + 1))) |
79 | 78 | feq2d 6578 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢:{1}⟶ℕ0 ↔ 𝑢:(1...(𝐾 +
1))⟶ℕ0)) |
80 | 78 | sumeq1d 15423 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Σ𝑖 ∈ {1} (𝑢‘𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖)) |
81 | 80 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁)) |
82 | 79, 81 | anbi12d 631 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁) ↔ (𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁))) |
83 | 82 | imbi1d 342 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁) → 𝑢 ∈ {{〈1, 𝑁〉}}) ↔ ((𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) → 𝑢 ∈ {{〈1, 𝑁〉}}))) |
84 | 66, 83 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) → 𝑢 ∈ {{〈1, 𝑁〉}})) |
85 | | feq1 6573 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑢 → (𝑔:(1...(𝐾 + 1))⟶ℕ0 ↔
𝑢:(1...(𝐾 +
1))⟶ℕ0)) |
86 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔 = 𝑢 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → 𝑔 = 𝑢) |
87 | 86 | fveq1d 6768 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 = 𝑢 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝑔‘𝑖) = (𝑢‘𝑖)) |
88 | 87 | sumeq2dv 15425 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑢 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖)) |
89 | 88 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑢 → (Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁)) |
90 | 85, 89 | anbi12d 631 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = 𝑢 → ((𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁) ↔ (𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁))) |
91 | 63, 90 | elab 3608 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ (𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁)) |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ (𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁))) |
93 | 92 | imbi1d 342 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} → 𝑢 ∈ {{〈1, 𝑁〉}}) ↔ ((𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) → 𝑢 ∈ {{〈1, 𝑁〉}}))) |
94 | 84, 93 | mpbird 256 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} → 𝑢 ∈ {{〈1, 𝑁〉}})) |
95 | 94 | imp 407 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) → 𝑢 ∈ {{〈1, 𝑁〉}}) |
96 | 95 | ex 413 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} → 𝑢 ∈ {{〈1, 𝑁〉}})) |
97 | 13, 14, 15, 96 | ssrd 3925 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ⊆ {{〈1, 𝑁〉}}) |
98 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℕ) |
99 | 98, 1, 55 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑢:{1}⟶{𝑁} ↔ 𝑢 = {〈1, 𝑁〉})) |
100 | 99 | bicomd 222 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑢 = {〈1, 𝑁〉} ↔ 𝑢:{1}⟶{𝑁})) |
101 | 100 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢 = {〈1, 𝑁〉} → 𝑢:{1}⟶{𝑁})) |
102 | | elsni 4578 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ {{〈1, 𝑁〉}} → 𝑢 = {〈1, 𝑁〉}) |
103 | 101, 102 | impel 506 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → 𝑢:{1}⟶{𝑁}) |
104 | 1 | snssd 4742 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → {𝑁} ⊆
ℕ0) |
105 | 104 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → {𝑁} ⊆
ℕ0) |
106 | | fss 6609 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢:{1}⟶{𝑁} ∧ {𝑁} ⊆ ℕ0) → 𝑢:{1}⟶ℕ0) |
107 | 103, 105,
106 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → 𝑢:{1}⟶ℕ0) |
108 | 79 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → (𝑢:{1}⟶ℕ0 ↔ 𝑢:(1...(𝐾 +
1))⟶ℕ0)) |
109 | 107, 108 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → 𝑢:(1...(𝐾 +
1))⟶ℕ0) |
110 | 102 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → 𝑢 = {〈1, 𝑁〉}) |
111 | 78 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → {1} = (1...(𝐾 + 1))) |
112 | 111 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → (1...(𝐾 + 1)) = {1}) |
113 | 112 | sumeq1d 15423 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = Σ𝑖 ∈ {1} (𝑢‘𝑖)) |
114 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 1 ∈
ℕ) |
115 | 1 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 𝑁 ∈
ℕ0) |
116 | 115 | nn0cnd 12305 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 𝑁 ∈ ℂ) |
117 | 114, 115,
45 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → ({〈1, 𝑁〉}‘1) = 𝑁) |
118 | 117 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 𝑁 = ({〈1, 𝑁〉}‘1)) |
119 | 110 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 𝑢 = {〈1, 𝑁〉}) |
120 | 119 | fveq1d 6768 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → (𝑢‘1) = ({〈1, 𝑁〉}‘1)) |
121 | 118, 120 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 𝑁 = (𝑢‘1)) |
122 | 121 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → (𝑁 ∈ ℂ ↔ (𝑢‘1) ∈ ℂ)) |
123 | 116, 122 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → (𝑢‘1) ∈ ℂ) |
124 | 114, 123,
34 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) |
125 | 120, 117 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → (𝑢‘1) = 𝑁) |
126 | 124, 125 | eqtrd 2778 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁) |
127 | 113, 126 | eqtrd 2778 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) |
128 | 127 | 3expa 1117 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) ∧ 𝑢 = {〈1, 𝑁〉}) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) |
129 | 110, 128 | mpdan 684 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) |
130 | 109, 129 | jca 512 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → (𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁)) |
131 | 130, 91 | sylibr 233 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → 𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) |
132 | 131 | ex 413 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ {{〈1, 𝑁〉}} → 𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)})) |
133 | 13, 15, 14, 132 | ssrd 3925 |
. . . . . . . . . 10
⊢ (𝜑 → {{〈1, 𝑁〉}} ⊆ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) |
134 | 97, 133 | eqssd 3937 |
. . . . . . . . 9
⊢ (𝜑 → {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} = {{〈1, 𝑁〉}}) |
135 | 12, 134 | eqtrd 2778 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 = {{〈1, 𝑁〉}}) |
136 | | eqss 3935 |
. . . . . . . . . 10
⊢ (𝐴 = {{〈1, 𝑁〉}} ↔ (𝐴 ⊆ {{〈1, 𝑁〉}} ∧ {{〈1, 𝑁〉}} ⊆ 𝐴)) |
137 | 136 | biimpi 215 |
. . . . . . . . 9
⊢ (𝐴 = {{〈1, 𝑁〉}} → (𝐴 ⊆ {{〈1, 𝑁〉}} ∧ {{〈1, 𝑁〉}} ⊆ 𝐴)) |
138 | 137 | simpld 495 |
. . . . . . . 8
⊢ (𝐴 = {{〈1, 𝑁〉}} → 𝐴 ⊆ {{〈1, 𝑁〉}}) |
139 | 135, 138 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ {{〈1, 𝑁〉}}) |
140 | | fss 6609 |
. . . . . . 7
⊢ ((𝐺:𝐵⟶𝐴 ∧ 𝐴 ⊆ {{〈1, 𝑁〉}}) → 𝐺:𝐵⟶{{〈1, 𝑁〉}}) |
141 | 11, 139, 140 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 𝐺:𝐵⟶{{〈1, 𝑁〉}}) |
142 | 141 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐺:𝐵⟶{{〈1, 𝑁〉}}) |
143 | 9 | ffvelrnda 6953 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐹‘𝑐) ∈ 𝐵) |
144 | | fvconst 7028 |
. . . . 5
⊢ ((𝐺:𝐵⟶{{〈1, 𝑁〉}} ∧ (𝐹‘𝑐) ∈ 𝐵) → (𝐺‘(𝐹‘𝑐)) = {〈1, 𝑁〉}) |
145 | 142, 143,
144 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐺‘(𝐹‘𝑐)) = {〈1, 𝑁〉}) |
146 | 135 | eleq2d 2824 |
. . . . . . . 8
⊢ (𝜑 → (𝑐 ∈ 𝐴 ↔ 𝑐 ∈ {{〈1, 𝑁〉}})) |
147 | 146 | biimpd 228 |
. . . . . . 7
⊢ (𝜑 → (𝑐 ∈ 𝐴 → 𝑐 ∈ {{〈1, 𝑁〉}})) |
148 | 147 | imp 407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ {{〈1, 𝑁〉}}) |
149 | | vex 3433 |
. . . . . . 7
⊢ 𝑐 ∈ V |
150 | 149 | elsn 4576 |
. . . . . 6
⊢ (𝑐 ∈ {{〈1, 𝑁〉}} ↔ 𝑐 = {〈1, 𝑁〉}) |
151 | 148, 150 | sylib 217 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 = {〈1, 𝑁〉}) |
152 | 151 | eqcomd 2744 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → {〈1, 𝑁〉} = 𝑐) |
153 | 145, 152 | eqtrd 2778 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐺‘(𝐹‘𝑐)) = 𝑐) |
154 | 153 | ralrimiva 3108 |
. 2
⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝐺‘(𝐹‘𝑐)) = 𝑐) |
155 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 ∈ 𝐵) |
156 | | nfv 1917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑𝜑 |
157 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑𝐵 |
158 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑{∅} |
159 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) |
160 | 159 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑑 ∈ 𝐵 ↔ 𝑑 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))})) |
161 | 160 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑑 ∈ 𝐵 → 𝑑 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))})) |
162 | 161 | syldbl2 838 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) |
163 | | vex 3433 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑑 ∈ V |
164 | | feq1 6573 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑑 → (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ 𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)))) |
165 | | fveq1 6765 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑑 → (𝑓‘𝑥) = (𝑑‘𝑥)) |
166 | | fveq1 6765 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑑 → (𝑓‘𝑦) = (𝑑‘𝑦)) |
167 | 165, 166 | breq12d 5086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑑 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑑‘𝑥) < (𝑑‘𝑦))) |
168 | 167 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑑 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑑‘𝑥) < (𝑑‘𝑦)))) |
169 | 168 | 2ralbidv 3123 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑑 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑑‘𝑥) < (𝑑‘𝑦)))) |
170 | 164, 169 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑑 → ((𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑑‘𝑥) < (𝑑‘𝑦))))) |
171 | 163, 170 | elab 3608 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ (𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑑‘𝑥) < (𝑑‘𝑦)))) |
172 | 162, 171 | sylib 217 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑑‘𝑥) < (𝑑‘𝑦)))) |
173 | 172 | simpld 495 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾))) |
174 | | 0lt1 11507 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 <
1 |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 < 1) |
176 | 2, 175 | eqbrtrd 5095 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 < 1) |
177 | 5 | nn0zd 12434 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 ∈ ℤ) |
178 | | fzn 13282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℤ ∧ 𝐾
∈ ℤ) → (𝐾
< 1 ↔ (1...𝐾) =
∅)) |
179 | 67, 177, 178 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐾 < 1 ↔ (1...𝐾) = ∅)) |
180 | 176, 179 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...𝐾) = ∅) |
181 | 180 | feq2d 6578 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ 𝑑:∅⟶(1...(𝑁 + 𝐾)))) |
182 | 181 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ 𝑑:∅⟶(1...(𝑁 + 𝐾)))) |
183 | 173, 182 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑:∅⟶(1...(𝑁 + 𝐾))) |
184 | | f0bi 6649 |
. . . . . . . . . . . . . . 15
⊢ (𝑑:∅⟶(1...(𝑁 + 𝐾)) ↔ 𝑑 = ∅) |
185 | 183, 184 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 = ∅) |
186 | | velsn 4577 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ {∅} ↔ 𝑑 = ∅) |
187 | 185, 186 | sylibr 233 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 ∈ {∅}) |
188 | 187 | ex 413 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑑 ∈ 𝐵 → 𝑑 ∈ {∅})) |
189 | | f0 6647 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∅:∅⟶(1...(𝑁 + 𝐾)) |
190 | 189 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
∅:∅⟶(1...(𝑁 + 𝐾))) |
191 | 180 | feq2d 6578 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ ∅:∅⟶(1...(𝑁 + 𝐾)))) |
192 | 190, 191 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∅:(1...𝐾)⟶(1...(𝑁 + 𝐾))) |
193 | | ral0 4443 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∀𝑥 ∈
∅ ∀𝑦 ∈
(1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)) |
194 | 193 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ ∅ ∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦))) |
195 | | biidd 261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐾)) → (∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)) ↔ ∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)))) |
196 | 180, 195 | raleqbidva 3352 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)) ↔ ∀𝑥 ∈ ∅ ∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)))) |
197 | 194, 196 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦))) |
198 | 192, 197 | jca 512 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)))) |
199 | | 0ex 5229 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ V |
200 | | feq1 6573 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = ∅ → (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ ∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)))) |
201 | | fveq1 6765 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = ∅ → (𝑓‘𝑥) = (∅‘𝑥)) |
202 | | fveq1 6765 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = ∅ → (𝑓‘𝑦) = (∅‘𝑦)) |
203 | 201, 202 | breq12d 5086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = ∅ → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (∅‘𝑥) < (∅‘𝑦))) |
204 | 203 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = ∅ → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)))) |
205 | 204 | 2ralbidv 3123 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = ∅ → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)))) |
206 | 200, 205 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = ∅ → ((𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦))))) |
207 | 206 | elabg 3606 |
. . . . . . . . . . . . . . . . . 18
⊢ (∅
∈ V → (∅ ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ (∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦))))) |
208 | 199, 207 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ (∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)))) |
209 | 198, 208 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∅ ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) |
210 | 8 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) |
211 | 209, 210 | eleqtrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∅ ∈ 𝐵) |
212 | 211 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ {∅}) → ∅ ∈
𝐵) |
213 | | elsni 4578 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ {∅} → 𝑑 = ∅) |
214 | 213 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ {∅}) → 𝑑 = ∅) |
215 | 214 | eleq1d 2823 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ {∅}) → (𝑑 ∈ 𝐵 ↔ ∅ ∈ 𝐵)) |
216 | 212, 215 | mpbird 256 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {∅}) → 𝑑 ∈ 𝐵) |
217 | 216 | ex 413 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑑 ∈ {∅} → 𝑑 ∈ 𝐵)) |
218 | 188, 217 | impbid 211 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑑 ∈ 𝐵 ↔ 𝑑 ∈ {∅})) |
219 | 156, 157,
158, 218 | eqrd 3939 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = {∅}) |
220 | 219 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝐵 = {∅}) |
221 | 155, 220 | eleqtrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 ∈ {∅}) |
222 | 163 | elsn 4576 |
. . . . . . . 8
⊢ (𝑑 ∈ {∅} ↔ 𝑑 = ∅) |
223 | 221, 222 | sylib 217 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 = ∅) |
224 | 223 | fveq2d 6770 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐺‘𝑑) = (𝐺‘∅)) |
225 | 224 | fveq2d 6770 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐹‘(𝐺‘𝑑)) = (𝐹‘(𝐺‘∅))) |
226 | 180 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (1...𝐾) = ∅) |
227 | 226 | mpteq1d 5168 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = (𝑗 ∈ ∅ ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) |
228 | | mpt0 6567 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ∅ ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅ |
229 | 228 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ ∅ ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅) |
230 | 227, 229 | eqtrd 2778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅) |
231 | | fzfid 13703 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝐾) ∈ Fin) |
232 | 231 | mptexd 7092 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ V) |
233 | | elsng 4575 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ V → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {∅} ↔ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅)) |
234 | 232, 233 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {∅} ↔ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅)) |
235 | 234 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {∅} ↔ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅)) |
236 | 230, 235 | mpbird 256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {∅}) |
237 | 236, 6 | fmptd 6980 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶{∅}) |
238 | 237 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝐹:𝐴⟶{∅}) |
239 | | ffvelrn 6951 |
. . . . . . . 8
⊢ ((𝐺:𝐵⟶𝐴 ∧ ∅ ∈ 𝐵) → (𝐺‘∅) ∈ 𝐴) |
240 | 11, 211, 239 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘∅) ∈ 𝐴) |
241 | 240 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐺‘∅) ∈ 𝐴) |
242 | | fvconst 7028 |
. . . . . 6
⊢ ((𝐹:𝐴⟶{∅} ∧ (𝐺‘∅) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) = ∅) |
243 | 238, 241,
242 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐹‘(𝐺‘∅)) = ∅) |
244 | 225, 243 | eqtrd 2778 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐹‘(𝐺‘𝑑)) = ∅) |
245 | 223 | eqcomd 2744 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → ∅ = 𝑑) |
246 | 244, 245 | eqtrd 2778 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐹‘(𝐺‘𝑑)) = 𝑑) |
247 | 246 | ralrimiva 3108 |
. 2
⊢ (𝜑 → ∀𝑑 ∈ 𝐵 (𝐹‘(𝐺‘𝑑)) = 𝑑) |
248 | 9, 11, 154, 247 | 2fvidf1od 7162 |
1
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |