| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sticksstones11.1 | . . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 2 |  | sticksstones11.2 | . . . 4
⊢ (𝜑 → 𝐾 = 0) | 
| 3 |  | 0nn0 12541 | . . . . 5
⊢ 0 ∈
ℕ0 | 
| 4 | 3 | a1i 11 | . . . 4
⊢ (𝜑 → 0 ∈
ℕ0) | 
| 5 | 2, 4 | eqeltrd 2841 | . . 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 42154 | . 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 42155 | . 2
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) | 
| 12 | 7 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) | 
| 13 |  | nfv 1914 | . . . . . . . . . . 11
⊢
Ⅎ𝑢𝜑 | 
| 14 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑢{𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} | 
| 15 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑢{{〈1, 𝑁〉}} | 
| 16 |  | ffn 6736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢:{1}⟶ℕ0
→ 𝑢 Fn
{1}) | 
| 17 | 16 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢 Fn {1}) | 
| 18 |  | 1nn 12277 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℕ | 
| 19 | 18 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 1 ∈ ℕ) | 
| 20 | 1 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑁 ∈
ℕ0) | 
| 21 |  | fnsng 6618 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℕ ∧ 𝑁
∈ ℕ0) → {〈1, 𝑁〉} Fn {1}) | 
| 22 | 19, 20, 21 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → {〈1, 𝑁〉} Fn {1}) | 
| 23 |  | elsni 4643 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 ∈ {1} → 𝑝 = 1) | 
| 24 | 23 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → 𝑝 = 1) | 
| 25 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → 𝑝 = 1) | 
| 26 | 25 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → (𝑢‘𝑝) = (𝑢‘1)) | 
| 27 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢:{1}⟶ℕ0) | 
| 28 |  | 1ex 11257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 1 ∈
V | 
| 29 | 28 | snid 4662 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 1 ∈
{1} | 
| 30 | 29 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 1 ∈ {1}) | 
| 31 | 27, 30 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → (𝑢‘1) ∈
ℕ0) | 
| 32 | 31 | nn0cnd 12589 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → (𝑢‘1) ∈ ℂ) | 
| 33 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = 1 → (𝑢‘𝑖) = (𝑢‘1)) | 
| 34 | 33 | sumsn 15782 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((1
∈ ℕ ∧ (𝑢‘1) ∈ ℂ) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) | 
| 35 | 19, 32, 34 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) | 
| 37 | 36 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) → (𝑢‘1) = Σ𝑖 ∈ {1} (𝑢‘𝑖)) | 
| 38 |  | simplrr 778 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁) | 
| 39 | 37, 38 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) → (𝑢‘1) = 𝑁) | 
| 40 | 39 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → (Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1) → (𝑢‘1) = 𝑁)) | 
| 41 | 35, 40 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → (𝑢‘1) = 𝑁) | 
| 42 | 41 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → (𝑢‘1) = 𝑁) | 
| 43 | 18 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → 1 ∈
ℕ) | 
| 44 | 20 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → 𝑁 ∈
ℕ0) | 
| 45 |  | fvsng 7200 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((1
∈ ℕ ∧ 𝑁
∈ ℕ0) → ({〈1, 𝑁〉}‘1) = 𝑁) | 
| 46 | 43, 44, 45 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → ({〈1, 𝑁〉}‘1) = 𝑁) | 
| 47 | 46 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → 𝑁 = ({〈1, 𝑁〉}‘1)) | 
| 48 | 42, 47 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → (𝑢‘1) = ({〈1, 𝑁〉}‘1)) | 
| 49 | 48 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → (𝑢‘1) = ({〈1, 𝑁〉}‘1)) | 
| 50 | 25 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → 1 = 𝑝) | 
| 51 | 50 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → ({〈1, 𝑁〉}‘1) = ({〈1, 𝑁〉}‘𝑝)) | 
| 52 | 26, 49, 51 | 3eqtrd 2781 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) ∧ 𝑝 = 1) → (𝑢‘𝑝) = ({〈1, 𝑁〉}‘𝑝)) | 
| 53 | 24, 52 | mpdan 687 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) ∧ 𝑝 ∈ {1}) → (𝑢‘𝑝) = ({〈1, 𝑁〉}‘𝑝)) | 
| 54 | 17, 22, 53 | eqfnfvd 7054 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢 = {〈1, 𝑁〉}) | 
| 55 |  | fsng 7157 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℕ ∧ 𝑁
∈ ℕ0) → (𝑢:{1}⟶{𝑁} ↔ 𝑢 = {〈1, 𝑁〉})) | 
| 56 | 19, 20, 55 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → (𝑢:{1}⟶{𝑁} ↔ 𝑢 = {〈1, 𝑁〉})) | 
| 57 | 54, 56 | mpbird 257 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢:{1}⟶{𝑁}) | 
| 58 |  | ssidd 4007 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → {𝑁} ⊆ {𝑁}) | 
| 59 |  | fss 6752 | . . . . . . . . . . . . . . . . . . . 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 232 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢 = {〈1, 𝑁〉}) | 
| 63 |  | vex 3484 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑢 ∈ V | 
| 64 | 63 | elsn 4641 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ {{〈1, 𝑁〉}} ↔ 𝑢 = {〈1, 𝑁〉}) | 
| 65 | 62, 64 | sylibr 234 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁)) → 𝑢 ∈ {{〈1, 𝑁〉}}) | 
| 66 | 65 | ex 412 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁) → 𝑢 ∈ {{〈1, 𝑁〉}})) | 
| 67 |  | 1zzd 12648 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 ∈
ℤ) | 
| 68 |  | fzsn 13606 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
ℤ → (1...1) = {1}) | 
| 69 | 67, 68 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1...1) =
{1}) | 
| 70 | 69 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → {1} =
(1...1)) | 
| 71 |  | 1e0p1 12775 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 = (0 +
1) | 
| 72 | 71 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 = (0 +
1)) | 
| 73 | 72 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...1) = (1...(0 +
1))) | 
| 74 | 70, 73 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {1} = (1...(0 +
1))) | 
| 75 | 2 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 = 𝐾) | 
| 76 | 75 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0 + 1) = (𝐾 + 1)) | 
| 77 | 76 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1...(0 + 1)) =
(1...(𝐾 +
1))) | 
| 78 | 74, 77 | eqtrd 2777 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {1} = (1...(𝐾 + 1))) | 
| 79 | 78 | feq2d 6722 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢:{1}⟶ℕ0 ↔ 𝑢:(1...(𝐾 +
1))⟶ℕ0)) | 
| 80 | 78 | sumeq1d 15736 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Σ𝑖 ∈ {1} (𝑢‘𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖)) | 
| 81 | 80 | eqeq1d 2739 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁)) | 
| 82 | 79, 81 | anbi12d 632 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁) ↔ (𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁))) | 
| 83 | 82 | imbi1d 341 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑢:{1}⟶ℕ0 ∧
Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁) → 𝑢 ∈ {{〈1, 𝑁〉}}) ↔ ((𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) → 𝑢 ∈ {{〈1, 𝑁〉}}))) | 
| 84 | 66, 83 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) → 𝑢 ∈ {{〈1, 𝑁〉}})) | 
| 85 |  | feq1 6716 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑢 → (𝑔:(1...(𝐾 + 1))⟶ℕ0 ↔
𝑢:(1...(𝐾 +
1))⟶ℕ0)) | 
| 86 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔 = 𝑢 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → 𝑔 = 𝑢) | 
| 87 | 86 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 = 𝑢 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝑔‘𝑖) = (𝑢‘𝑖)) | 
| 88 | 87 | sumeq2dv 15738 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑢 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖)) | 
| 89 | 88 | eqeq1d 2739 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑢 → (Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁)) | 
| 90 | 85, 89 | anbi12d 632 | . . . . . . . . . . . . . . . . 17
⊢ (𝑔 = 𝑢 → ((𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁) ↔ (𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁))) | 
| 91 | 63, 90 | elab 3679 | . . . . . . . . . . . . . . . 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 341 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} → 𝑢 ∈ {{〈1, 𝑁〉}}) ↔ ((𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) → 𝑢 ∈ {{〈1, 𝑁〉}}))) | 
| 94 | 84, 93 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} → 𝑢 ∈ {{〈1, 𝑁〉}})) | 
| 95 | 94 | imp 406 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) → 𝑢 ∈ {{〈1, 𝑁〉}}) | 
| 96 | 95 | ex 412 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} → 𝑢 ∈ {{〈1, 𝑁〉}})) | 
| 97 | 13, 14, 15, 96 | ssrd 3988 | . . . . . . . . . 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 223 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑢 = {〈1, 𝑁〉} ↔ 𝑢:{1}⟶{𝑁})) | 
| 101 | 100 | biimpd 229 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢 = {〈1, 𝑁〉} → 𝑢:{1}⟶{𝑁})) | 
| 102 |  | elsni 4643 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ {{〈1, 𝑁〉}} → 𝑢 = {〈1, 𝑁〉}) | 
| 103 | 101, 102 | impel 505 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → 𝑢:{1}⟶{𝑁}) | 
| 104 | 1 | snssd 4809 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → {𝑁} ⊆
ℕ0) | 
| 105 | 104 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → {𝑁} ⊆
ℕ0) | 
| 106 |  | fss 6752 | . . . . . . . . . . . . . . . 16
⊢ ((𝑢:{1}⟶{𝑁} ∧ {𝑁} ⊆ ℕ0) → 𝑢:{1}⟶ℕ0) | 
| 107 | 103, 105,
106 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → 𝑢:{1}⟶ℕ0) | 
| 108 | 79 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → (𝑢:{1}⟶ℕ0 ↔ 𝑢:(1...(𝐾 +
1))⟶ℕ0)) | 
| 109 | 107, 108 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → 𝑢:(1...(𝐾 +
1))⟶ℕ0) | 
| 110 | 102 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → 𝑢 = {〈1, 𝑁〉}) | 
| 111 | 78 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → {1} = (1...(𝐾 + 1))) | 
| 112 | 111 | eqcomd 2743 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → (1...(𝐾 + 1)) = {1}) | 
| 113 | 112 | sumeq1d 15736 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = Σ𝑖 ∈ {1} (𝑢‘𝑖)) | 
| 114 | 18 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 1 ∈
ℕ) | 
| 115 | 1 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 𝑁 ∈
ℕ0) | 
| 116 | 115 | nn0cnd 12589 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 𝑁 ∈ ℂ) | 
| 117 | 114, 115,
45 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → ({〈1, 𝑁〉}‘1) = 𝑁) | 
| 118 | 117 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 𝑁 = ({〈1, 𝑁〉}‘1)) | 
| 119 | 110 | 3adant3 1133 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 𝑢 = {〈1, 𝑁〉}) | 
| 120 | 119 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → (𝑢‘1) = ({〈1, 𝑁〉}‘1)) | 
| 121 | 118, 120 | eqtr4d 2780 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → 𝑁 = (𝑢‘1)) | 
| 122 | 121 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → (𝑁 ∈ ℂ ↔ (𝑢‘1) ∈ ℂ)) | 
| 123 | 116, 122 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → (𝑢‘1) ∈ ℂ) | 
| 124 | 114, 123,
34 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = (𝑢‘1)) | 
| 125 | 120, 117 | eqtrd 2777 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → (𝑢‘1) = 𝑁) | 
| 126 | 124, 125 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → Σ𝑖 ∈ {1} (𝑢‘𝑖) = 𝑁) | 
| 127 | 113, 126 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}} ∧ 𝑢 = {〈1, 𝑁〉}) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) | 
| 128 | 127 | 3expa 1119 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) ∧ 𝑢 = {〈1, 𝑁〉}) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) | 
| 129 | 110, 128 | mpdan 687 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁) | 
| 130 | 109, 129 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → (𝑢:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑢‘𝑖) = 𝑁)) | 
| 131 | 130, 91 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ {{〈1, 𝑁〉}}) → 𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) | 
| 132 | 131 | ex 412 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ {{〈1, 𝑁〉}} → 𝑢 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)})) | 
| 133 | 13, 15, 14, 132 | ssrd 3988 | . . . . . . . . . 10
⊢ (𝜑 → {{〈1, 𝑁〉}} ⊆ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) | 
| 134 | 97, 133 | eqssd 4001 | . . . . . . . . 9
⊢ (𝜑 → {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} = {{〈1, 𝑁〉}}) | 
| 135 | 12, 134 | eqtrd 2777 | . . . . . . . 8
⊢ (𝜑 → 𝐴 = {{〈1, 𝑁〉}}) | 
| 136 |  | eqss 3999 | . . . . . . . . . 10
⊢ (𝐴 = {{〈1, 𝑁〉}} ↔ (𝐴 ⊆ {{〈1, 𝑁〉}} ∧ {{〈1, 𝑁〉}} ⊆ 𝐴)) | 
| 137 | 136 | biimpi 216 | . . . . . . . . 9
⊢ (𝐴 = {{〈1, 𝑁〉}} → (𝐴 ⊆ {{〈1, 𝑁〉}} ∧ {{〈1, 𝑁〉}} ⊆ 𝐴)) | 
| 138 | 137 | simpld 494 | . . . . . . . 8
⊢ (𝐴 = {{〈1, 𝑁〉}} → 𝐴 ⊆ {{〈1, 𝑁〉}}) | 
| 139 | 135, 138 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ {{〈1, 𝑁〉}}) | 
| 140 |  | fss 6752 | . . . . . . 7
⊢ ((𝐺:𝐵⟶𝐴 ∧ 𝐴 ⊆ {{〈1, 𝑁〉}}) → 𝐺:𝐵⟶{{〈1, 𝑁〉}}) | 
| 141 | 11, 139, 140 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → 𝐺:𝐵⟶{{〈1, 𝑁〉}}) | 
| 142 | 141 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐺:𝐵⟶{{〈1, 𝑁〉}}) | 
| 143 | 9 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐹‘𝑐) ∈ 𝐵) | 
| 144 |  | fvconst 7184 | . . . . 5
⊢ ((𝐺:𝐵⟶{{〈1, 𝑁〉}} ∧ (𝐹‘𝑐) ∈ 𝐵) → (𝐺‘(𝐹‘𝑐)) = {〈1, 𝑁〉}) | 
| 145 | 142, 143,
144 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐺‘(𝐹‘𝑐)) = {〈1, 𝑁〉}) | 
| 146 | 135 | eleq2d 2827 | . . . . . . . 8
⊢ (𝜑 → (𝑐 ∈ 𝐴 ↔ 𝑐 ∈ {{〈1, 𝑁〉}})) | 
| 147 | 146 | biimpd 229 | . . . . . . 7
⊢ (𝜑 → (𝑐 ∈ 𝐴 → 𝑐 ∈ {{〈1, 𝑁〉}})) | 
| 148 | 147 | imp 406 | . . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ {{〈1, 𝑁〉}}) | 
| 149 |  | vex 3484 | . . . . . . 7
⊢ 𝑐 ∈ V | 
| 150 | 149 | elsn 4641 | . . . . . 6
⊢ (𝑐 ∈ {{〈1, 𝑁〉}} ↔ 𝑐 = {〈1, 𝑁〉}) | 
| 151 | 148, 150 | sylib 218 | . . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 = {〈1, 𝑁〉}) | 
| 152 | 151 | eqcomd 2743 | . . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → {〈1, 𝑁〉} = 𝑐) | 
| 153 | 145, 152 | eqtrd 2777 | . . 3
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐺‘(𝐹‘𝑐)) = 𝑐) | 
| 154 | 153 | ralrimiva 3146 | . 2
⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝐺‘(𝐹‘𝑐)) = 𝑐) | 
| 155 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 ∈ 𝐵) | 
| 156 |  | nfv 1914 | . . . . . . . . . . 11
⊢
Ⅎ𝑑𝜑 | 
| 157 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑑𝐵 | 
| 158 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑑{∅} | 
| 159 | 8 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) | 
| 160 | 159 | eleq2d 2827 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑑 ∈ 𝐵 ↔ 𝑑 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))})) | 
| 161 | 160 | biimpd 229 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑑 ∈ 𝐵 → 𝑑 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))})) | 
| 162 | 161 | syldbl2 842 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) | 
| 163 |  | vex 3484 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑑 ∈ V | 
| 164 |  | feq1 6716 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑑 → (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ 𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)))) | 
| 165 |  | fveq1 6905 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑑 → (𝑓‘𝑥) = (𝑑‘𝑥)) | 
| 166 |  | fveq1 6905 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑑 → (𝑓‘𝑦) = (𝑑‘𝑦)) | 
| 167 | 165, 166 | breq12d 5156 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑑 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑑‘𝑥) < (𝑑‘𝑦))) | 
| 168 | 167 | imbi2d 340 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑑 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑑‘𝑥) < (𝑑‘𝑦)))) | 
| 169 | 168 | 2ralbidv 3221 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑑 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑑‘𝑥) < (𝑑‘𝑦)))) | 
| 170 | 164, 169 | anbi12d 632 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑑 → ((𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑑‘𝑥) < (𝑑‘𝑦))))) | 
| 171 | 163, 170 | elab 3679 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑑 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ (𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑑‘𝑥) < (𝑑‘𝑦)))) | 
| 172 | 162, 171 | sylib 218 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑑‘𝑥) < (𝑑‘𝑦)))) | 
| 173 | 172 | simpld 494 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾))) | 
| 174 |  | 0lt1 11785 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 0 <
1 | 
| 175 | 174 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 < 1) | 
| 176 | 2, 175 | eqbrtrd 5165 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 < 1) | 
| 177 | 5 | nn0zd 12639 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 ∈ ℤ) | 
| 178 |  | fzn 13580 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℤ ∧ 𝐾
∈ ℤ) → (𝐾
< 1 ↔ (1...𝐾) =
∅)) | 
| 179 | 67, 177, 178 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐾 < 1 ↔ (1...𝐾) = ∅)) | 
| 180 | 176, 179 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...𝐾) = ∅) | 
| 181 | 180 | feq2d 6722 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ 𝑑:∅⟶(1...(𝑁 + 𝐾)))) | 
| 182 | 181 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑑:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ 𝑑:∅⟶(1...(𝑁 + 𝐾)))) | 
| 183 | 173, 182 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑:∅⟶(1...(𝑁 + 𝐾))) | 
| 184 |  | f0bi 6791 | . . . . . . . . . . . . . . 15
⊢ (𝑑:∅⟶(1...(𝑁 + 𝐾)) ↔ 𝑑 = ∅) | 
| 185 | 183, 184 | sylib 218 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 = ∅) | 
| 186 |  | velsn 4642 | . . . . . . . . . . . . . 14
⊢ (𝑑 ∈ {∅} ↔ 𝑑 = ∅) | 
| 187 | 185, 186 | sylibr 234 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 ∈ {∅}) | 
| 188 | 187 | ex 412 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑑 ∈ 𝐵 → 𝑑 ∈ {∅})) | 
| 189 |  | f0 6789 | . . . . . . . . . . . . . . . . . . . 20
⊢
∅:∅⟶(1...(𝑁 + 𝐾)) | 
| 190 | 189 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
∅:∅⟶(1...(𝑁 + 𝐾))) | 
| 191 | 180 | feq2d 6722 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ ∅:∅⟶(1...(𝑁 + 𝐾)))) | 
| 192 | 190, 191 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∅:(1...𝐾)⟶(1...(𝑁 + 𝐾))) | 
| 193 |  | ral0 4513 | . . . . . . . . . . . . . . . . . . . 20
⊢
∀𝑥 ∈
∅ ∀𝑦 ∈
(1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)) | 
| 194 | 193 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ ∅ ∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦))) | 
| 195 | 194, 180 | raleqtrrdv 3330 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦))) | 
| 196 | 192, 195 | jca 511 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)))) | 
| 197 |  | 0ex 5307 | . . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ V | 
| 198 |  | feq1 6716 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = ∅ → (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ ∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)))) | 
| 199 |  | fveq1 6905 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = ∅ → (𝑓‘𝑥) = (∅‘𝑥)) | 
| 200 |  | fveq1 6905 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = ∅ → (𝑓‘𝑦) = (∅‘𝑦)) | 
| 201 | 199, 200 | breq12d 5156 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = ∅ → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (∅‘𝑥) < (∅‘𝑦))) | 
| 202 | 201 | imbi2d 340 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = ∅ → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)))) | 
| 203 | 202 | 2ralbidv 3221 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = ∅ → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)))) | 
| 204 | 198, 203 | anbi12d 632 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = ∅ → ((𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦))))) | 
| 205 | 204 | elabg 3676 | . . . . . . . . . . . . . . . . . 18
⊢ (∅
∈ V → (∅ ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ (∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦))))) | 
| 206 | 197, 205 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢ (∅
∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ (∅:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (∅‘𝑥) < (∅‘𝑦)))) | 
| 207 | 196, 206 | sylibr 234 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∅ ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) | 
| 208 | 8 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) | 
| 209 | 207, 208 | eleqtrrd 2844 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ∅ ∈ 𝐵) | 
| 210 | 209 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ {∅}) → ∅ ∈
𝐵) | 
| 211 |  | elsni 4643 | . . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ {∅} → 𝑑 = ∅) | 
| 212 | 211 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ {∅}) → 𝑑 = ∅) | 
| 213 | 212 | eleq1d 2826 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ {∅}) → (𝑑 ∈ 𝐵 ↔ ∅ ∈ 𝐵)) | 
| 214 | 210, 213 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ {∅}) → 𝑑 ∈ 𝐵) | 
| 215 | 214 | ex 412 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑑 ∈ {∅} → 𝑑 ∈ 𝐵)) | 
| 216 | 188, 215 | impbid 212 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑑 ∈ 𝐵 ↔ 𝑑 ∈ {∅})) | 
| 217 | 156, 157,
158, 216 | eqrd 4003 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 = {∅}) | 
| 218 | 217 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝐵 = {∅}) | 
| 219 | 155, 218 | eleqtrd 2843 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 ∈ {∅}) | 
| 220 | 163 | elsn 4641 | . . . . . . . 8
⊢ (𝑑 ∈ {∅} ↔ 𝑑 = ∅) | 
| 221 | 219, 220 | sylib 218 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 = ∅) | 
| 222 | 221 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐺‘𝑑) = (𝐺‘∅)) | 
| 223 | 222 | fveq2d 6910 | . . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐹‘(𝐺‘𝑑)) = (𝐹‘(𝐺‘∅))) | 
| 224 | 180 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (1...𝐾) = ∅) | 
| 225 | 224 | mpteq1d 5237 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = (𝑗 ∈ ∅ ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) | 
| 226 |  | mpt0 6710 | . . . . . . . . . . 11
⊢ (𝑗 ∈ ∅ ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅ | 
| 227 | 226 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ ∅ ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅) | 
| 228 | 225, 227 | eqtrd 2777 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅) | 
| 229 |  | fzfid 14014 | . . . . . . . . . . . 12
⊢ (𝜑 → (1...𝐾) ∈ Fin) | 
| 230 | 229 | mptexd 7244 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ V) | 
| 231 |  | elsng 4640 | . . . . . . . . . . 11
⊢ ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ V → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {∅} ↔ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅)) | 
| 232 | 230, 231 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {∅} ↔ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅)) | 
| 233 | 232 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {∅} ↔ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = ∅)) | 
| 234 | 228, 233 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {∅}) | 
| 235 | 234, 6 | fmptd 7134 | . . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶{∅}) | 
| 236 | 235 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝐹:𝐴⟶{∅}) | 
| 237 |  | ffvelcdm 7101 | . . . . . . . 8
⊢ ((𝐺:𝐵⟶𝐴 ∧ ∅ ∈ 𝐵) → (𝐺‘∅) ∈ 𝐴) | 
| 238 | 11, 209, 237 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝐺‘∅) ∈ 𝐴) | 
| 239 | 238 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐺‘∅) ∈ 𝐴) | 
| 240 |  | fvconst 7184 | . . . . . 6
⊢ ((𝐹:𝐴⟶{∅} ∧ (𝐺‘∅) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) = ∅) | 
| 241 | 236, 239,
240 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐹‘(𝐺‘∅)) = ∅) | 
| 242 | 223, 241 | eqtrd 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐹‘(𝐺‘𝑑)) = ∅) | 
| 243 | 221 | eqcomd 2743 | . . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → ∅ = 𝑑) | 
| 244 | 242, 243 | eqtrd 2777 | . . 3
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐹‘(𝐺‘𝑑)) = 𝑑) | 
| 245 | 244 | ralrimiva 3146 | . 2
⊢ (𝜑 → ∀𝑑 ∈ 𝐵 (𝐹‘(𝐺‘𝑑)) = 𝑑) | 
| 246 | 9, 11, 154, 245 | 2fvidf1od 7318 | 1
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |