Step |
Hyp |
Ref |
Expression |
1 |
|
efmnd.1 |
⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) |
2 |
|
efmnd.2 |
⊢ 𝐵 = ( 𝐴 ↑m 𝐴 ) |
3 |
|
efmnd.3 |
⊢ + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) |
4 |
|
efmnd.4 |
⊢ 𝐽 = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) |
5 |
|
elex |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V ) |
6 |
|
ovexd |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 ↑m 𝑎 ) ∈ V ) |
7 |
|
id |
⊢ ( 𝑏 = ( 𝑎 ↑m 𝑎 ) → 𝑏 = ( 𝑎 ↑m 𝑎 ) ) |
8 |
|
id |
⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 ) |
9 |
8 8
|
oveq12d |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 ↑m 𝑎 ) = ( 𝐴 ↑m 𝐴 ) ) |
10 |
9 2
|
eqtr4di |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 ↑m 𝑎 ) = 𝐵 ) |
11 |
7 10
|
sylan9eqr |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → 𝑏 = 𝐵 ) |
12 |
11
|
opeq2d |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → 〈 ( Base ‘ ndx ) , 𝑏 〉 = 〈 ( Base ‘ ndx ) , 𝐵 〉 ) |
13 |
|
eqidd |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → ( 𝑓 ∘ 𝑔 ) = ( 𝑓 ∘ 𝑔 ) ) |
14 |
11 11 13
|
mpoeq123dv |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) ) |
15 |
14 3
|
eqtr4di |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) = + ) |
16 |
15
|
opeq2d |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 = 〈 ( +g ‘ ndx ) , + 〉 ) |
17 |
|
simpl |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → 𝑎 = 𝐴 ) |
18 |
|
pweq |
⊢ ( 𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴 ) |
19 |
18
|
sneqd |
⊢ ( 𝑎 = 𝐴 → { 𝒫 𝑎 } = { 𝒫 𝐴 } ) |
20 |
19
|
adantr |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → { 𝒫 𝑎 } = { 𝒫 𝐴 } ) |
21 |
17 20
|
xpeq12d |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → ( 𝑎 × { 𝒫 𝑎 } ) = ( 𝐴 × { 𝒫 𝐴 } ) ) |
22 |
21
|
fveq2d |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ) |
23 |
22 4
|
eqtr4di |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) = 𝐽 ) |
24 |
23
|
opeq2d |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) 〉 = 〈 ( TopSet ‘ ndx ) , 𝐽 〉 ) |
25 |
12 16 24
|
tpeq123d |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = ( 𝑎 ↑m 𝑎 ) ) → { 〈 ( Base ‘ ndx ) , 𝑏 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) 〉 } = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } ) |
26 |
6 25
|
csbied |
⊢ ( 𝑎 = 𝐴 → ⦋ ( 𝑎 ↑m 𝑎 ) / 𝑏 ⦌ { 〈 ( Base ‘ ndx ) , 𝑏 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) 〉 } = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } ) |
27 |
|
df-efmnd |
⊢ EndoFMnd = ( 𝑎 ∈ V ↦ ⦋ ( 𝑎 ↑m 𝑎 ) / 𝑏 ⦌ { 〈 ( Base ‘ ndx ) , 𝑏 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) 〉 } ) |
28 |
|
tpex |
⊢ { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } ∈ V |
29 |
26 27 28
|
fvmpt |
⊢ ( 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } ) |
30 |
5 29
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → ( EndoFMnd ‘ 𝐴 ) = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } ) |
31 |
1 30
|
eqtrid |
⊢ ( 𝐴 ∈ 𝑉 → 𝐺 = { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , + 〉 , 〈 ( TopSet ‘ ndx ) , 𝐽 〉 } ) |