fthinv

Description: A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	fthsect.b	$⊢ B = {Base}_{C}$
	fthsect.h	$⊢ H = Hom (C)$
	fthsect.f	$⊢ φ \to F (C Faith D) G$
	fthsect.x	$⊢ φ \to X \in B$
	fthsect.y	$⊢ φ \to Y \in B$
	fthsect.m	$⊢ φ \to M \in (X H Y)$
	fthsect.n	$⊢ φ \to N \in (Y H X)$
	fthinv.s	$⊢ I = Inv (C)$
	fthinv.t	$⊢ J = Inv (D)$
Assertion	fthinv	$⊢ φ \to (M (X I Y) N \leftrightarrow (X G Y) (M) (F (X) J F (Y)) (Y G X) (N))$

Proof

Step	Hyp	Ref	Expression
1		fthsect.b	$⊢ B = {Base}_{C}$
2		fthsect.h	$⊢ H = Hom (C)$
3		fthsect.f	$⊢ φ \to F (C Faith D) G$
4		fthsect.x	$⊢ φ \to X \in B$
5		fthsect.y	$⊢ φ \to Y \in B$
6		fthsect.m	$⊢ φ \to M \in (X H Y)$
7		fthsect.n	$⊢ φ \to N \in (Y H X)$
8		fthinv.s	$⊢ I = Inv (C)$
9		fthinv.t	$⊢ J = Inv (D)$
10		eqid	$⊢ Sect (C) = Sect (C)$
11		eqid	$⊢ Sect (D) = Sect (D)$
12	1 2 3 4 5 6 7 10 11	fthsect	$⊢ φ \to (M (X Sect (C) Y) N \leftrightarrow (X G Y) (M) (F (X) Sect (D) F (Y)) (Y G X) (N))$
13	1 2 3 5 4 7 6 10 11	fthsect	$⊢ φ \to (N (Y Sect (C) X) M \leftrightarrow (Y G X) (N) (F (Y) Sect (D) F (X)) (X G Y) (M))$
14	12 13	anbi12d	$⊢ φ \to ((M (X Sect (C) Y) N \land N (Y Sect (C) X) M) \leftrightarrow ((X G Y) (M) (F (X) Sect (D) F (Y)) (Y G X) (N) \land (Y G X) (N) (F (Y) Sect (D) F (X)) (X G Y) (M)))$
15		fthfunc	$⊢ C Faith D \subseteq C Func D$
16	15	ssbri	$⊢ F (C Faith D) G \to F (C Func D) G$
17	3 16	syl	$⊢ φ \to F (C Func D) G$
18		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
19	17 18	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
20		funcrcl	$⊢ ⟨F, G⟩ \in (C Func D) \to (C \in Cat \land D \in Cat)$
21	19 20	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
22	21	simpld	$⊢ φ \to C \in Cat$
23	1 8 22 4 5 10	isinv	$⊢ φ \to (M (X I Y) N \leftrightarrow (M (X Sect (C) Y) N \land N (Y Sect (C) X) M))$
24		eqid	$⊢ {Base}_{D} = {Base}_{D}$
25	21	simprd	$⊢ φ \to D \in Cat$
26	1 24 17	funcf1	$⊢ φ \to F : B ⟶ {Base}_{D}$
27	26 4	ffvelcdmd	$⊢ φ \to F (X) \in {Base}_{D}$
28	26 5	ffvelcdmd	$⊢ φ \to F (Y) \in {Base}_{D}$
29	24 9 25 27 28 11	isinv	$⊢ φ \to ((X G Y) (M) (F (X) J F (Y)) (Y G X) (N) \leftrightarrow ((X G Y) (M) (F (X) Sect (D) F (Y)) (Y G X) (N) \land (Y G X) (N) (F (Y) Sect (D) F (X)) (X G Y) (M)))$
30	14 23 29	3bitr4d	$⊢ φ \to (M (X I Y) N \leftrightarrow (X G Y) (M) (F (X) J F (Y)) (Y G X) (N))$

Metamath Proof Explorer

Theorem fthinv

Proof