| Step | Hyp | Ref
| Expression |
| 1 | | actfunsn.5 |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝑥 ∪ {〈𝐼, 𝑘〉})) |
| 2 | | uneq1 4161 |
. . . 4
⊢ (𝑥 = 𝑧 → (𝑥 ∪ {〈𝐼, 𝑘〉}) = (𝑧 ∪ {〈𝐼, 𝑘〉})) |
| 3 | 2 | cbvmptv 5255 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ (𝑥 ∪ {〈𝐼, 𝑘〉})) = (𝑧 ∈ 𝐴 ↦ (𝑧 ∪ {〈𝐼, 𝑘〉})) |
| 4 | 1, 3 | eqtri 2765 |
. 2
⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ (𝑧 ∪ {〈𝐼, 𝑘〉})) |
| 5 | | vex 3484 |
. . . 4
⊢ 𝑧 ∈ V |
| 6 | | snex 5436 |
. . . 4
⊢
{〈𝐼, 𝑘〉} ∈
V |
| 7 | 5, 6 | unex 7764 |
. . 3
⊢ (𝑧 ∪ {〈𝐼, 𝑘〉}) ∈ V |
| 8 | 7 | a1i 11 |
. 2
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (𝑧 ∪ {〈𝐼, 𝑘〉}) ∈ V) |
| 9 | | vex 3484 |
. . . 4
⊢ 𝑦 ∈ V |
| 10 | 9 | resex 6047 |
. . 3
⊢ (𝑦 ↾ 𝐵) ∈ V |
| 11 | 10 | a1i 11 |
. 2
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 ↾ 𝐵) ∈ V) |
| 12 | | rspe 3249 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → ∃𝑧 ∈ 𝐴 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) |
| 13 | 4, 7 | elrnmpti 5973 |
. . . . . . 7
⊢ (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝐴 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) |
| 14 | 12, 13 | sylibr 234 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝑦 ∈ ran 𝐹) |
| 15 | 14 | adantll 714 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝑦 ∈ ran 𝐹) |
| 16 | | simpr 484 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) |
| 17 | 16 | reseq1d 5996 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → (𝑦 ↾ 𝐵) = ((𝑧 ∪ {〈𝐼, 𝑘〉}) ↾ 𝐵)) |
| 18 | | actfunsn.1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐴 ⊆ (𝐶 ↑m 𝐵)) |
| 19 | 18 | sselda 3983 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ (𝐶 ↑m 𝐵)) |
| 20 | | elmapfn 8905 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐶 ↑m 𝐵) → 𝑧 Fn 𝐵) |
| 21 | 19, 20 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝑧 Fn 𝐵) |
| 22 | | actfunsn.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
| 23 | | fnsng 6618 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑘 ∈ 𝐶) → {〈𝐼, 𝑘〉} Fn {𝐼}) |
| 24 | 22, 23 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → {〈𝐼, 𝑘〉} Fn {𝐼}) |
| 25 | 24 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → {〈𝐼, 𝑘〉} Fn {𝐼}) |
| 26 | | actfunsn.4 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝐼 ∈ 𝐵) |
| 27 | | disjsn 4711 |
. . . . . . . . . . 11
⊢ ((𝐵 ∩ {𝐼}) = ∅ ↔ ¬ 𝐼 ∈ 𝐵) |
| 28 | 26, 27 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∩ {𝐼}) = ∅) |
| 29 | 28 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → (𝐵 ∩ {𝐼}) = ∅) |
| 30 | 29 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (𝐵 ∩ {𝐼}) = ∅) |
| 31 | | fnunres1 6680 |
. . . . . . . 8
⊢ ((𝑧 Fn 𝐵 ∧ {〈𝐼, 𝑘〉} Fn {𝐼} ∧ (𝐵 ∩ {𝐼}) = ∅) → ((𝑧 ∪ {〈𝐼, 𝑘〉}) ↾ 𝐵) = 𝑧) |
| 32 | 21, 25, 30, 31 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ((𝑧 ∪ {〈𝐼, 𝑘〉}) ↾ 𝐵) = 𝑧) |
| 33 | 32 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → ((𝑧 ∪ {〈𝐼, 𝑘〉}) ↾ 𝐵) = 𝑧) |
| 34 | 17, 33 | eqtr2d 2778 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝑧 = (𝑦 ↾ 𝐵)) |
| 35 | 15, 34 | jca 511 |
. . . 4
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 ↾ 𝐵))) |
| 36 | 35 | anasss 466 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉}))) → (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 ↾ 𝐵))) |
| 37 | | simpr 484 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 ↾ 𝐵)) → 𝑧 = (𝑦 ↾ 𝐵)) |
| 38 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) |
| 39 | 38 | reseq1d 5996 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → (𝑦 ↾ 𝐵) = ((𝑧 ∪ {〈𝐼, 𝑘〉}) ↾ 𝐵)) |
| 40 | 18 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝐴 ⊆ (𝐶 ↑m 𝐵)) |
| 41 | | simplr 769 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝑧 ∈ 𝐴) |
| 42 | 40, 41 | sseldd 3984 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝑧 ∈ (𝐶 ↑m 𝐵)) |
| 43 | 42, 20 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝑧 Fn 𝐵) |
| 44 | 22 | ad4antr 732 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝐼 ∈ 𝑉) |
| 45 | | simp-4r 784 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → 𝑘 ∈ 𝐶) |
| 46 | 44, 45, 23 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → {〈𝐼, 𝑘〉} Fn {𝐼}) |
| 47 | 28 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → (𝐵 ∩ {𝐼}) = ∅) |
| 48 | 43, 46, 47, 31 | syl3anc 1373 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → ((𝑧 ∪ {〈𝐼, 𝑘〉}) ↾ 𝐵) = 𝑧) |
| 49 | 48, 41 | eqeltrd 2841 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → ((𝑧 ∪ {〈𝐼, 𝑘〉}) ↾ 𝐵) ∈ 𝐴) |
| 50 | 39, 49 | eqeltrd 2841 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → (𝑦 ↾ 𝐵) ∈ 𝐴) |
| 51 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹) |
| 52 | 51, 13 | sylib 218 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑧 ∈ 𝐴 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) |
| 53 | 50, 52 | r19.29a 3162 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 ↾ 𝐵) ∈ 𝐴) |
| 54 | 53 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 ↾ 𝐵)) → (𝑦 ↾ 𝐵) ∈ 𝐴) |
| 55 | 37, 54 | eqeltrd 2841 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 ↾ 𝐵)) → 𝑧 ∈ 𝐴) |
| 56 | 37 | uneq1d 4167 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 ↾ 𝐵)) → (𝑧 ∪ {〈𝐼, 𝑘〉}) = ((𝑦 ↾ 𝐵) ∪ {〈𝐼, 𝑘〉})) |
| 57 | 39, 48 | eqtrd 2777 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → (𝑦 ↾ 𝐵) = 𝑧) |
| 58 | 57 | uneq1d 4167 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → ((𝑦 ↾ 𝐵) ∪ {〈𝐼, 𝑘〉}) = (𝑧 ∪ {〈𝐼, 𝑘〉})) |
| 59 | 58, 38 | eqtr4d 2780 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) → ((𝑦 ↾ 𝐵) ∪ {〈𝐼, 𝑘〉}) = 𝑦) |
| 60 | 59, 52 | r19.29a 3162 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 ↾ 𝐵) ∪ {〈𝐼, 𝑘〉}) = 𝑦) |
| 61 | 60 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 ↾ 𝐵)) → ((𝑦 ↾ 𝐵) ∪ {〈𝐼, 𝑘〉}) = 𝑦) |
| 62 | 56, 61 | eqtr2d 2778 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 ↾ 𝐵)) → 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) |
| 63 | 55, 62 | jca 511 |
. . . 4
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 ↾ 𝐵)) → (𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉}))) |
| 64 | 63 | anasss 466 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐶) ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 ↾ 𝐵))) → (𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉}))) |
| 65 | 36, 64 | impbida 801 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → ((𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 ∪ {〈𝐼, 𝑘〉})) ↔ (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 ↾ 𝐵)))) |
| 66 | 4, 8, 11, 65 | f1od 7685 |
1
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐹:𝐴–1-1-onto→ran
𝐹) |