ffthiso

Description: A fully faithful functor reflects isomorphisms. Corollary 3.32 of Adamek p. 35. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	fthmon.b	$⊢ B = {Base}_{C}$
	fthmon.h	$⊢ H = Hom (C)$
	fthmon.f	$⊢ φ \to F (C Faith D) G$
	fthmon.x	$⊢ φ \to X \in B$
	fthmon.y	$⊢ φ \to Y \in B$
	fthmon.r	$⊢ φ \to R \in (X H Y)$
	ffthiso.f	$⊢ φ \to F (C Full D) G$
	ffthiso.s	$⊢ I = Iso (C)$
	ffthiso.t	$⊢ J = Iso (D)$
Assertion	ffthiso	$⊢ φ \to (R \in (X I Y) \leftrightarrow (X G Y) (R) \in (F (X) J F (Y)))$

Proof

Step	Hyp	Ref	Expression
1		fthmon.b	$⊢ B = {Base}_{C}$
2		fthmon.h	$⊢ H = Hom (C)$
3		fthmon.f	$⊢ φ \to F (C Faith D) G$
4		fthmon.x	$⊢ φ \to X \in B$
5		fthmon.y	$⊢ φ \to Y \in B$
6		fthmon.r	$⊢ φ \to R \in (X H Y)$
7		ffthiso.f	$⊢ φ \to F (C Full D) G$
8		ffthiso.s	$⊢ I = Iso (C)$
9		ffthiso.t	$⊢ J = Iso (D)$
10		fthfunc	$⊢ C Faith D \subseteq C Func D$
11	10	ssbri	$⊢ F (C Faith D) G \to F (C Func D) G$
12	3 11	syl	$⊢ φ \to F (C Func D) G$
13	12	adantr	$⊢ (φ \land R \in (X I Y)) \to F (C Func D) G$
14	4	adantr	$⊢ (φ \land R \in (X I Y)) \to X \in B$
15	5	adantr	$⊢ (φ \land R \in (X I Y)) \to Y \in B$
16		simpr	$⊢ (φ \land R \in (X I Y)) \to R \in (X I Y)$
17	1 8 9 13 14 15 16	funciso	$⊢ (φ \land R \in (X I Y)) \to (X G Y) (R) \in (F (X) J F (Y))$
18		eqid	$⊢ Inv (C) = Inv (C)$
19		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
20	12 19	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
21		funcrcl	$⊢ ⟨F, G⟩ \in (C Func D) \to (C \in Cat \land D \in Cat)$
22	20 21	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
23	22	simpld	$⊢ φ \to C \in Cat$
24	23	ad3antrrr	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to C \in Cat$
25	4	ad3antrrr	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to X \in B$
26	5	ad3antrrr	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to Y \in B$
27		eqid	$⊢ {Base}_{D} = {Base}_{D}$
28		eqid	$⊢ Inv (D) = Inv (D)$
29	22	simprd	$⊢ φ \to D \in Cat$
30	1 27 12	funcf1	$⊢ φ \to F : B ⟶ {Base}_{D}$
31	30 4	ffvelcdmd	$⊢ φ \to F (X) \in {Base}_{D}$
32	30 5	ffvelcdmd	$⊢ φ \to F (Y) \in {Base}_{D}$
33	27 28 29 31 32 9	isoval	$⊢ φ \to F (X) J F (Y) = dom (F (X) Inv (D) F (Y))$
34	33	eleq2d	$⊢ φ \to ((X G Y) (R) \in (F (X) J F (Y)) \leftrightarrow (X G Y) (R) \in dom (F (X) Inv (D) F (Y)))$
35	34	biimpa	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to (X G Y) (R) \in dom (F (X) Inv (D) F (Y))$
36	27 28 29 31 32	invfun	$⊢ φ \to Fun (F (X) Inv (D) F (Y))$
37	36	adantr	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to Fun (F (X) Inv (D) F (Y))$
38		funfvbrb	$⊢ Fun (F (X) Inv (D) F (Y)) \to ((X G Y) (R) \in dom (F (X) Inv (D) F (Y)) \leftrightarrow (X G Y) (R) (F (X) Inv (D) F (Y)) (F (X) Inv (D) F (Y)) ((X G Y) (R)))$
39	37 38	syl	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to ((X G Y) (R) \in dom (F (X) Inv (D) F (Y)) \leftrightarrow (X G Y) (R) (F (X) Inv (D) F (Y)) (F (X) Inv (D) F (Y)) ((X G Y) (R)))$
40	35 39	mpbid	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to (X G Y) (R) (F (X) Inv (D) F (Y)) (F (X) Inv (D) F (Y)) ((X G Y) (R))$
41	40	ad2antrr	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to (X G Y) (R) (F (X) Inv (D) F (Y)) (F (X) Inv (D) F (Y)) ((X G Y) (R))$
42		simpr	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)$
43	41 42	breqtrd	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to (X G Y) (R) (F (X) Inv (D) F (Y)) (Y G X) (f)$
44	3	ad3antrrr	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to F (C Faith D) G$
45	6	ad3antrrr	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to R \in (X H Y)$
46		simplr	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to f \in (Y H X)$
47	1 2 44 25 26 45 46 18 28	fthinv	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to (R (X Inv (C) Y) f \leftrightarrow (X G Y) (R) (F (X) Inv (D) F (Y)) (Y G X) (f))$
48	43 47	mpbird	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to R (X Inv (C) Y) f$
49	1 18 24 25 26 8 48	inviso1	$⊢ (((φ \land (X G Y) (R) \in (F (X) J F (Y))) \land f \in (Y H X)) \land (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)) \to R \in (X I Y)$
50		eqid	$⊢ Hom (D) = Hom (D)$
51	7	adantr	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to F (C Full D) G$
52	5	adantr	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to Y \in B$
53	4	adantr	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to X \in B$
54	27 50 9 29 32 31	isohom	$⊢ φ \to F (Y) J F (X) \subseteq F (Y) Hom (D) F (X)$
55	54	adantr	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to F (Y) J F (X) \subseteq F (Y) Hom (D) F (X)$
56	27 28 29 31 32 9	invf	$⊢ φ \to (F (X) Inv (D) F (Y)) : F (X) J F (Y) ⟶ F (Y) J F (X)$
57	56	ffvelcdmda	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to (F (X) Inv (D) F (Y)) ((X G Y) (R)) \in (F (Y) J F (X))$
58	55 57	sseldd	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to (F (X) Inv (D) F (Y)) ((X G Y) (R)) \in (F (Y) Hom (D) F (X))$
59	1 50 2 51 52 53 58	fulli	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to \exists f \in (Y H X) (F (X) Inv (D) F (Y)) ((X G Y) (R)) = (Y G X) (f)$
60	49 59	r19.29a	$⊢ (φ \land (X G Y) (R) \in (F (X) J F (Y))) \to R \in (X I Y)$
61	17 60	impbida	$⊢ φ \to (R \in (X I Y) \leftrightarrow (X G Y) (R) \in (F (X) J F (Y)))$

Metamath Proof Explorer

Theorem ffthiso

Proof