Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cicsym Structured version   Visualization version   GIF version

Theorem cicsym 17065
 Description: Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.)
Assertion
Ref Expression
cicsym ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐𝐶)𝑆) → 𝑆( ≃𝑐𝐶)𝑅)

Proof of Theorem cicsym
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cicrcl 17064 . 2 ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐𝐶)𝑆) → 𝑆 ∈ (Base‘𝐶))
2 ciclcl 17063 . 2 ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐𝐶)𝑆) → 𝑅 ∈ (Base‘𝐶))
3 eqid 2822 . . . . 5 (Iso‘𝐶) = (Iso‘𝐶)
4 eqid 2822 . . . . 5 (Base‘𝐶) = (Base‘𝐶)
5 simpl 486 . . . . 5 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
6 simpr 488 . . . . . 6 ((𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶)) → 𝑅 ∈ (Base‘𝐶))
76adantl 485 . . . . 5 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → 𝑅 ∈ (Base‘𝐶))
8 simpl 486 . . . . . 6 ((𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶)) → 𝑆 ∈ (Base‘𝐶))
98adantl 485 . . . . 5 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → 𝑆 ∈ (Base‘𝐶))
103, 4, 5, 7, 9cic 17060 . . . 4 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑅( ≃𝑐𝐶)𝑆 ↔ ∃𝑓 𝑓 ∈ (𝑅(Iso‘𝐶)𝑆)))
11 eqid 2822 . . . . . . . . . 10 (Inv‘𝐶) = (Inv‘𝐶)
124, 11, 5, 7, 9, 3isoval 17026 . . . . . . . . 9 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑅(Iso‘𝐶)𝑆) = dom (𝑅(Inv‘𝐶)𝑆))
134, 11, 5, 9, 7invsym2 17024 . . . . . . . . . . . 12 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑆(Inv‘𝐶)𝑅) = (𝑅(Inv‘𝐶)𝑆))
1413eqcomd 2828 . . . . . . . . . . 11 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑅(Inv‘𝐶)𝑆) = (𝑆(Inv‘𝐶)𝑅))
1514dmeqd 5751 . . . . . . . . . 10 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → dom (𝑅(Inv‘𝐶)𝑆) = dom (𝑆(Inv‘𝐶)𝑅))
16 df-rn 5543 . . . . . . . . . 10 ran (𝑆(Inv‘𝐶)𝑅) = dom (𝑆(Inv‘𝐶)𝑅)
1715, 16eqtr4di 2875 . . . . . . . . 9 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → dom (𝑅(Inv‘𝐶)𝑆) = ran (𝑆(Inv‘𝐶)𝑅))
1812, 17eqtrd 2857 . . . . . . . 8 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑅(Iso‘𝐶)𝑆) = ran (𝑆(Inv‘𝐶)𝑅))
1918eleq2d 2899 . . . . . . 7 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑅(Iso‘𝐶)𝑆) ↔ 𝑓 ∈ ran (𝑆(Inv‘𝐶)𝑅)))
20 vex 3472 . . . . . . . 8 𝑓 ∈ V
21 elrng 5739 . . . . . . . 8 (𝑓 ∈ V → (𝑓 ∈ ran (𝑆(Inv‘𝐶)𝑅) ↔ ∃𝑔 𝑔(𝑆(Inv‘𝐶)𝑅)𝑓))
2220, 21mp1i 13 . . . . . . 7 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑓 ∈ ran (𝑆(Inv‘𝐶)𝑅) ↔ ∃𝑔 𝑔(𝑆(Inv‘𝐶)𝑅)𝑓))
2319, 22bitrd 282 . . . . . 6 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑅(Iso‘𝐶)𝑆) ↔ ∃𝑔 𝑔(𝑆(Inv‘𝐶)𝑅)𝑓))
24 df-br 5043 . . . . . . . 8 (𝑔(𝑆(Inv‘𝐶)𝑅)𝑓 ↔ ⟨𝑔, 𝑓⟩ ∈ (𝑆(Inv‘𝐶)𝑅))
2524exbii 1849 . . . . . . 7 (∃𝑔 𝑔(𝑆(Inv‘𝐶)𝑅)𝑓 ↔ ∃𝑔𝑔, 𝑓⟩ ∈ (𝑆(Inv‘𝐶)𝑅))
26 vex 3472 . . . . . . . . . . 11 𝑔 ∈ V
2726, 20opeldm 5753 . . . . . . . . . 10 (⟨𝑔, 𝑓⟩ ∈ (𝑆(Inv‘𝐶)𝑅) → 𝑔 ∈ dom (𝑆(Inv‘𝐶)𝑅))
284, 11, 5, 9, 7, 3isoval 17026 . . . . . . . . . . . . 13 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑆(Iso‘𝐶)𝑅) = dom (𝑆(Inv‘𝐶)𝑅))
2928eqcomd 2828 . . . . . . . . . . . 12 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → dom (𝑆(Inv‘𝐶)𝑅) = (𝑆(Iso‘𝐶)𝑅))
3029eleq2d 2899 . . . . . . . . . . 11 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑔 ∈ dom (𝑆(Inv‘𝐶)𝑅) ↔ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)))
315adantr 484 . . . . . . . . . . . . 13 (((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) → 𝐶 ∈ Cat)
329adantr 484 . . . . . . . . . . . . 13 (((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) → 𝑆 ∈ (Base‘𝐶))
337adantr 484 . . . . . . . . . . . . 13 (((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) → 𝑅 ∈ (Base‘𝐶))
34 simpr 488 . . . . . . . . . . . . 13 (((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) → 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅))
353, 4, 31, 32, 33, 34brcici 17061 . . . . . . . . . . . 12 (((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑆(Iso‘𝐶)𝑅)) → 𝑆( ≃𝑐𝐶)𝑅)
3635ex 416 . . . . . . . . . . 11 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑔 ∈ (𝑆(Iso‘𝐶)𝑅) → 𝑆( ≃𝑐𝐶)𝑅))
3730, 36sylbid 243 . . . . . . . . . 10 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑔 ∈ dom (𝑆(Inv‘𝐶)𝑅) → 𝑆( ≃𝑐𝐶)𝑅))
3827, 37syl5com 31 . . . . . . . . 9 (⟨𝑔, 𝑓⟩ ∈ (𝑆(Inv‘𝐶)𝑅) → ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → 𝑆( ≃𝑐𝐶)𝑅))
3938exlimiv 1931 . . . . . . . 8 (∃𝑔𝑔, 𝑓⟩ ∈ (𝑆(Inv‘𝐶)𝑅) → ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → 𝑆( ≃𝑐𝐶)𝑅))
4039com12 32 . . . . . . 7 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (∃𝑔𝑔, 𝑓⟩ ∈ (𝑆(Inv‘𝐶)𝑅) → 𝑆( ≃𝑐𝐶)𝑅))
4125, 40syl5bi 245 . . . . . 6 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (∃𝑔 𝑔(𝑆(Inv‘𝐶)𝑅)𝑓𝑆( ≃𝑐𝐶)𝑅))
4223, 41sylbid 243 . . . . 5 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑅(Iso‘𝐶)𝑆) → 𝑆( ≃𝑐𝐶)𝑅))
4342exlimdv 1934 . . . 4 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (∃𝑓 𝑓 ∈ (𝑅(Iso‘𝐶)𝑆) → 𝑆( ≃𝑐𝐶)𝑅))
4410, 43sylbid 243 . . 3 ((𝐶 ∈ Cat ∧ (𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶))) → (𝑅( ≃𝑐𝐶)𝑆𝑆( ≃𝑐𝐶)𝑅))
4544impancom 455 . 2 ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐𝐶)𝑆) → ((𝑆 ∈ (Base‘𝐶) ∧ 𝑅 ∈ (Base‘𝐶)) → 𝑆( ≃𝑐𝐶)𝑅))
461, 2, 45mp2and 698 1 ((𝐶 ∈ Cat ∧ 𝑅( ≃𝑐𝐶)𝑆) → 𝑆( ≃𝑐𝐶)𝑅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∃wex 1781   ∈ wcel 2114  Vcvv 3469  ⟨cop 4545   class class class wbr 5042  ◡ccnv 5531  dom cdm 5532  ran crn 5533  ‘cfv 6334  (class class class)co 7140  Basecbs 16474  Catccat 16926  Invcinv 17006  Isociso 17007   ≃𝑐 ccic 17056 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-ov 7143  df-oprab 7144  df-mpo 7145  df-1st 7675  df-2nd 7676  df-supp 7818  df-sect 17008  df-inv 17009  df-iso 17010  df-cic 17057 This theorem is referenced by:  cicer  17067  initoeu2  17267
 Copyright terms: Public domain W3C validator