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 ∧ 𝑅 ( ≃𝑐𝐶 ) 𝑆𝑆 ( ≃𝑐𝐶 ) 𝑇 ) → 𝑅 ( ≃𝑐𝐶 ) 𝑇 )