Metamath Proof Explorer

Theorem cicsym

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

Ref Expression
Assertion cicsym ⊢ C ∈ Cat ∧ R ≃ 𝑐 ⁡ C S → S ≃ 𝑐 ⁡ C R

Proof

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