Step |
Hyp |
Ref |
Expression |
0 |
|
cefmnd |
⊢ EndoFMnd |
1 |
|
vx |
⊢ 𝑥 |
2 |
|
cvv |
⊢ V |
3 |
1
|
cv |
⊢ 𝑥 |
4 |
|
cmap |
⊢ ↑m |
5 |
3 3 4
|
co |
⊢ ( 𝑥 ↑m 𝑥 ) |
6 |
|
vb |
⊢ 𝑏 |
7 |
|
cbs |
⊢ Base |
8 |
|
cnx |
⊢ ndx |
9 |
8 7
|
cfv |
⊢ ( Base ‘ ndx ) |
10 |
6
|
cv |
⊢ 𝑏 |
11 |
9 10
|
cop |
⊢ 〈 ( Base ‘ ndx ) , 𝑏 〉 |
12 |
|
cplusg |
⊢ +g |
13 |
8 12
|
cfv |
⊢ ( +g ‘ ndx ) |
14 |
|
vf |
⊢ 𝑓 |
15 |
|
vg |
⊢ 𝑔 |
16 |
14
|
cv |
⊢ 𝑓 |
17 |
15
|
cv |
⊢ 𝑔 |
18 |
16 17
|
ccom |
⊢ ( 𝑓 ∘ 𝑔 ) |
19 |
14 15 10 10 18
|
cmpo |
⊢ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) |
20 |
13 19
|
cop |
⊢ 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 |
21 |
|
cts |
⊢ TopSet |
22 |
8 21
|
cfv |
⊢ ( TopSet ‘ ndx ) |
23 |
|
cpt |
⊢ ∏t |
24 |
3
|
cpw |
⊢ 𝒫 𝑥 |
25 |
24
|
csn |
⊢ { 𝒫 𝑥 } |
26 |
3 25
|
cxp |
⊢ ( 𝑥 × { 𝒫 𝑥 } ) |
27 |
26 23
|
cfv |
⊢ ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) |
28 |
22 27
|
cop |
⊢ 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) 〉 |
29 |
11 20 28
|
ctp |
⊢ { 〈 ( Base ‘ ndx ) , 𝑏 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) 〉 } |
30 |
6 5 29
|
csb |
⊢ ⦋ ( 𝑥 ↑m 𝑥 ) / 𝑏 ⦌ { 〈 ( Base ‘ ndx ) , 𝑏 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) 〉 } |
31 |
1 2 30
|
cmpt |
⊢ ( 𝑥 ∈ V ↦ ⦋ ( 𝑥 ↑m 𝑥 ) / 𝑏 ⦌ { 〈 ( Base ‘ ndx ) , 𝑏 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) 〉 } ) |
32 |
0 31
|
wceq |
⊢ EndoFMnd = ( 𝑥 ∈ V ↦ ⦋ ( 𝑥 ↑m 𝑥 ) / 𝑏 ⦌ { 〈 ( Base ‘ ndx ) , 𝑏 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) 〉 } ) |