Theorem gicsym

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

	Ref	Expression
Assertion	gicsym	⊢ ( 𝑅 ≃𝑔 𝑆 → 𝑆 ≃𝑔 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		brgic	⊢ ( 𝑅 ≃𝑔 𝑆 ↔ ( 𝑅 GrpIso 𝑆 ) ≠ ∅ )
2		n0	⊢ ( ( 𝑅 GrpIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) )
3		gimcnv	⊢ ( 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) → ◡ 𝑓 ∈ ( 𝑆 GrpIso 𝑅 ) )
4		brgici	⊢ ( ◡ 𝑓 ∈ ( 𝑆 GrpIso 𝑅 ) → 𝑆 ≃𝑔 𝑅 )
5	3 4	syl	⊢ ( 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑆 ≃𝑔 𝑅 )
6	5	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑆 ≃𝑔 𝑅 )
7	2 6	sylbi	⊢ ( ( 𝑅 GrpIso 𝑆 ) ≠ ∅ → 𝑆 ≃𝑔 𝑅 )
8	1 7	sylbi	⊢ ( 𝑅 ≃𝑔 𝑆 → 𝑆 ≃𝑔 𝑅 )