cicsym

		Ref	Expression
	Assertion	cicsym	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S) \to S ≃_{𝑐} (C) R$

Proof

Step	Hyp	Ref	Expression
1		cicrcl	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S) \to S \in {Base}_{C}$
2		ciclcl	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S) \to R \in {Base}_{C}$
3		eqid	$⊢ Iso (C) = Iso (C)$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5		simpl	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to C \in Cat$
6		simpr	$⊢ (S \in {Base}_{C} \land R \in {Base}_{C}) \to R \in {Base}_{C}$
7	6	adantl	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to R \in {Base}_{C}$
8		simpl	$⊢ (S \in {Base}_{C} \land R \in {Base}_{C}) \to S \in {Base}_{C}$
9	8	adantl	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to S \in {Base}_{C}$
10	3 4 5 7 9	cic	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (R ≃_{𝑐} (C) S \leftrightarrow \exists f f \in (R Iso (C) S))$
11		eqid	$⊢ Inv (C) = Inv (C)$
12	4 11 5 7 9 3	isoval	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to R Iso (C) S = dom (R Inv (C) S)$
13	4 11 5 9 7	invsym2	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to {(S Inv (C) R)}^{-1} = R Inv (C) S$
14	13	eqcomd	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to R Inv (C) S = {(S Inv (C) R)}^{-1}$
15	14	dmeqd	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to 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 \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to dom (R Inv (C) S) = ran (S Inv (C) R)$
18	12 17	eqtrd	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to R Iso (C) S = ran (S Inv (C) R)$
19	18	eleq2d	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (f \in (R Iso (C) S) \leftrightarrow f \in ran (S Inv (C) R))$
20		vex	$⊢ f \in V$
21		elrng	$⊢ f \in V \to (f \in ran (S Inv (C) R) \leftrightarrow \exists g g (S Inv (C) R) f)$
22	20 21	mp1i	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (f \in ran (S Inv (C) R) \leftrightarrow \exists g g (S Inv (C) R) f)$
23	19 22	bitrd	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (f \in (R Iso (C) S) \leftrightarrow \exists g g (S Inv (C) R) f)$
24		df-br	$⊢ g (S Inv (C) R) f \leftrightarrow ⟨g, f⟩ \in (S Inv (C) R)$
25	24	exbii	$⊢ \exists g g (S Inv (C) R) f \leftrightarrow \exists g ⟨g, f⟩ \in (S Inv (C) R)$
26		vex	$⊢ g \in V$
27	26 20	opeldm	$⊢ ⟨g, f⟩ \in (S Inv (C) R) \to g \in dom (S Inv (C) R)$
28	4 11 5 9 7 3	isoval	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to S Iso (C) R = dom (S Inv (C) R)$
29	28	eqcomd	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to dom (S Inv (C) R) = S Iso (C) R$
30	29	eleq2d	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (g \in dom (S Inv (C) R) \leftrightarrow g \in (S Iso (C) R))$
31	5	adantr	$⊢ ((C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \land g \in (S Iso (C) R)) \to C \in Cat$
32	9	adantr	$⊢ ((C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \land g \in (S Iso (C) R)) \to S \in {Base}_{C}$
33	7	adantr	$⊢ ((C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \land g \in (S Iso (C) R)) \to R \in {Base}_{C}$
34		simpr	$⊢ ((C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \land g \in (S Iso (C) R)) \to g \in (S Iso (C) R)$
35	3 4 31 32 33 34	brcici	$⊢ ((C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \land g \in (S Iso (C) R)) \to S ≃_{𝑐} (C) R$
36	35	ex	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (g \in (S Iso (C) R) \to S ≃_{𝑐} (C) R)$
37	30 36	sylbid	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (g \in dom (S Inv (C) R) \to S ≃_{𝑐} (C) R)$
38	27 37	syl5com	$⊢ ⟨g, f⟩ \in (S Inv (C) R) \to ((C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to S ≃_{𝑐} (C) R)$
39	38	exlimiv	$⊢ \exists g ⟨g, f⟩ \in (S Inv (C) R) \to ((C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to S ≃_{𝑐} (C) R)$
40	39	com12	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (\exists g ⟨g, f⟩ \in (S Inv (C) R) \to S ≃_{𝑐} (C) R)$
41	25 40	biimtrid	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (\exists g g (S Inv (C) R) f \to S ≃_{𝑐} (C) R)$
42	23 41	sylbid	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (f \in (R Iso (C) S) \to S ≃_{𝑐} (C) R)$
43	42	exlimdv	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (\exists f f \in (R Iso (C) S) \to S ≃_{𝑐} (C) R)$
44	10 43	sylbid	$⊢ (C \in Cat \land (S \in {Base}_{C} \land R \in {Base}_{C})) \to (R ≃_{𝑐} (C) S \to S ≃_{𝑐} (C) R)$
45	44	impancom	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S) \to ((S \in {Base}_{C} \land R \in {Base}_{C}) \to S ≃_{𝑐} (C) R)$
46	1 2 45	mp2and	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S) \to S ≃_{𝑐} (C) R$

Metamath Proof Explorer

Theorem cicsym

Proof