Step |
Hyp |
Ref |
Expression |
1 |
|
df-ric |
⊢ ≃𝑟 = ( ◡ RingIso “ ( V ∖ 1o ) ) |
2 |
|
ovex |
⊢ ( 𝑟 RingHom 𝑠 ) ∈ V |
3 |
|
rabexg |
⊢ ( ( 𝑟 RingHom 𝑠 ) ∈ V → { ℎ ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ ℎ ∈ ( 𝑠 RingHom 𝑟 ) } ∈ V ) |
4 |
2 3
|
mp1i |
⊢ ( ( 𝑟 ∈ V ∧ 𝑠 ∈ V ) → { ℎ ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ ℎ ∈ ( 𝑠 RingHom 𝑟 ) } ∈ V ) |
5 |
4
|
rgen2 |
⊢ ∀ 𝑟 ∈ V ∀ 𝑠 ∈ V { ℎ ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ ℎ ∈ ( 𝑠 RingHom 𝑟 ) } ∈ V |
6 |
|
df-rngiso |
⊢ RingIso = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { ℎ ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ ℎ ∈ ( 𝑠 RingHom 𝑟 ) } ) |
7 |
6
|
fnmpo |
⊢ ( ∀ 𝑟 ∈ V ∀ 𝑠 ∈ V { ℎ ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ ℎ ∈ ( 𝑠 RingHom 𝑟 ) } ∈ V → RingIso Fn ( V × V ) ) |
8 |
5 7
|
ax-mp |
⊢ RingIso Fn ( V × V ) |
9 |
1 8
|
brwitnlem |
⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ ) |