Step |
Hyp |
Ref |
Expression |
1 |
|
ptval.1 |
⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } |
2 |
|
df-pt |
⊢ ∏t = ( 𝑓 ∈ V ↦ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } ) ) |
3 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 ) |
4 |
3
|
dmeqd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = dom 𝐹 ) |
5 |
|
fndm |
⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 ) |
6 |
5
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → dom 𝐹 = 𝐴 ) |
7 |
4 6
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = 𝐴 ) |
8 |
7
|
fneq2d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( 𝑔 Fn dom 𝑓 ↔ 𝑔 Fn 𝐴 ) ) |
9 |
3
|
fveq1d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
10 |
9
|
eleq2d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) |
11 |
7 10
|
raleqbidv |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) |
12 |
7
|
difeq1d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( dom 𝑓 ∖ 𝑧 ) = ( 𝐴 ∖ 𝑧 ) ) |
13 |
9
|
unieqd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ∪ ( 𝑓 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) |
14 |
13
|
eqeq2d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) |
15 |
12 14
|
raleqbidv |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) |
16 |
15
|
rexbidv |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) |
17 |
8 11 16
|
3anbi123d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) |
18 |
7
|
ixpeq1d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) |
19 |
18
|
eqeq2d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ↔ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ) |
20 |
17 19
|
anbi12d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) ↔ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ) ) |
21 |
20
|
exbidv |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ) ) |
22 |
21
|
abbidv |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) |
23 |
22 1
|
eqtr4di |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } = 𝐵 ) |
24 |
23
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) ∧ 𝑓 = 𝐹 ) → ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn dom 𝑓 ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( dom 𝑓 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ dom 𝑓 ( 𝑔 ‘ 𝑦 ) ) } ) = ( topGen ‘ 𝐵 ) ) |
25 |
|
fnex |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V ) |
26 |
25
|
ancoms |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) → 𝐹 ∈ V ) |
27 |
|
fvexd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) → ( topGen ‘ 𝐵 ) ∈ V ) |
28 |
2 24 26 27
|
fvmptd2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) → ( ∏t ‘ 𝐹 ) = ( topGen ‘ 𝐵 ) ) |