Metamath Proof Explorer

Theorem cicsym

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

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

Proof

Step Hyp Ref Expression
1 cicrcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )
2 ciclcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ) → 𝑅 ∈ ( Base ‘ 𝐶 ) )
3 eqid ⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
6 simpr ⊢ ( ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( Base ‘ 𝐶 ) )
7 6 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐶 ) )
8 simpl ⊢ ( ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )
9 8 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )
10 3 4 5 7 9 cic ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ) )
11 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
12 4 11 5 7 9 3 isoval ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) = dom ( 𝑅 ( Inv ‘ 𝐶 ) 𝑆 ) )
13 4 11 5 9 7 invsym2 ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ◡ ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) = ( 𝑅 ( Inv ‘ 𝐶 ) 𝑆 ) )
14 13 eqcomd ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑅 ( Inv ‘ 𝐶 ) 𝑆 ) = ◡ ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) )
15 14 dmeqd ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → dom ( 𝑅 ( Inv ‘ 𝐶 ) 𝑆 ) = dom ◡ ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) )
16 df-rn ⊢ ran ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) = dom ◡ ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 )
17 15 16 eqtr4di ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → dom ( 𝑅 ( Inv ‘ 𝐶 ) 𝑆 ) = ran ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) )
18 12 17 eqtrd ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) = ran ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) )
19 18 eleq2d ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ↔ 𝑓 ∈ ran ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) ) )
20 vex ⊢ 𝑓 ∈ V
21 elrng ⊢ ( 𝑓 ∈ V → ( 𝑓 ∈ ran ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) ↔ ∃ 𝑔 𝑔 ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) 𝑓 ) )
22 20 21 mp1i ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ran ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) ↔ ∃ 𝑔 𝑔 ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) 𝑓 ) )
23 19 22 bitrd ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) ↔ ∃ 𝑔 𝑔 ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) 𝑓 ) )
24 df-br ⊢ ( 𝑔 ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) 𝑓 ↔ ⟨ 𝑔 , 𝑓 ⟩ ∈ ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) )
25 24 exbii ⊢ ( ∃ 𝑔 𝑔 ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) 𝑓 ↔ ∃ 𝑔 ⟨ 𝑔 , 𝑓 ⟩ ∈ ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) )
26 vex ⊢ 𝑔 ∈ V
27 26 20 opeldm ⊢ ( ⟨ 𝑔 , 𝑓 ⟩ ∈ ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) → 𝑔 ∈ dom ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) )
28 4 11 5 9 7 3 isoval ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑆 ( Iso ‘ 𝐶 ) 𝑅 ) = dom ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) )
29 28 eqcomd ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → dom ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) = ( 𝑆 ( Iso ‘ 𝐶 ) 𝑅 ) )
30 29 eleq2d ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ∈ dom ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) ↔ 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑅 ) ) )
31 5 adantr ⊢ ( ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑅 ) ) → 𝐶 ∈ Cat )
32 9 adantr ⊢ ( ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑅 ) ) → 𝑆 ∈ ( Base ‘ 𝐶 ) )
33 7 adantr ⊢ ( ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑅 ) ) → 𝑅 ∈ ( Base ‘ 𝐶 ) )
34 simpr ⊢ ( ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑅 ) ) → 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑅 ) )
35 3 4 31 32 33 34 brcici ⊢ ( ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑅 ) ) → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 )
36 35 ex ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ∈ ( 𝑆 ( Iso ‘ 𝐶 ) 𝑅 ) → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 ) )
37 30 36 sylbid ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ∈ dom ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 ) )
38 27 37 syl5com ⊢ ( ⟨ 𝑔 , 𝑓 ⟩ ∈ ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) → ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 ) )
39 38 exlimiv ⊢ ( ∃ 𝑔 ⟨ 𝑔 , 𝑓 ⟩ ∈ ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) → ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 ) )
40 39 com12 ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∃ 𝑔 ⟨ 𝑔 , 𝑓 ⟩ ∈ ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 ) )
41 25 40 syl5bi ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∃ 𝑔 𝑔 ( 𝑆 ( Inv ‘ 𝐶 ) 𝑅 ) 𝑓 → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 ) )
42 23 41 sylbid ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 ) )
43 42 exlimdv ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∃ 𝑓 𝑓 ∈ ( 𝑅 ( Iso ‘ 𝐶 ) 𝑆 ) → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 ) )
44 10 43 sylbid ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 ) )
45 44 impancom ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ) → ( ( 𝑆 ∈ ( Base ‘ 𝐶 ) ∧ 𝑅 ∈ ( Base ‘ 𝐶 ) ) → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 ) )
46 1 2 45 mp2and ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ) → 𝑆 ( ≃𝑐 ‘ 𝐶 ) 𝑅 )