Step | Hyp | Ref
| Expression |
1 | | brgic 17534 |
. . 3
⊢ (𝑅 ≃𝑔
𝑆 ↔ (𝑅 GrpIso 𝑆) ≠ ∅) |
2 | | n0 3890 |
. . 3
⊢ ((𝑅 GrpIso 𝑆) ≠ ∅ ↔ ∃𝑎 𝑎 ∈ (𝑅 GrpIso 𝑆)) |
3 | 1, 2 | bitri 263 |
. 2
⊢ (𝑅 ≃𝑔
𝑆 ↔ ∃𝑎 𝑎 ∈ (𝑅 GrpIso 𝑆)) |
4 | | fvex 6113 |
. . . . 5
⊢
(SubGrp‘𝑅)
∈ V |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝑎 ∈ (𝑅 GrpIso 𝑆) → (SubGrp‘𝑅) ∈ V) |
6 | | fvex 6113 |
. . . . 5
⊢
(SubGrp‘𝑆)
∈ V |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝑎 ∈ (𝑅 GrpIso 𝑆) → (SubGrp‘𝑆) ∈ V) |
8 | | vex 3176 |
. . . . . 6
⊢ 𝑎 ∈ V |
9 | 8 | imaex 6996 |
. . . . 5
⊢ (𝑎 “ 𝑏) ∈ V |
10 | 9 | 2a1i 12 |
. . . 4
⊢ (𝑎 ∈ (𝑅 GrpIso 𝑆) → (𝑏 ∈ (SubGrp‘𝑅) → (𝑎 “ 𝑏) ∈ V)) |
11 | 8 | cnvex 7006 |
. . . . . 6
⊢ ◡𝑎 ∈ V |
12 | 11 | imaex 6996 |
. . . . 5
⊢ (◡𝑎 “ 𝑐) ∈ V |
13 | 12 | 2a1i 12 |
. . . 4
⊢ (𝑎 ∈ (𝑅 GrpIso 𝑆) → (𝑐 ∈ (SubGrp‘𝑆) → (◡𝑎 “ 𝑐) ∈ V)) |
14 | | gimghm 17529 |
. . . . . . . . 9
⊢ (𝑎 ∈ (𝑅 GrpIso 𝑆) → 𝑎 ∈ (𝑅 GrpHom 𝑆)) |
15 | | ghmima 17504 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (𝑅 GrpHom 𝑆) ∧ 𝑏 ∈ (SubGrp‘𝑅)) → (𝑎 “ 𝑏) ∈ (SubGrp‘𝑆)) |
16 | 14, 15 | sylan 487 |
. . . . . . . 8
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑏 ∈ (SubGrp‘𝑅)) → (𝑎 “ 𝑏) ∈ (SubGrp‘𝑆)) |
17 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) |
18 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝑆) =
(Base‘𝑆) |
19 | 17, 18 | gimf1o 17528 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝑅 GrpIso 𝑆) → 𝑎:(Base‘𝑅)–1-1-onto→(Base‘𝑆)) |
20 | | f1of1 6049 |
. . . . . . . . . . 11
⊢ (𝑎:(Base‘𝑅)–1-1-onto→(Base‘𝑆) → 𝑎:(Base‘𝑅)–1-1→(Base‘𝑆)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (𝑅 GrpIso 𝑆) → 𝑎:(Base‘𝑅)–1-1→(Base‘𝑆)) |
22 | 17 | subgss 17418 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (SubGrp‘𝑅) → 𝑏 ⊆ (Base‘𝑅)) |
23 | | f1imacnv 6066 |
. . . . . . . . . 10
⊢ ((𝑎:(Base‘𝑅)–1-1→(Base‘𝑆) ∧ 𝑏 ⊆ (Base‘𝑅)) → (◡𝑎 “ (𝑎 “ 𝑏)) = 𝑏) |
24 | 21, 22, 23 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑏 ∈ (SubGrp‘𝑅)) → (◡𝑎 “ (𝑎 “ 𝑏)) = 𝑏) |
25 | 24 | eqcomd 2616 |
. . . . . . . 8
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑏 ∈ (SubGrp‘𝑅)) → 𝑏 = (◡𝑎 “ (𝑎 “ 𝑏))) |
26 | 16, 25 | jca 553 |
. . . . . . 7
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑏 ∈ (SubGrp‘𝑅)) → ((𝑎 “ 𝑏) ∈ (SubGrp‘𝑆) ∧ 𝑏 = (◡𝑎 “ (𝑎 “ 𝑏)))) |
27 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑐 = (𝑎 “ 𝑏) → (𝑐 ∈ (SubGrp‘𝑆) ↔ (𝑎 “ 𝑏) ∈ (SubGrp‘𝑆))) |
28 | | imaeq2 5381 |
. . . . . . . . 9
⊢ (𝑐 = (𝑎 “ 𝑏) → (◡𝑎 “ 𝑐) = (◡𝑎 “ (𝑎 “ 𝑏))) |
29 | 28 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑐 = (𝑎 “ 𝑏) → (𝑏 = (◡𝑎 “ 𝑐) ↔ 𝑏 = (◡𝑎 “ (𝑎 “ 𝑏)))) |
30 | 27, 29 | anbi12d 743 |
. . . . . . 7
⊢ (𝑐 = (𝑎 “ 𝑏) → ((𝑐 ∈ (SubGrp‘𝑆) ∧ 𝑏 = (◡𝑎 “ 𝑐)) ↔ ((𝑎 “ 𝑏) ∈ (SubGrp‘𝑆) ∧ 𝑏 = (◡𝑎 “ (𝑎 “ 𝑏))))) |
31 | 26, 30 | syl5ibrcom 236 |
. . . . . 6
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑏 ∈ (SubGrp‘𝑅)) → (𝑐 = (𝑎 “ 𝑏) → (𝑐 ∈ (SubGrp‘𝑆) ∧ 𝑏 = (◡𝑎 “ 𝑐)))) |
32 | 31 | impr 647 |
. . . . 5
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ (𝑏 ∈ (SubGrp‘𝑅) ∧ 𝑐 = (𝑎 “ 𝑏))) → (𝑐 ∈ (SubGrp‘𝑆) ∧ 𝑏 = (◡𝑎 “ 𝑐))) |
33 | | ghmpreima 17505 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (𝑅 GrpHom 𝑆) ∧ 𝑐 ∈ (SubGrp‘𝑆)) → (◡𝑎 “ 𝑐) ∈ (SubGrp‘𝑅)) |
34 | 14, 33 | sylan 487 |
. . . . . . . 8
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑐 ∈ (SubGrp‘𝑆)) → (◡𝑎 “ 𝑐) ∈ (SubGrp‘𝑅)) |
35 | | f1ofo 6057 |
. . . . . . . . . . 11
⊢ (𝑎:(Base‘𝑅)–1-1-onto→(Base‘𝑆) → 𝑎:(Base‘𝑅)–onto→(Base‘𝑆)) |
36 | 19, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (𝑅 GrpIso 𝑆) → 𝑎:(Base‘𝑅)–onto→(Base‘𝑆)) |
37 | 18 | subgss 17418 |
. . . . . . . . . 10
⊢ (𝑐 ∈ (SubGrp‘𝑆) → 𝑐 ⊆ (Base‘𝑆)) |
38 | | foimacnv 6067 |
. . . . . . . . . 10
⊢ ((𝑎:(Base‘𝑅)–onto→(Base‘𝑆) ∧ 𝑐 ⊆ (Base‘𝑆)) → (𝑎 “ (◡𝑎 “ 𝑐)) = 𝑐) |
39 | 36, 37, 38 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑐 ∈ (SubGrp‘𝑆)) → (𝑎 “ (◡𝑎 “ 𝑐)) = 𝑐) |
40 | 39 | eqcomd 2616 |
. . . . . . . 8
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑐 ∈ (SubGrp‘𝑆)) → 𝑐 = (𝑎 “ (◡𝑎 “ 𝑐))) |
41 | 34, 40 | jca 553 |
. . . . . . 7
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑐 ∈ (SubGrp‘𝑆)) → ((◡𝑎 “ 𝑐) ∈ (SubGrp‘𝑅) ∧ 𝑐 = (𝑎 “ (◡𝑎 “ 𝑐)))) |
42 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑏 = (◡𝑎 “ 𝑐) → (𝑏 ∈ (SubGrp‘𝑅) ↔ (◡𝑎 “ 𝑐) ∈ (SubGrp‘𝑅))) |
43 | | imaeq2 5381 |
. . . . . . . . 9
⊢ (𝑏 = (◡𝑎 “ 𝑐) → (𝑎 “ 𝑏) = (𝑎 “ (◡𝑎 “ 𝑐))) |
44 | 43 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑏 = (◡𝑎 “ 𝑐) → (𝑐 = (𝑎 “ 𝑏) ↔ 𝑐 = (𝑎 “ (◡𝑎 “ 𝑐)))) |
45 | 42, 44 | anbi12d 743 |
. . . . . . 7
⊢ (𝑏 = (◡𝑎 “ 𝑐) → ((𝑏 ∈ (SubGrp‘𝑅) ∧ 𝑐 = (𝑎 “ 𝑏)) ↔ ((◡𝑎 “ 𝑐) ∈ (SubGrp‘𝑅) ∧ 𝑐 = (𝑎 “ (◡𝑎 “ 𝑐))))) |
46 | 41, 45 | syl5ibrcom 236 |
. . . . . 6
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑐 ∈ (SubGrp‘𝑆)) → (𝑏 = (◡𝑎 “ 𝑐) → (𝑏 ∈ (SubGrp‘𝑅) ∧ 𝑐 = (𝑎 “ 𝑏)))) |
47 | 46 | impr 647 |
. . . . 5
⊢ ((𝑎 ∈ (𝑅 GrpIso 𝑆) ∧ (𝑐 ∈ (SubGrp‘𝑆) ∧ 𝑏 = (◡𝑎 “ 𝑐))) → (𝑏 ∈ (SubGrp‘𝑅) ∧ 𝑐 = (𝑎 “ 𝑏))) |
48 | 32, 47 | impbida 873 |
. . . 4
⊢ (𝑎 ∈ (𝑅 GrpIso 𝑆) → ((𝑏 ∈ (SubGrp‘𝑅) ∧ 𝑐 = (𝑎 “ 𝑏)) ↔ (𝑐 ∈ (SubGrp‘𝑆) ∧ 𝑏 = (◡𝑎 “ 𝑐)))) |
49 | 5, 7, 10, 13, 48 | en2d 7877 |
. . 3
⊢ (𝑎 ∈ (𝑅 GrpIso 𝑆) → (SubGrp‘𝑅) ≈ (SubGrp‘𝑆)) |
50 | 49 | exlimiv 1845 |
. 2
⊢
(∃𝑎 𝑎 ∈ (𝑅 GrpIso 𝑆) → (SubGrp‘𝑅) ≈ (SubGrp‘𝑆)) |
51 | 3, 50 | sylbi 206 |
1
⊢ (𝑅 ≃𝑔
𝑆 →
(SubGrp‘𝑅) ≈
(SubGrp‘𝑆)) |