Step |
Hyp |
Ref |
Expression |
1 |
|
efmnd1bas.1 |
⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) |
2 |
|
efmnd1bas.2 |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
3 |
|
efmnd1bas.0 |
⊢ 𝐴 = { 𝐼 } |
4 |
3
|
fveq2i |
⊢ ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ { 𝐼 } ) |
5 |
1 4
|
eqtri |
⊢ 𝐺 = ( EndoFMnd ‘ { 𝐼 } ) |
6 |
5 2
|
efmndbas |
⊢ 𝐵 = ( { 𝐼 } ↑m { 𝐼 } ) |
7 |
|
fsng |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉 ) → ( 𝑝 : { 𝐼 } ⟶ { 𝐼 } ↔ 𝑝 = { 〈 𝐼 , 𝐼 〉 } ) ) |
8 |
7
|
anidms |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝑝 : { 𝐼 } ⟶ { 𝐼 } ↔ 𝑝 = { 〈 𝐼 , 𝐼 〉 } ) ) |
9 |
|
snex |
⊢ { 𝐼 } ∈ V |
10 |
9 9
|
elmap |
⊢ ( 𝑝 ∈ ( { 𝐼 } ↑m { 𝐼 } ) ↔ 𝑝 : { 𝐼 } ⟶ { 𝐼 } ) |
11 |
|
velsn |
⊢ ( 𝑝 ∈ { { 〈 𝐼 , 𝐼 〉 } } ↔ 𝑝 = { 〈 𝐼 , 𝐼 〉 } ) |
12 |
8 10 11
|
3bitr4g |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝑝 ∈ ( { 𝐼 } ↑m { 𝐼 } ) ↔ 𝑝 ∈ { { 〈 𝐼 , 𝐼 〉 } } ) ) |
13 |
12
|
eqrdv |
⊢ ( 𝐼 ∈ 𝑉 → ( { 𝐼 } ↑m { 𝐼 } ) = { { 〈 𝐼 , 𝐼 〉 } } ) |
14 |
6 13
|
syl5eq |
⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = { { 〈 𝐼 , 𝐼 〉 } } ) |