Metamath Proof Explorer

Theorem cictr

Description: Isomorphism is transitive. (Contributed by AV, 5-Apr-2020)

Ref Expression
Assertion cictr ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ∧ 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 )

Proof

Step Hyp Ref Expression
1 ciclcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ) → 𝑅 ∈ ( Base ‘ 𝐶 ) )
2 cicrcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )
3 1 2 jca ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ) → ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) )
4 3 ex ⊢ ( 𝐶 ∈ Cat → ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 → ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ) )
5 cicrcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) → 𝑇 ∈ ( Base ‘ 𝐶 ) )
6 5 ex ⊢ ( 𝐶 ∈ Cat → ( 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 → 𝑇 ∈ ( Base ‘ 𝐶 ) ) )
7 4 6 anim12d ⊢ ( 𝐶 ∈ Cat → ( ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ∧ 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) → ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) )
8 7 3impib ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ∧ 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) → ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) )
9 eqid ⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
10 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
11 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
12 simpll ⊢ ( ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( Base ‘ 𝐶 ) )
13 12 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐶 ) )
14 simplr ⊢ ( ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )
15 14 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )
16 9 10 11 13 15 cic ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) )
17 simprr ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑇 ∈ ( Base ‘ 𝐶 ) )
18 9 10 11 15 17 cic ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ↔ ∃ 𝑔 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ) )
19 16 18 anbi12d ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ∧ 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) ↔ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ) ) )
20 11 adantl ⊢ ( ( ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) ∧ ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) ) → 𝐶 ∈ Cat )
21 13 adantl ⊢ ( ( ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) ∧ ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) ) → 𝑅 ∈ ( Base ‘ 𝐶 ) )
22 17 adantl ⊢ ( ( ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) ∧ ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) ) → 𝑇 ∈ ( Base ‘ 𝐶 ) )
23 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
24 15 adantl ⊢ ( ( ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) ∧ ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )
25 simplr ⊢ ( ( ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) ∧ ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) ) → 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) )
26 simpll ⊢ ( ( ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) ∧ ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) ) → 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) )
27 10 23 9 20 21 24 22 25 26 isoco ⊢ ( ( ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) ∧ ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) ) → ( 𝑔 ( ⟨ 𝑅 , 𝑆 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑇 ) )
28 9 10 20 21 22 27 brcici ⊢ ( ( ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) ∧ ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 )
29 28 ex ⊢ ( ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) → ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) )
30 29 ex ⊢ ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) → ( 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) → ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) ) )
31 30 exlimiv ⊢ ( ∃ 𝑔 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) → ( 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) → ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) ) )
32 31 com12 ⊢ ( 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) → ( ∃ 𝑔 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) → ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) ) )
33 32 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) → ( ∃ 𝑔 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) → ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) ) )
34 33 imp ⊢ ( ( ∃ 𝑓 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ) → ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) )
35 34 com12 ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ∃ 𝑓 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑇 ) ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) )
36 19 35 sylbid ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ∧ 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) )
37 36 ex ⊢ ( 𝐶 ∈ Cat → ( ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ∧ 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) ) )
38 37 com23 ⊢ ( 𝐶 ∈ Cat → ( ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ∧ 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) → ( ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) ) )
39 38 3impib ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ∧ 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) → ( ( ( 𝑅 ∈ ( Base ‘ 𝐶 ) ∧ 𝑆 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑇 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) )
40 8 39 mpd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ∧ 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑇 ) → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑇 )