Proof of Theorem elptr2
| Step | Hyp | Ref
| Expression |
| 1 | | nffvmpt1 6917 |
. . . 4
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) |
| 2 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑦((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) |
| 3 | | fveq2 6906 |
. . . 4
⊢ (𝑦 = 𝑘 → ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) = ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘)) |
| 4 | 1, 2, 3 | cbvixp 8954 |
. . 3
⊢ X𝑦 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) = X𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) |
| 5 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴) |
| 6 | | elptr2.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ (𝐹‘𝑘)) |
| 7 | | eqid 2737 |
. . . . . 6
⊢ (𝑘 ∈ 𝐴 ↦ 𝑆) = (𝑘 ∈ 𝐴 ↦ 𝑆) |
| 8 | 7 | fvmpt2 7027 |
. . . . 5
⊢ ((𝑘 ∈ 𝐴 ∧ 𝑆 ∈ (𝐹‘𝑘)) → ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) = 𝑆) |
| 9 | 5, 6, 8 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) = 𝑆) |
| 10 | 9 | ixpeq2dva 8952 |
. . 3
⊢ (𝜑 → X𝑘 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) = X𝑘 ∈ 𝐴 𝑆) |
| 11 | 4, 10 | eqtrid 2789 |
. 2
⊢ (𝜑 → X𝑦 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) = X𝑘 ∈ 𝐴 𝑆) |
| 12 | | elptr2.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 13 | 6 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑆 ∈ (𝐹‘𝑘)) |
| 14 | 7 | fnmpt 6708 |
. . . 4
⊢
(∀𝑘 ∈
𝐴 𝑆 ∈ (𝐹‘𝑘) → (𝑘 ∈ 𝐴 ↦ 𝑆) Fn 𝐴) |
| 15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑆) Fn 𝐴) |
| 16 | 9, 6 | eqeltrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) ∈ (𝐹‘𝑘)) |
| 17 | 16 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) ∈ (𝐹‘𝑘)) |
| 18 | 1 | nfel1 2922 |
. . . . 5
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) ∈ (𝐹‘𝑦) |
| 19 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑦((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) ∈ (𝐹‘𝑘) |
| 20 | | fveq2 6906 |
. . . . . 6
⊢ (𝑦 = 𝑘 → (𝐹‘𝑦) = (𝐹‘𝑘)) |
| 21 | 3, 20 | eleq12d 2835 |
. . . . 5
⊢ (𝑦 = 𝑘 → (((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) ∈ (𝐹‘𝑦) ↔ ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) ∈ (𝐹‘𝑘))) |
| 22 | 18, 19, 21 | cbvralw 3306 |
. . . 4
⊢
(∀𝑦 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) ∈ (𝐹‘𝑦) ↔ ∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) ∈ (𝐹‘𝑘)) |
| 23 | 17, 22 | sylibr 234 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) ∈ (𝐹‘𝑦)) |
| 24 | | elptr2.2 |
. . 3
⊢ (𝜑 → 𝑊 ∈ Fin) |
| 25 | | eldifi 4131 |
. . . . . . 7
⊢ (𝑘 ∈ (𝐴 ∖ 𝑊) → 𝑘 ∈ 𝐴) |
| 26 | 25, 9 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) = 𝑆) |
| 27 | | elptr2.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝑆 = ∪ (𝐹‘𝑘)) |
| 28 | 26, 27 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) = ∪ (𝐹‘𝑘)) |
| 29 | 28 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ (𝐴 ∖ 𝑊)((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) = ∪ (𝐹‘𝑘)) |
| 30 | 1 | nfeq1 2921 |
. . . . 5
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) = ∪ (𝐹‘𝑦) |
| 31 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑦((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) = ∪ (𝐹‘𝑘) |
| 32 | 20 | unieqd 4920 |
. . . . . 6
⊢ (𝑦 = 𝑘 → ∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑘)) |
| 33 | 3, 32 | eqeq12d 2753 |
. . . . 5
⊢ (𝑦 = 𝑘 → (((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) = ∪ (𝐹‘𝑦) ↔ ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) = ∪ (𝐹‘𝑘))) |
| 34 | 30, 31, 33 | cbvralw 3306 |
. . . 4
⊢
(∀𝑦 ∈
(𝐴 ∖ 𝑊)((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) = ∪ (𝐹‘𝑦) ↔ ∀𝑘 ∈ (𝐴 ∖ 𝑊)((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑘) = ∪ (𝐹‘𝑘)) |
| 35 | 29, 34 | sylibr 234 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ (𝐴 ∖ 𝑊)((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) = ∪ (𝐹‘𝑦)) |
| 36 | | ptbas.1 |
. . . 4
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} |
| 37 | 36 | elptr 23581 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ((𝑘 ∈ 𝐴 ↦ 𝑆) Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) ∈ 𝐵) |
| 38 | 12, 15, 23, 24, 35, 37 | syl122anc 1381 |
. 2
⊢ (𝜑 → X𝑦 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝑆)‘𝑦) ∈ 𝐵) |
| 39 | 11, 38 | eqeltrrd 2842 |
1
⊢ (𝜑 → X𝑘 ∈
𝐴 𝑆 ∈ 𝐵) |