Step |
Hyp |
Ref |
Expression |
1 |
|
ptcmpg.1 |
⊢ 𝐽 = ( ∏t ‘ 𝐹 ) |
2 |
|
ptcmpg.2 |
⊢ 𝑋 = ∪ 𝐽 |
3 |
|
nfcv |
⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑎 ) |
4 |
|
nfcv |
⊢ Ⅎ 𝑎 ( 𝐹 ‘ 𝑘 ) |
5 |
|
nfcv |
⊢ Ⅎ 𝑘 ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑎 ) ) “ 𝑏 ) |
6 |
|
nfcv |
⊢ Ⅎ 𝑢 ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑎 ) ) “ 𝑏 ) |
7 |
|
nfcv |
⊢ Ⅎ 𝑎 ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) |
8 |
|
nfcv |
⊢ Ⅎ 𝑏 ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) |
9 |
|
fveq2 |
⊢ ( 𝑎 = 𝑘 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑘 ) ) |
10 |
|
fveq2 |
⊢ ( 𝑎 = 𝑘 → ( 𝑤 ‘ 𝑎 ) = ( 𝑤 ‘ 𝑘 ) ) |
11 |
10
|
mpteq2dv |
⊢ ( 𝑎 = 𝑘 → ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑎 ) ) = ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ) |
12 |
11
|
cnveqd |
⊢ ( 𝑎 = 𝑘 → ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑎 ) ) = ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ) |
13 |
12
|
imaeq1d |
⊢ ( 𝑎 = 𝑘 → ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑎 ) ) “ 𝑏 ) = ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑏 ) ) |
14 |
|
imaeq2 |
⊢ ( 𝑏 = 𝑢 → ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑏 ) = ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) |
15 |
13 14
|
sylan9eq |
⊢ ( ( 𝑎 = 𝑘 ∧ 𝑏 = 𝑢 ) → ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑎 ) ) “ 𝑏 ) = ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) |
16 |
3 4 5 6 7 8 9 15
|
cbvmpox |
⊢ ( 𝑎 ∈ 𝐴 , 𝑏 ∈ ( 𝐹 ‘ 𝑎 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑎 ) ) “ 𝑏 ) ) = ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) |
17 |
|
fveq2 |
⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) ) |
18 |
17
|
unieqd |
⊢ ( 𝑛 = 𝑚 → ∪ ( 𝐹 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑚 ) ) |
19 |
18
|
cbvixpv |
⊢ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = X 𝑚 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑚 ) |
20 |
|
simp1 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝐴 ∈ 𝑉 ) |
21 |
|
simp2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝐹 : 𝐴 ⟶ Comp ) |
22 |
|
cmptop |
⊢ ( 𝑘 ∈ Comp → 𝑘 ∈ Top ) |
23 |
22
|
ssriv |
⊢ Comp ⊆ Top |
24 |
|
fss |
⊢ ( ( 𝐹 : 𝐴 ⟶ Comp ∧ Comp ⊆ Top ) → 𝐹 : 𝐴 ⟶ Top ) |
25 |
21 23 24
|
sylancl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝐹 : 𝐴 ⟶ Top ) |
26 |
1
|
ptuni |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = ∪ 𝐽 ) |
27 |
20 25 26
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = ∪ 𝐽 ) |
28 |
27 2
|
eqtr4di |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = 𝑋 ) |
29 |
|
simp3 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝑋 ∈ ( UFL ∩ dom card ) ) |
30 |
28 29
|
eqeltrd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ∈ ( UFL ∩ dom card ) ) |
31 |
16 19 20 21 30
|
ptcmplem5 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → ( ∏t ‘ 𝐹 ) ∈ Comp ) |
32 |
1 31
|
eqeltrid |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝐽 ∈ Comp ) |