Theorem gictr

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

	Ref	Expression
Assertion	gictr	⊢ ( ( 𝑅 ≃𝑔 𝑆 ∧ 𝑆 ≃𝑔 𝑇 ) → 𝑅 ≃𝑔 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		brgic	⊢ ( 𝑅 ≃𝑔 𝑆 ↔ ( 𝑅 GrpIso 𝑆 ) ≠ ∅ )
2		brgic	⊢ ( 𝑆 ≃𝑔 𝑇 ↔ ( 𝑆 GrpIso 𝑇 ) ≠ ∅ )
3		n0	⊢ ( ( 𝑅 GrpIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) )
4		n0	⊢ ( ( 𝑆 GrpIso 𝑇 ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( 𝑆 GrpIso 𝑇 ) )
5		exdistrv	⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑔 ∈ ( 𝑆 GrpIso 𝑇 ) ) ↔ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑆 GrpIso 𝑇 ) ) )
6		gimco	⊢ ( ( 𝑔 ∈ ( 𝑆 GrpIso 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑅 GrpIso 𝑇 ) )
7		brgici	⊢ ( ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑅 GrpIso 𝑇 ) → 𝑅 ≃𝑔 𝑇 )
8	6 7	syl	⊢ ( ( 𝑔 ∈ ( 𝑆 GrpIso 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) ) → 𝑅 ≃𝑔 𝑇 )
9	8	ancoms	⊢ ( ( 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑔 ∈ ( 𝑆 GrpIso 𝑇 ) ) → 𝑅 ≃𝑔 𝑇 )
10	9	exlimivv	⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝑔 ∈ ( 𝑆 GrpIso 𝑇 ) ) → 𝑅 ≃𝑔 𝑇 )
11	5 10	sylbir	⊢ ( ( ∃ 𝑓 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑆 GrpIso 𝑇 ) ) → 𝑅 ≃𝑔 𝑇 )
12	3 4 11	syl2anb	⊢ ( ( ( 𝑅 GrpIso 𝑆 ) ≠ ∅ ∧ ( 𝑆 GrpIso 𝑇 ) ≠ ∅ ) → 𝑅 ≃𝑔 𝑇 )
13	1 2 12	syl2anb	⊢ ( ( 𝑅 ≃𝑔 𝑆 ∧ 𝑆 ≃𝑔 𝑇 ) → 𝑅 ≃𝑔 𝑇 )