Step |
Hyp |
Ref |
Expression |
1 |
|
df-gic |
⊢ ≃𝑔 = ( ◡ GrpIso “ ( V ∖ 1o ) ) |
2 |
|
cnvimass |
⊢ ( ◡ GrpIso “ ( V ∖ 1o ) ) ⊆ dom GrpIso |
3 |
|
gimfn |
⊢ GrpIso Fn ( Grp × Grp ) |
4 |
3
|
fndmi |
⊢ dom GrpIso = ( Grp × Grp ) |
5 |
2 4
|
sseqtri |
⊢ ( ◡ GrpIso “ ( V ∖ 1o ) ) ⊆ ( Grp × Grp ) |
6 |
1 5
|
eqsstri |
⊢ ≃𝑔 ⊆ ( Grp × Grp ) |
7 |
|
relxp |
⊢ Rel ( Grp × Grp ) |
8 |
|
relss |
⊢ ( ≃𝑔 ⊆ ( Grp × Grp ) → ( Rel ( Grp × Grp ) → Rel ≃𝑔 ) ) |
9 |
6 7 8
|
mp2 |
⊢ Rel ≃𝑔 |
10 |
|
gicsym |
⊢ ( 𝑥 ≃𝑔 𝑦 → 𝑦 ≃𝑔 𝑥 ) |
11 |
|
gictr |
⊢ ( ( 𝑥 ≃𝑔 𝑦 ∧ 𝑦 ≃𝑔 𝑧 ) → 𝑥 ≃𝑔 𝑧 ) |
12 |
|
gicref |
⊢ ( 𝑥 ∈ Grp → 𝑥 ≃𝑔 𝑥 ) |
13 |
|
giclcl |
⊢ ( 𝑥 ≃𝑔 𝑥 → 𝑥 ∈ Grp ) |
14 |
12 13
|
impbii |
⊢ ( 𝑥 ∈ Grp ↔ 𝑥 ≃𝑔 𝑥 ) |
15 |
9 10 11 14
|
iseri |
⊢ ≃𝑔 Er Grp |