gicref - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > gicref		Structured version Visualization version GIF version

Theorem gicref 19491

Description: Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016.)

**Assertion**
Ref	Expression
gicref	⊢ (𝑅 ∈ Grp → 𝑅 ≃_𝑔 𝑅)

**Proof of Theorem gicref**
Step	Hyp	Ref	Expression
1		eqid 2760	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
2	1	idghm 19450	. . 3 ⊢ (𝑅 ∈ Grp → ( I ↾ (Base‘𝑅)) ∈ (𝑅 GrpHom 𝑅))
3		cnvresid 6619	. . . 4 ⊢ ^◡( I ↾ (Base‘𝑅)) = ( I ↾ (Base‘𝑅))
4	3, 2	eqeltrid 2864	. . 3 ⊢ (𝑅 ∈ Grp → ^◡( I ↾ (Base‘𝑅)) ∈ (𝑅 GrpHom 𝑅))
5		isgim2 19484	. . 3 ⊢ (( I ↾ (Base‘𝑅)) ∈ (𝑅 GrpIso 𝑅) ↔ (( I ↾ (Base‘𝑅)) ∈ (𝑅 GrpHom 𝑅) ∧ ^◡( I ↾ (Base‘𝑅)) ∈ (𝑅 GrpHom 𝑅)))
6	2, 4, 5	sylanbrc 595	. 2 ⊢ (𝑅 ∈ Grp → ( I ↾ (Base‘𝑅)) ∈ (𝑅 GrpIso 𝑅))
7		brgici 19490	. 2 ⊢ (( I ↾ (Base‘𝑅)) ∈ (𝑅 GrpIso 𝑅) → 𝑅 ≃_𝑔 𝑅)
8	6, 7	syl 18	1 ⊢ (𝑅 ∈ Grp → 𝑅 ≃_𝑔 𝑅)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∈ wcel 2144 class class class wbr 5102 I cid 5544 ^◡ccnv 5649 ↾ cres 5652 ‘cfv 6538 (class class class)co 7420 Basecbs 17392 Grpcgrp 19149 GrpHom cghm 19432 GrpIso cgim 19476 ≃_𝑔 cgic 19477

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7423 df-oprab 7424 df-mpo 7425 df-1st 8001 df-2nd 8002 df-1o 8479 df-map 8852 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-grp 19152 df-ghm 19433 df-gim 19478 df-gic 19479

This theorem is used by: gicer 19496

W3C validator