inveq

Description: If there are two inverses of a morphism, these inverses are equal. Corollary 3.11 of Adamek p. 28. (Contributed by AV, 10-Apr-2020) (Revised by AV, 3-Jul-2022)

	Ref	Expression
Hypotheses	inveq.b	$⊢ B = {Base}_{C}$
	inveq.n	$⊢ N = Inv (C)$
	inveq.c	$⊢ φ \to C \in Cat$
	inveq.x	$⊢ φ \to X \in B$
	inveq.y	$⊢ φ \to Y \in B$
Assertion	inveq	$⊢ φ \to ((F (X N Y) G \land F (X N Y) K) \to G = K)$

Proof

Step	Hyp	Ref	Expression
1		inveq.b	$⊢ B = {Base}_{C}$
2		inveq.n	$⊢ N = Inv (C)$
3		inveq.c	$⊢ φ \to C \in Cat$
4		inveq.x	$⊢ φ \to X \in B$
5		inveq.y	$⊢ φ \to Y \in B$
6		eqid	$⊢ Sect (C) = Sect (C)$
7	3	adantr	$⊢ (φ \land (F (X N Y) G \land F (X N Y) K)) \to C \in Cat$
8	5	adantr	$⊢ (φ \land (F (X N Y) G \land F (X N Y) K)) \to Y \in B$
9	4	adantr	$⊢ (φ \land (F (X N Y) G \land F (X N Y) K)) \to X \in B$
10	1 2 3 4 5 6	isinv	$⊢ φ \to (F (X N Y) G \leftrightarrow (F (X Sect (C) Y) G \land G (Y Sect (C) X) F))$
11		simpr	$⊢ (F (X Sect (C) Y) G \land G (Y Sect (C) X) F) \to G (Y Sect (C) X) F$
12	10 11	biimtrdi	$⊢ φ \to (F (X N Y) G \to G (Y Sect (C) X) F)$
13	12	com12	$⊢ F (X N Y) G \to (φ \to G (Y Sect (C) X) F)$
14	13	adantr	$⊢ (F (X N Y) G \land F (X N Y) K) \to (φ \to G (Y Sect (C) X) F)$
15	14	impcom	$⊢ (φ \land (F (X N Y) G \land F (X N Y) K)) \to G (Y Sect (C) X) F$
16	1 2 3 4 5 6	isinv	$⊢ φ \to (F (X N Y) K \leftrightarrow (F (X Sect (C) Y) K \land K (Y Sect (C) X) F))$
17		simpl	$⊢ (F (X Sect (C) Y) K \land K (Y Sect (C) X) F) \to F (X Sect (C) Y) K$
18	16 17	biimtrdi	$⊢ φ \to (F (X N Y) K \to F (X Sect (C) Y) K)$
19	18	adantld	$⊢ φ \to ((F (X N Y) G \land F (X N Y) K) \to F (X Sect (C) Y) K)$
20	19	imp	$⊢ (φ \land (F (X N Y) G \land F (X N Y) K)) \to F (X Sect (C) Y) K$
21	1 6 7 8 9 15 20	sectcan	$⊢ (φ \land (F (X N Y) G \land F (X N Y) K)) \to G = K$
22	21	ex	$⊢ φ \to ((F (X N Y) G \land F (X N Y) K) \to G = K)$

Metamath Proof Explorer

Theorem inveq

Proof