dfiso3

Description: Alternate definition of an isomorphism of a category as a section in both directions. (Contributed by AV, 11-Apr-2020)

	Ref	Expression
Hypotheses	dfiso3.b	$⊢ B = {Base}_{C}$
	dfiso3.h	$⊢ H = Hom (C)$
	dfiso3.i	$⊢ I = Iso (C)$
	dfiso3.s	$⊢ S = Sect (C)$
	dfiso3.c	$⊢ φ \to C \in Cat$
	dfiso3.x	$⊢ φ \to X \in B$
	dfiso3.y	$⊢ φ \to Y \in B$
	dfiso3.f	$⊢ φ \to F \in (X H Y)$
Assertion	dfiso3	$⊢ φ \to (F \in (X I Y) \leftrightarrow \exists g \in (Y H X) (g (Y S X) F \land F (X S Y) g))$

Proof

Step	Hyp	Ref	Expression
1		dfiso3.b	$⊢ B = {Base}_{C}$
2		dfiso3.h	$⊢ H = Hom (C)$
3		dfiso3.i	$⊢ I = Iso (C)$
4		dfiso3.s	$⊢ S = Sect (C)$
5		dfiso3.c	$⊢ φ \to C \in Cat$
6		dfiso3.x	$⊢ φ \to X \in B$
7		dfiso3.y	$⊢ φ \to Y \in B$
8		dfiso3.f	$⊢ φ \to F \in (X H Y)$
9		eqid	$⊢ Id (C) = Id (C)$
10		eqid	$⊢ ⟨X, Y⟩ comp (C) X = ⟨X, Y⟩ comp (C) X$
11		eqid	$⊢ ⟨Y, X⟩ comp (C) Y = ⟨Y, X⟩ comp (C) Y$
12	1 2 5 3 6 7 8 9 10 11	dfiso2	$⊢ φ \to (F \in (X I Y) \leftrightarrow \exists g \in (Y H X) (g (⟨X, Y⟩ comp (C) X) F = Id (C) (X) \land F (⟨Y, X⟩ comp (C) Y) g = Id (C) (Y)))$
13		eqid	$⊢ comp (C) = comp (C)$
14	5	adantr	$⊢ (φ \land g \in (Y H X)) \to C \in Cat$
15	7	adantr	$⊢ (φ \land g \in (Y H X)) \to Y \in B$
16	6	adantr	$⊢ (φ \land g \in (Y H X)) \to X \in B$
17		simpr	$⊢ (φ \land g \in (Y H X)) \to g \in (Y H X)$
18	8	adantr	$⊢ (φ \land g \in (Y H X)) \to F \in (X H Y)$
19	1 2 13 9 4 14 15 16 17 18	issect2	$⊢ (φ \land g \in (Y H X)) \to (g (Y S X) F \leftrightarrow F (⟨Y, X⟩ comp (C) Y) g = Id (C) (Y))$
20	1 2 13 9 4 14 16 15 18 17	issect2	$⊢ (φ \land g \in (Y H X)) \to (F (X S Y) g \leftrightarrow g (⟨X, Y⟩ comp (C) X) F = Id (C) (X))$
21	19 20	anbi12d	$⊢ (φ \land g \in (Y H X)) \to ((g (Y S X) F \land F (X S Y) g) \leftrightarrow (F (⟨Y, X⟩ comp (C) Y) g = Id (C) (Y) \land g (⟨X, Y⟩ comp (C) X) F = Id (C) (X)))$
22		ancom	$⊢ (F (⟨Y, X⟩ comp (C) Y) g = Id (C) (Y) \land g (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow (g (⟨X, Y⟩ comp (C) X) F = Id (C) (X) \land F (⟨Y, X⟩ comp (C) Y) g = Id (C) (Y))$
23	21 22	bitr2di	$⊢ (φ \land g \in (Y H X)) \to ((g (⟨X, Y⟩ comp (C) X) F = Id (C) (X) \land F (⟨Y, X⟩ comp (C) Y) g = Id (C) (Y)) \leftrightarrow (g (Y S X) F \land F (X S Y) g))$
24	23	rexbidva	$⊢ φ \to (\exists g \in (Y H X) (g (⟨X, Y⟩ comp (C) X) F = Id (C) (X) \land F (⟨Y, X⟩ comp (C) Y) g = Id (C) (Y)) \leftrightarrow \exists g \in (Y H X) (g (Y S X) F \land F (X S Y) g))$
25	12 24	bitrd	$⊢ φ \to (F \in (X I Y) \leftrightarrow \exists g \in (Y H X) (g (Y S X) F \land F (X S Y) g))$

Metamath Proof Explorer

Theorem dfiso3

Proof