dfiso2

Description: Alternate definition of an isomorphism of a category, according to definition 3.8 in Adamek p. 28. (Contributed by AV, 10-Apr-2020)

	Ref	Expression
Hypotheses	dfiso2.b	$⊢ B = {Base}_{C}$
	dfiso2.h	$⊢ H = Hom (C)$
	dfiso2.c	$⊢ φ \to C \in Cat$
	dfiso2.i	$⊢ I = Iso (C)$
	dfiso2.x	$⊢ φ \to X \in B$
	dfiso2.y	$⊢ φ \to Y \in B$
	dfiso2.f	$⊢ φ \to F \in (X H Y)$
	dfiso2.1	$⊢ \underset{˙}{1} = Id (C)$
	dfiso2.o	No typesetting found for \|- .o. = ( <. X , Y >. ( comp ` C ) X ) with typecode \|-
	dfiso2.p	$⊢ \underset{˙}{*} = ⟨Y, X⟩ comp (C) Y$
Assertion	dfiso2	Could not format assertion : No typesetting found for \|- ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		dfiso2.b	$⊢ B = {Base}_{C}$
2		dfiso2.h	$⊢ H = Hom (C)$
3		dfiso2.c	$⊢ φ \to C \in Cat$
4		dfiso2.i	$⊢ I = Iso (C)$
5		dfiso2.x	$⊢ φ \to X \in B$
6		dfiso2.y	$⊢ φ \to Y \in B$
7		dfiso2.f	$⊢ φ \to F \in (X H Y)$
8		dfiso2.1	$⊢ \underset{˙}{1} = Id (C)$
9		dfiso2.o	Could not format .o. = ( <. X , Y >. ( comp ` C ) X ) : No typesetting found for \|- .o. = ( <. X , Y >. ( comp ` C ) X ) with typecode \|-
10		dfiso2.p	$⊢ \underset{˙}{*} = ⟨Y, X⟩ comp (C) Y$
11		eqid	$⊢ Inv (C) = Inv (C)$
12	1 11 3 5 6 4	isoval	$⊢ φ \to X I Y = dom (X Inv (C) Y)$
13	12	eleq2d	$⊢ φ \to (F \in (X I Y) \leftrightarrow F \in dom (X Inv (C) Y))$
14		eqid	$⊢ Sect (C) = Sect (C)$
15	1 11 3 5 6 14	invfval	$⊢ φ \to X Inv (C) Y = (X Sect (C) Y) \cap {(Y Sect (C) X)}^{-1}$
16	15	dmeqd	$⊢ φ \to dom (X Inv (C) Y) = dom ((X Sect (C) Y) \cap {(Y Sect (C) X)}^{-1})$
17	16	eleq2d	$⊢ φ \to (F \in dom (X Inv (C) Y) \leftrightarrow F \in dom ((X Sect (C) Y) \cap {(Y Sect (C) X)}^{-1}))$
18		eqid	$⊢ comp (C) = comp (C)$
19	1 2 18 8 14 3 5 6	sectfval	$⊢ φ \to X Sect (C) Y = \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X))\}$
20	1 2 18 8 14 3 6 5	sectfval	$⊢ φ \to Y Sect (C) X = \{⟨g, f⟩ \| ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))\}$
21	20	cnveqd	$⊢ φ \to {(Y Sect (C) X)}^{-1} = {\{⟨g, f⟩ \| ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))\}}^{-1}$
22		cnvopab	$⊢ {\{⟨g, f⟩ \| ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))\}}^{-1} = \{⟨f, g⟩ \| ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))\}$
23	21 22	eqtrdi	$⊢ φ \to {(Y Sect (C) X)}^{-1} = \{⟨f, g⟩ \| ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))\}$
24	19 23	ineq12d	$⊢ φ \to (X Sect (C) Y) \cap {(Y Sect (C) X)}^{-1} = \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X))\} \cap \{⟨f, g⟩ \| ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))\}$
25		inopab	$⊢ \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X))\} \cap \{⟨f, g⟩ \| ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))\} = \{⟨f, g⟩ \| (((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X)) \land ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\}$
26		an4	$⊢ (((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X)) \land ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))) \leftrightarrow (((f \in (X H Y) \land g \in (Y H X)) \land (g \in (Y H X) \land f \in (X H Y))) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))$
27		an42	$⊢ ((f \in (X H Y) \land g \in (Y H X)) \land (g \in (Y H X) \land f \in (X H Y))) \leftrightarrow ((f \in (X H Y) \land g \in (Y H X)) \land (f \in (X H Y) \land g \in (Y H X)))$
28		anidm	$⊢ ((f \in (X H Y) \land g \in (Y H X)) \land (f \in (X H Y) \land g \in (Y H X))) \leftrightarrow (f \in (X H Y) \land g \in (Y H X))$
29	27 28	bitri	$⊢ ((f \in (X H Y) \land g \in (Y H X)) \land (g \in (Y H X) \land f \in (X H Y))) \leftrightarrow (f \in (X H Y) \land g \in (Y H X))$
30	29	anbi1i	$⊢ (((f \in (X H Y) \land g \in (Y H X)) \land (g \in (Y H X) \land f \in (X H Y))) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))) \leftrightarrow ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))$
31	26 30	bitri	$⊢ (((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X)) \land ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))) \leftrightarrow ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))$
32	31	opabbii	$⊢ \{⟨f, g⟩ \| (((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X)) \land ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\} = \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\}$
33	25 32	eqtri	$⊢ \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X))\} \cap \{⟨f, g⟩ \| ((g \in (Y H X) \land f \in (X H Y)) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))\} = \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\}$
34	24 33	eqtrdi	$⊢ φ \to (X Sect (C) Y) \cap {(Y Sect (C) X)}^{-1} = \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\}$
35	34	dmeqd	$⊢ φ \to dom ((X Sect (C) Y) \cap {(Y Sect (C) X)}^{-1}) = dom \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\}$
36		dmopab	$⊢ dom \{⟨f, g⟩ \| ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\} = \{f \| \exists g ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\}$
37	35 36	eqtrdi	$⊢ φ \to dom ((X Sect (C) Y) \cap {(Y Sect (C) X)}^{-1}) = \{f \| \exists g ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\}$
38	37	eleq2d	$⊢ φ \to (F \in dom ((X Sect (C) Y) \cap {(Y Sect (C) X)}^{-1}) \leftrightarrow F \in \{f \| \exists g ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\})$
39		eleq1	$⊢ f = F \to (f \in (X H Y) \leftrightarrow F \in (X H Y))$
40	39	anbi1d	$⊢ f = F \to ((f \in (X H Y) \land g \in (Y H X)) \leftrightarrow (F \in (X H Y) \land g \in (Y H X)))$
41		oveq2	$⊢ f = F \to g (⟨X, Y⟩ comp (C) X) f = g (⟨X, Y⟩ comp (C) X) F$
42	41	eqeq1d	$⊢ f = F \to (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \leftrightarrow g (⟨X, Y⟩ comp (C) X) F = \underset{˙}{1} (X))$
43		oveq1	$⊢ f = F \to f (⟨Y, X⟩ comp (C) Y) g = F (⟨Y, X⟩ comp (C) Y) g$
44	43	eqeq1d	$⊢ f = F \to (f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y) \leftrightarrow F (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))$
45	42 44	anbi12d	$⊢ f = F \to ((g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)) \leftrightarrow (g (⟨X, Y⟩ comp (C) X) F = \underset{˙}{1} (X) \land F (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))$
46	40 45	anbi12d	$⊢ f = F \to (((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))) \leftrightarrow ((F \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) F = \underset{˙}{1} (X) \land F (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))))$
47	46	exbidv	$⊢ f = F \to (\exists g ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))) \leftrightarrow \exists g ((F \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) F = \underset{˙}{1} (X) \land F (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))))$
48	47	elabg	$⊢ F \in (X H Y) \to (F \in \{f \| \exists g ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\} \leftrightarrow \exists g ((F \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) F = \underset{˙}{1} (X) \land F (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))))$
49	7 48	syl	$⊢ φ \to (F \in \{f \| \exists g ((f \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) f = \underset{˙}{1} (X) \land f (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y)))\} \leftrightarrow \exists g ((F \in (X H Y) \land g \in (Y H X)) \land (g (⟨X, Y⟩ comp (C) X) F = \underset{˙}{1} (X) \land F (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y))))$
50	7	biantrurd	$⊢ φ \to (g \in (Y H X) \leftrightarrow (F \in (X H Y) \land g \in (Y H X)))$
51	50	bicomd	$⊢ φ \to ((F \in (X H Y) \land g \in (Y H X)) \leftrightarrow g \in (Y H X))$
52	9	a1i	Could not format ( ph -> .o. = ( <. X , Y >. ( comp ` C ) X ) ) : No typesetting found for \|- ( ph -> .o. = ( <. X , Y >. ( comp ` C ) X ) ) with typecode \|-
53	52	eqcomd	Could not format ( ph -> ( <. X , Y >. ( comp ` C ) X ) = .o. ) : No typesetting found for \|- ( ph -> ( <. X , Y >. ( comp ` C ) X ) = .o. ) with typecode \|-
54	53	oveqd	Could not format ( ph -> ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( g .o. F ) ) : No typesetting found for \|- ( ph -> ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( g .o. F ) ) with typecode \|-
55	54	eqeq1d	Could not format ( ph -> ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) <-> ( g .o. F ) = ( .1. ` X ) ) ) : No typesetting found for \|- ( ph -> ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) <-> ( g .o. F ) = ( .1. ` X ) ) ) with typecode \|-
56	10	a1i	$⊢ φ \to \underset{˙}{*} = ⟨Y, X⟩ comp (C) Y$
57	56	eqcomd	$⊢ φ \to ⟨Y, X⟩ comp (C) Y = \underset{˙}{*}$
58	57	oveqd	$⊢ φ \to F (⟨Y, X⟩ comp (C) Y) g = F \underset{˙}{*} g$
59	58	eqeq1d	$⊢ φ \to (F (⟨Y, X⟩ comp (C) Y) g = \underset{˙}{1} (Y) \leftrightarrow F \underset{˙}{*} g = \underset{˙}{1} (Y))$
60	55 59	anbi12d	Could not format ( ph -> ( ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) <-> ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) : No typesetting found for \|- ( ph -> ( ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) <-> ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) with typecode \|-
61	51 60	anbi12d	Could not format ( ph -> ( ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> ( g e. ( Y H X ) /\ ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) ) : No typesetting found for \|- ( ph -> ( ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> ( g e. ( Y H X ) /\ ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) ) with typecode \|-
62	61	exbidv	Could not format ( ph -> ( E. g ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> E. g ( g e. ( Y H X ) /\ ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) ) : No typesetting found for \|- ( ph -> ( E. g ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> E. g ( g e. ( Y H X ) /\ ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) ) with typecode \|-
63		df-rex	Could not format ( E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) <-> E. g ( g e. ( Y H X ) /\ ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) : No typesetting found for \|- ( E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) <-> E. g ( g e. ( Y H X ) /\ ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) with typecode \|-
64	62 63	bitr4di	Could not format ( ph -> ( E. g ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) : No typesetting found for \|- ( ph -> ( E. g ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) with typecode \|-
65	38 49 64	3bitrd	Could not format ( ph -> ( F e. dom ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) : No typesetting found for \|- ( ph -> ( F e. dom ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) with typecode \|-
66	13 17 65	3bitrd	Could not format ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) : No typesetting found for \|- ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem dfiso2

Proof