| Step | Hyp | Ref
| Expression |
| 1 | | sticksstones19.1 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 2 | | sticksstones19.2 |
. . 3
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 3 | | sticksstones19.3 |
. . 3
⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} |
| 4 | | sticksstones19.4 |
. . 3
⊢ 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧
Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)} |
| 5 | | sticksstones19.5 |
. . 3
⊢ (𝜑 → 𝑍:(1...𝐾)–1-1-onto→𝑆) |
| 6 | | sticksstones19.6 |
. . 3
⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥)))) |
| 7 | 1, 2, 3, 4, 5, 6 | sticksstones18 42165 |
. 2
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 8 | | sticksstones19.7 |
. . 3
⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦)))) |
| 9 | 1, 2, 3, 4, 5, 8 | sticksstones17 42164 |
. 2
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
| 10 | 8 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦))))) |
| 11 | | simplr 769 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑏 = (𝐹‘𝑐)) ∧ 𝑦 ∈ (1...𝐾)) → 𝑏 = (𝐹‘𝑐)) |
| 12 | 11 | fveq1d 6908 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑏 = (𝐹‘𝑐)) ∧ 𝑦 ∈ (1...𝐾)) → (𝑏‘(𝑍‘𝑦)) = ((𝐹‘𝑐)‘(𝑍‘𝑦))) |
| 13 | 12 | mpteq2dva 5242 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑏 = (𝐹‘𝑐)) → (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦))) = (𝑦 ∈ (1...𝐾) ↦ ((𝐹‘𝑐)‘(𝑍‘𝑦)))) |
| 14 | 7 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐹‘𝑐) ∈ 𝐵) |
| 15 | | fzfid 14014 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1...𝐾) ∈ Fin) |
| 16 | 15 | mptexd 7244 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑦 ∈ (1...𝐾) ↦ ((𝐹‘𝑐)‘(𝑍‘𝑦))) ∈ V) |
| 17 | 10, 13, 14, 16 | fvmptd 7023 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐺‘(𝐹‘𝑐)) = (𝑦 ∈ (1...𝐾) ↦ ((𝐹‘𝑐)‘(𝑍‘𝑦)))) |
| 18 | 6 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑦 ∈ (1...𝐾)) → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))) |
| 19 | 18 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑦 ∈ (1...𝐾)) → (𝐹‘𝑐) = ((𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))‘𝑐)) |
| 20 | 19 | fveq1d 6908 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑦 ∈ (1...𝐾)) → ((𝐹‘𝑐)‘(𝑍‘𝑦)) = (((𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))‘𝑐)‘(𝑍‘𝑦))) |
| 21 | 20 | 3expa 1119 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → ((𝐹‘𝑐)‘(𝑍‘𝑦)) = (((𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))‘𝑐)‘(𝑍‘𝑦))) |
| 22 | 21 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑦 ∈ (1...𝐾) ↦ ((𝐹‘𝑐)‘(𝑍‘𝑦))) = (𝑦 ∈ (1...𝐾) ↦ (((𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))‘𝑐)‘(𝑍‘𝑦)))) |
| 23 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥)))) = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))) |
| 24 | | simplr 769 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑎 = 𝑐) ∧ 𝑥 ∈ 𝑆) → 𝑎 = 𝑐) |
| 25 | 24 | fveq1d 6908 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑎 = 𝑐) ∧ 𝑥 ∈ 𝑆) → (𝑎‘(◡𝑍‘𝑥)) = (𝑐‘(◡𝑍‘𝑥))) |
| 26 | 25 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑎 = 𝑐) → (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))) = (𝑥 ∈ 𝑆 ↦ (𝑐‘(◡𝑍‘𝑥)))) |
| 27 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → 𝑐 ∈ 𝐴) |
| 28 | | fzfid 14014 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝐾) ∈ Fin) |
| 29 | | f1oenfi 9219 |
. . . . . . . . . . . . . . 15
⊢
(((1...𝐾) ∈ Fin
∧ 𝑍:(1...𝐾)–1-1-onto→𝑆) → (1...𝐾) ≈ 𝑆) |
| 30 | 28, 5, 29 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...𝐾) ≈ 𝑆) |
| 31 | 30 | ensymd 9045 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ≈ (1...𝐾)) |
| 32 | | enfii 9226 |
. . . . . . . . . . . . 13
⊢
(((1...𝐾) ∈ Fin
∧ 𝑆 ≈ (1...𝐾)) → 𝑆 ∈ Fin) |
| 33 | 28, 31, 32 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Fin) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑆 ∈ Fin) |
| 35 | 34 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → 𝑆 ∈ Fin) |
| 36 | 35 | mptexd 7244 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → (𝑥 ∈ 𝑆 ↦ (𝑐‘(◡𝑍‘𝑥))) ∈ V) |
| 37 | 23, 26, 27, 36 | fvmptd 7023 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → ((𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))‘𝑐) = (𝑥 ∈ 𝑆 ↦ (𝑐‘(◡𝑍‘𝑥)))) |
| 38 | 37 | fveq1d 6908 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → (((𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))‘𝑐)‘(𝑍‘𝑦)) = ((𝑥 ∈ 𝑆 ↦ (𝑐‘(◡𝑍‘𝑥)))‘(𝑍‘𝑦))) |
| 39 | 38 | mpteq2dva 5242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑦 ∈ (1...𝐾) ↦ (((𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))‘𝑐)‘(𝑍‘𝑦))) = (𝑦 ∈ (1...𝐾) ↦ ((𝑥 ∈ 𝑆 ↦ (𝑐‘(◡𝑍‘𝑥)))‘(𝑍‘𝑦)))) |
| 40 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → (𝑥 ∈ 𝑆 ↦ (𝑐‘(◡𝑍‘𝑥))) = (𝑥 ∈ 𝑆 ↦ (𝑐‘(◡𝑍‘𝑥)))) |
| 41 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑥 = (𝑍‘𝑦)) → 𝑥 = (𝑍‘𝑦)) |
| 42 | 41 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑥 = (𝑍‘𝑦)) → (◡𝑍‘𝑥) = (◡𝑍‘(𝑍‘𝑦))) |
| 43 | 42 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑥 = (𝑍‘𝑦)) → (𝑐‘(◡𝑍‘𝑥)) = (𝑐‘(◡𝑍‘(𝑍‘𝑦)))) |
| 44 | | f1of 6848 |
. . . . . . . . . . . 12
⊢ (𝑍:(1...𝐾)–1-1-onto→𝑆 → 𝑍:(1...𝐾)⟶𝑆) |
| 45 | 5, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍:(1...𝐾)⟶𝑆) |
| 46 | 45 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑍:(1...𝐾)⟶𝑆) |
| 47 | 46 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → (𝑍‘𝑦) ∈ 𝑆) |
| 48 | | fvexd 6921 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → (𝑐‘(◡𝑍‘(𝑍‘𝑦))) ∈ V) |
| 49 | 40, 43, 47, 48 | fvmptd 7023 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → ((𝑥 ∈ 𝑆 ↦ (𝑐‘(◡𝑍‘𝑥)))‘(𝑍‘𝑦)) = (𝑐‘(◡𝑍‘(𝑍‘𝑦)))) |
| 50 | 49 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑦 ∈ (1...𝐾) ↦ ((𝑥 ∈ 𝑆 ↦ (𝑐‘(◡𝑍‘𝑥)))‘(𝑍‘𝑦))) = (𝑦 ∈ (1...𝐾) ↦ (𝑐‘(◡𝑍‘(𝑍‘𝑦))))) |
| 51 | 5 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → 𝑍:(1...𝐾)–1-1-onto→𝑆) |
| 52 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → 𝑦 ∈ (1...𝐾)) |
| 53 | | f1ocnvfv1 7296 |
. . . . . . . . . . 11
⊢ ((𝑍:(1...𝐾)–1-1-onto→𝑆 ∧ 𝑦 ∈ (1...𝐾)) → (◡𝑍‘(𝑍‘𝑦)) = 𝑦) |
| 54 | 51, 52, 53 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → (◡𝑍‘(𝑍‘𝑦)) = 𝑦) |
| 55 | 54 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑦 ∈ (1...𝐾)) → (𝑐‘(◡𝑍‘(𝑍‘𝑦))) = (𝑐‘𝑦)) |
| 56 | 55 | mpteq2dva 5242 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑦 ∈ (1...𝐾) ↦ (𝑐‘(◡𝑍‘(𝑍‘𝑦)))) = (𝑦 ∈ (1...𝐾) ↦ (𝑐‘𝑦))) |
| 57 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ 𝐴) |
| 58 | 3 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}) |
| 59 | 57, 58 | eleqtrd 2843 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)}) |
| 60 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑐 ∈ V |
| 61 | | feq1 6716 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑐 → (𝑔:(1...𝐾)⟶ℕ0 ↔ 𝑐:(1...𝐾)⟶ℕ0)) |
| 62 | | simpl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = 𝑐 ∧ 𝑖 ∈ (1...𝐾)) → 𝑔 = 𝑐) |
| 63 | 62 | fveq1d 6908 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 = 𝑐 ∧ 𝑖 ∈ (1...𝐾)) → (𝑔‘𝑖) = (𝑐‘𝑖)) |
| 64 | 63 | sumeq2dv 15738 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑐 → Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = Σ𝑖 ∈ (1...𝐾)(𝑐‘𝑖)) |
| 65 | 64 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑐 → (Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...𝐾)(𝑐‘𝑖) = 𝑁)) |
| 66 | 61, 65 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑐 → ((𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁) ↔ (𝑐:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑐‘𝑖) = 𝑁))) |
| 67 | 60, 66 | elab 3679 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑔‘𝑖) = 𝑁)} ↔ (𝑐:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑐‘𝑖) = 𝑁)) |
| 68 | 59, 67 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐:(1...𝐾)⟶ℕ0 ∧
Σ𝑖 ∈ (1...𝐾)(𝑐‘𝑖) = 𝑁)) |
| 69 | 68 | simpld 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐:(1...𝐾)⟶ℕ0) |
| 70 | | ffn 6736 |
. . . . . . . . . . 11
⊢ (𝑐:(1...𝐾)⟶ℕ0 → 𝑐 Fn (1...𝐾)) |
| 71 | 69, 70 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 Fn (1...𝐾)) |
| 72 | | dffn5 6967 |
. . . . . . . . . 10
⊢ (𝑐 Fn (1...𝐾) ↔ 𝑐 = (𝑦 ∈ (1...𝐾) ↦ (𝑐‘𝑦))) |
| 73 | 71, 72 | sylib 218 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 = (𝑦 ∈ (1...𝐾) ↦ (𝑐‘𝑦))) |
| 74 | 73 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑦 ∈ (1...𝐾) ↦ (𝑐‘𝑦)) = 𝑐) |
| 75 | 56, 74 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑦 ∈ (1...𝐾) ↦ (𝑐‘(◡𝑍‘(𝑍‘𝑦)))) = 𝑐) |
| 76 | 50, 75 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑦 ∈ (1...𝐾) ↦ ((𝑥 ∈ 𝑆 ↦ (𝑐‘(◡𝑍‘𝑥)))‘(𝑍‘𝑦))) = 𝑐) |
| 77 | 39, 76 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑦 ∈ (1...𝐾) ↦ (((𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))‘𝑐)‘(𝑍‘𝑦))) = 𝑐) |
| 78 | 22, 77 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑦 ∈ (1...𝐾) ↦ ((𝐹‘𝑐)‘(𝑍‘𝑦))) = 𝑐) |
| 79 | 17, 78 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐺‘(𝐹‘𝑐)) = 𝑐) |
| 80 | 79 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝐺‘(𝐹‘𝑐)) = 𝑐) |
| 81 | 6 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))))) |
| 82 | | simplr 769 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑎 = (𝐺‘𝑑)) ∧ 𝑥 ∈ 𝑆) → 𝑎 = (𝐺‘𝑑)) |
| 83 | 82 | fveq1d 6908 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑎 = (𝐺‘𝑑)) ∧ 𝑥 ∈ 𝑆) → (𝑎‘(◡𝑍‘𝑥)) = ((𝐺‘𝑑)‘(◡𝑍‘𝑥))) |
| 84 | 83 | mpteq2dva 5242 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑎 = (𝐺‘𝑑)) → (𝑥 ∈ 𝑆 ↦ (𝑎‘(◡𝑍‘𝑥))) = (𝑥 ∈ 𝑆 ↦ ((𝐺‘𝑑)‘(◡𝑍‘𝑥)))) |
| 85 | 9 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐺‘𝑑) ∈ 𝐴) |
| 86 | 33 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑆 ∈ Fin) |
| 87 | 86 | mptexd 7244 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑥 ∈ 𝑆 ↦ ((𝐺‘𝑑)‘(◡𝑍‘𝑥))) ∈ V) |
| 88 | 81, 84, 85, 87 | fvmptd 7023 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐹‘(𝐺‘𝑑)) = (𝑥 ∈ 𝑆 ↦ ((𝐺‘𝑑)‘(◡𝑍‘𝑥)))) |
| 89 | 8 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦))))) |
| 90 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) ∧ 𝑏 = 𝑑) ∧ 𝑦 ∈ (1...𝐾)) → 𝑏 = 𝑑) |
| 91 | 90 | fveq1d 6908 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) ∧ 𝑏 = 𝑑) ∧ 𝑦 ∈ (1...𝐾)) → (𝑏‘(𝑍‘𝑦)) = (𝑑‘(𝑍‘𝑦))) |
| 92 | 91 | mpteq2dva 5242 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) ∧ 𝑏 = 𝑑) → (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍‘𝑦))) = (𝑦 ∈ (1...𝐾) ↦ (𝑑‘(𝑍‘𝑦)))) |
| 93 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝑑 ∈ 𝐵) |
| 94 | | fzfid 14014 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → (1...𝐾) ∈ Fin) |
| 95 | 94 | mptexd 7244 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑦 ∈ (1...𝐾) ↦ (𝑑‘(𝑍‘𝑦))) ∈ V) |
| 96 | 89, 92, 93, 95 | fvmptd 7023 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑑) = (𝑦 ∈ (1...𝐾) ↦ (𝑑‘(𝑍‘𝑦)))) |
| 97 | 96 | fveq1d 6908 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → ((𝐺‘𝑑)‘(◡𝑍‘𝑥)) = ((𝑦 ∈ (1...𝐾) ↦ (𝑑‘(𝑍‘𝑦)))‘(◡𝑍‘𝑥))) |
| 98 | 97 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑥 ∈ 𝑆 ↦ ((𝐺‘𝑑)‘(◡𝑍‘𝑥))) = (𝑥 ∈ 𝑆 ↦ ((𝑦 ∈ (1...𝐾) ↦ (𝑑‘(𝑍‘𝑦)))‘(◡𝑍‘𝑥)))) |
| 99 | | eqidd 2738 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑦 ∈ (1...𝐾) ↦ (𝑑‘(𝑍‘𝑦))) = (𝑦 ∈ (1...𝐾) ↦ (𝑑‘(𝑍‘𝑦)))) |
| 100 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 = (◡𝑍‘𝑥)) → 𝑦 = (◡𝑍‘𝑥)) |
| 101 | 100 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 = (◡𝑍‘𝑥)) → (𝑍‘𝑦) = (𝑍‘(◡𝑍‘𝑥))) |
| 102 | 101 | fveq2d 6910 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 = (◡𝑍‘𝑥)) → (𝑑‘(𝑍‘𝑦)) = (𝑑‘(𝑍‘(◡𝑍‘𝑥)))) |
| 103 | | f1ocnv 6860 |
. . . . . . . . . . . 12
⊢ (𝑍:(1...𝐾)–1-1-onto→𝑆 → ◡𝑍:𝑆–1-1-onto→(1...𝐾)) |
| 104 | 5, 103 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝑍:𝑆–1-1-onto→(1...𝐾)) |
| 105 | | f1of 6848 |
. . . . . . . . . . 11
⊢ (◡𝑍:𝑆–1-1-onto→(1...𝐾) → ◡𝑍:𝑆⟶(1...𝐾)) |
| 106 | 104, 105 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝑍:𝑆⟶(1...𝐾)) |
| 107 | 106 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → ◡𝑍:𝑆⟶(1...𝐾)) |
| 108 | 107 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → (◡𝑍‘𝑥) ∈ (1...𝐾)) |
| 109 | | fvexd 6921 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑑‘(𝑍‘(◡𝑍‘𝑥))) ∈ V) |
| 110 | 99, 102, 108, 109 | fvmptd 7023 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → ((𝑦 ∈ (1...𝐾) ↦ (𝑑‘(𝑍‘𝑦)))‘(◡𝑍‘𝑥)) = (𝑑‘(𝑍‘(◡𝑍‘𝑥)))) |
| 111 | 110 | mpteq2dva 5242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑥 ∈ 𝑆 ↦ ((𝑦 ∈ (1...𝐾) ↦ (𝑑‘(𝑍‘𝑦)))‘(◡𝑍‘𝑥))) = (𝑥 ∈ 𝑆 ↦ (𝑑‘(𝑍‘(◡𝑍‘𝑥))))) |
| 112 | 5 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝑍:(1...𝐾)–1-1-onto→𝑆) |
| 113 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
| 114 | | f1ocnvfv2 7297 |
. . . . . . . . . 10
⊢ ((𝑍:(1...𝐾)–1-1-onto→𝑆 ∧ 𝑥 ∈ 𝑆) → (𝑍‘(◡𝑍‘𝑥)) = 𝑥) |
| 115 | 112, 113,
114 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑍‘(◡𝑍‘𝑥)) = 𝑥) |
| 116 | 115 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑑‘(𝑍‘(◡𝑍‘𝑥))) = (𝑑‘𝑥)) |
| 117 | 116 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑥 ∈ 𝑆 ↦ (𝑑‘(𝑍‘(◡𝑍‘𝑥)))) = (𝑥 ∈ 𝑆 ↦ (𝑑‘𝑥))) |
| 118 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 ∈ 𝐵) |
| 119 | 4 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝐵 = {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧
Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}) |
| 120 | 118, 119 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 ∈ {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧
Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)}) |
| 121 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑑 ∈ V |
| 122 | | feq1 6716 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝑑 → (ℎ:𝑆⟶ℕ0 ↔ 𝑑:𝑆⟶ℕ0)) |
| 123 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ = 𝑑 ∧ 𝑖 ∈ 𝑆) → ℎ = 𝑑) |
| 124 | 123 | fveq1d 6908 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ = 𝑑 ∧ 𝑖 ∈ 𝑆) → (ℎ‘𝑖) = (𝑑‘𝑖)) |
| 125 | 124 | sumeq2dv 15738 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝑑 → Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = Σ𝑖 ∈ 𝑆 (𝑑‘𝑖)) |
| 126 | 125 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝑑 → (Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁 ↔ Σ𝑖 ∈ 𝑆 (𝑑‘𝑖) = 𝑁)) |
| 127 | 122, 126 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑑 → ((ℎ:𝑆⟶ℕ0 ∧
Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁) ↔ (𝑑:𝑆⟶ℕ0 ∧
Σ𝑖 ∈ 𝑆 (𝑑‘𝑖) = 𝑁))) |
| 128 | 121, 127 | elab 3679 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ {ℎ ∣ (ℎ:𝑆⟶ℕ0 ∧
Σ𝑖 ∈ 𝑆 (ℎ‘𝑖) = 𝑁)} ↔ (𝑑:𝑆⟶ℕ0 ∧
Σ𝑖 ∈ 𝑆 (𝑑‘𝑖) = 𝑁)) |
| 129 | 120, 128 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑑:𝑆⟶ℕ0 ∧
Σ𝑖 ∈ 𝑆 (𝑑‘𝑖) = 𝑁)) |
| 130 | 129 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑:𝑆⟶ℕ0) |
| 131 | | ffn 6736 |
. . . . . . . . . 10
⊢ (𝑑:𝑆⟶ℕ0 → 𝑑 Fn 𝑆) |
| 132 | 130, 131 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 Fn 𝑆) |
| 133 | | dffn5 6967 |
. . . . . . . . 9
⊢ (𝑑 Fn 𝑆 ↔ 𝑑 = (𝑥 ∈ 𝑆 ↦ (𝑑‘𝑥))) |
| 134 | 132, 133 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → 𝑑 = (𝑥 ∈ 𝑆 ↦ (𝑑‘𝑥))) |
| 135 | 134 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑥 ∈ 𝑆 ↦ (𝑑‘𝑥)) = 𝑑) |
| 136 | 117, 135 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑥 ∈ 𝑆 ↦ (𝑑‘(𝑍‘(◡𝑍‘𝑥)))) = 𝑑) |
| 137 | 111, 136 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑥 ∈ 𝑆 ↦ ((𝑦 ∈ (1...𝐾) ↦ (𝑑‘(𝑍‘𝑦)))‘(◡𝑍‘𝑥))) = 𝑑) |
| 138 | 98, 137 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝑥 ∈ 𝑆 ↦ ((𝐺‘𝑑)‘(◡𝑍‘𝑥))) = 𝑑) |
| 139 | 88, 138 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ 𝐵) → (𝐹‘(𝐺‘𝑑)) = 𝑑) |
| 140 | 139 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑑 ∈ 𝐵 (𝐹‘(𝐺‘𝑑)) = 𝑑) |
| 141 | 7, 9, 80, 140 | 2fvidf1od 7318 |
1
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |