Step |
Hyp |
Ref |
Expression |
1 |
|
elcntr.b |
⊢ 𝐵 = ( Base ‘ 𝑀 ) |
2 |
|
elcntr.p |
⊢ + = ( +g ‘ 𝑀 ) |
3 |
|
elcntr.z |
⊢ 𝑍 = ( Cntr ‘ 𝑀 ) |
4 |
|
eqid |
⊢ ( Cntz ‘ 𝑀 ) = ( Cntz ‘ 𝑀 ) |
5 |
1 4
|
cntrval |
⊢ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) = ( Cntr ‘ 𝑀 ) |
6 |
3 5
|
eqtr4i |
⊢ 𝑍 = ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) |
7 |
6
|
eleq2i |
⊢ ( 𝐴 ∈ 𝑍 ↔ 𝐴 ∈ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) ) |
8 |
|
ssid |
⊢ 𝐵 ⊆ 𝐵 |
9 |
1 2 4
|
elcntz |
⊢ ( 𝐵 ⊆ 𝐵 → ( 𝐴 ∈ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 + 𝑦 ) = ( 𝑦 + 𝐴 ) ) ) ) |
10 |
8 9
|
ax-mp |
⊢ ( 𝐴 ∈ ( ( Cntz ‘ 𝑀 ) ‘ 𝐵 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 + 𝑦 ) = ( 𝑦 + 𝐴 ) ) ) |
11 |
7 10
|
bitri |
⊢ ( 𝐴 ∈ 𝑍 ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 + 𝑦 ) = ( 𝑦 + 𝐴 ) ) ) |