Step | Hyp | Ref
| Expression |
1 | | df-pt 16105 |
. . 3
⊢
∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))})) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → ∏t = (𝑓 ∈ V ↦
(topGen‘{𝑥 ∣
∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}))) |
3 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) |
4 | 3 | dmeqd 5326 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → dom 𝑓 = dom 𝐹) |
5 | | fndm 5990 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
6 | 5 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → dom 𝐹 = 𝐴) |
7 | 4, 6 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → dom 𝑓 = 𝐴) |
8 | 7 | fneq2d 5982 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (𝑔 Fn dom 𝑓 ↔ 𝑔 Fn 𝐴)) |
9 | 3 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (𝑓‘𝑦) = (𝐹‘𝑦)) |
10 | 9 | eleq2d 2687 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → ((𝑔‘𝑦) ∈ (𝑓‘𝑦) ↔ (𝑔‘𝑦) ∈ (𝐹‘𝑦))) |
11 | 7, 10 | raleqbidv 3152 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦))) |
12 | 7 | difeq1d 3727 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (dom 𝑓 ∖ 𝑧) = (𝐴 ∖ 𝑧)) |
13 | 9 | unieqd 4446 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → ∪ (𝑓‘𝑦) = ∪ (𝐹‘𝑦)) |
14 | 13 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → ((𝑔‘𝑦) = ∪ (𝑓‘𝑦) ↔ (𝑔‘𝑦) = ∪ (𝐹‘𝑦))) |
15 | 12, 14 | raleqbidv 3152 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦))) |
16 | 15 | rexbidv 3052 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦) ↔ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦))) |
17 | 8, 11, 16 | 3anbi123d 1399 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → ((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ↔ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)))) |
18 | 7 | ixpeq1d 7920 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → X𝑦 ∈ dom 𝑓(𝑔‘𝑦) = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) |
19 | 18 | eqeq2d 2632 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦) ↔ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))) |
20 | 17, 19 | anbi12d 747 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦)) ↔ ((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)))) |
21 | 20 | exbidv 1850 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦)) ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)))) |
22 | 21 | abbidv 2741 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → {𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}) |
23 | | ptval.1 |
. . . 4
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} |
24 | 22, 23 | syl6eqr 2674 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → {𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))} = 𝐵) |
25 | 24 | fveq2d 6195 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}) = (topGen‘𝐵)) |
26 | | fnex 6481 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
27 | 26 | ancoms 469 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → 𝐹 ∈ V) |
28 | | fvexd 6203 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → (topGen‘𝐵) ∈ V) |
29 | 2, 25, 27, 28 | fvmptd 6288 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → (∏t‘𝐹) = (topGen‘𝐵)) |