fuciso

Description: A natural transformation is an isomorphism of functors iff all its components are isomorphisms. (Contributed by Mario Carneiro, 28-Jan-2017)

	Ref	Expression
Hypotheses	fuciso.q	$⊢ Q = C FuncCat D$
	fuciso.b	$⊢ B = {Base}_{C}$
	fuciso.n	$⊢ N = C Nat D$
	fuciso.f	$⊢ φ \to F \in (C Func D)$
	fuciso.g	$⊢ φ \to G \in (C Func D)$
	fuciso.i	$⊢ I = Iso (Q)$
	fuciso.j	$⊢ J = Iso (D)$
Assertion	fuciso	$⊢ φ \to (A \in (F I G) \leftrightarrow (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x))))$

Proof

Step	Hyp	Ref	Expression
1		fuciso.q	$⊢ Q = C FuncCat D$
2		fuciso.b	$⊢ B = {Base}_{C}$
3		fuciso.n	$⊢ N = C Nat D$
4		fuciso.f	$⊢ φ \to F \in (C Func D)$
5		fuciso.g	$⊢ φ \to G \in (C Func D)$
6		fuciso.i	$⊢ I = Iso (Q)$
7		fuciso.j	$⊢ J = Iso (D)$
8	1	fucbas	$⊢ C Func D = {Base}_{Q}$
9	1 3	fuchom	$⊢ N = Hom (Q)$
10		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
11	4 10	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
12	11	simpld	$⊢ φ \to C \in Cat$
13	11	simprd	$⊢ φ \to D \in Cat$
14	1 12 13	fuccat	$⊢ φ \to Q \in Cat$
15	8 9 6 14 4 5	isohom	$⊢ φ \to F I G \subseteq F N G$
16	15	sselda	$⊢ (φ \land A \in (F I G)) \to A \in (F N G)$
17		eqid	$⊢ {Base}_{D} = {Base}_{D}$
18		eqid	$⊢ Inv (D) = Inv (D)$
19	13	ad2antrr	$⊢ ((φ \land A \in (F I G)) \land x \in B) \to D \in Cat$
20		relfunc	$⊢ Rel (C Func D)$
21		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
22	20 4 21	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
23	2 17 22	funcf1	$⊢ φ \to 1^{st} (F) : B ⟶ {Base}_{D}$
24	23	adantr	$⊢ (φ \land A \in (F I G)) \to 1^{st} (F) : B ⟶ {Base}_{D}$
25	24	ffvelcdmda	$⊢ ((φ \land A \in (F I G)) \land x \in B) \to 1^{st} (F) (x) \in {Base}_{D}$
26		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
27	20 5 26	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
28	2 17 27	funcf1	$⊢ φ \to 1^{st} (G) : B ⟶ {Base}_{D}$
29	28	adantr	$⊢ (φ \land A \in (F I G)) \to 1^{st} (G) : B ⟶ {Base}_{D}$
30	29	ffvelcdmda	$⊢ ((φ \land A \in (F I G)) \land x \in B) \to 1^{st} (G) (x) \in {Base}_{D}$
31		eqid	$⊢ Inv (Q) = Inv (Q)$
32	8 31 14 4 5 6	isoval	$⊢ φ \to F I G = dom (F Inv (Q) G)$
33	32	eleq2d	$⊢ φ \to (A \in (F I G) \leftrightarrow A \in dom (F Inv (Q) G))$
34	8 31 14 4 5	invfun	$⊢ φ \to Fun (F Inv (Q) G)$
35		funfvbrb	$⊢ Fun (F Inv (Q) G) \to (A \in dom (F Inv (Q) G) \leftrightarrow A (F Inv (Q) G) (F Inv (Q) G) (A))$
36	34 35	syl	$⊢ φ \to (A \in dom (F Inv (Q) G) \leftrightarrow A (F Inv (Q) G) (F Inv (Q) G) (A))$
37	33 36	bitrd	$⊢ φ \to (A \in (F I G) \leftrightarrow A (F Inv (Q) G) (F Inv (Q) G) (A))$
38	37	biimpa	$⊢ (φ \land A \in (F I G)) \to A (F Inv (Q) G) (F Inv (Q) G) (A)$
39	1 2 3 4 5 31 18	fucinv	$⊢ φ \to (A (F Inv (Q) G) (F Inv (Q) G) (A) \leftrightarrow (A \in (F N G) \land (F Inv (Q) G) (A) \in (G N F) \land \forall x \in B A (x) (1^{st} (F) (x) Inv (D) 1^{st} (G) (x)) (F Inv (Q) G) (A) (x)))$
40	39	adantr	$⊢ (φ \land A \in (F I G)) \to (A (F Inv (Q) G) (F Inv (Q) G) (A) \leftrightarrow (A \in (F N G) \land (F Inv (Q) G) (A) \in (G N F) \land \forall x \in B A (x) (1^{st} (F) (x) Inv (D) 1^{st} (G) (x)) (F Inv (Q) G) (A) (x)))$
41	38 40	mpbid	$⊢ (φ \land A \in (F I G)) \to (A \in (F N G) \land (F Inv (Q) G) (A) \in (G N F) \land \forall x \in B A (x) (1^{st} (F) (x) Inv (D) 1^{st} (G) (x)) (F Inv (Q) G) (A) (x))$
42	41	simp3d	$⊢ (φ \land A \in (F I G)) \to \forall x \in B A (x) (1^{st} (F) (x) Inv (D) 1^{st} (G) (x)) (F Inv (Q) G) (A) (x)$
43	42	r19.21bi	$⊢ ((φ \land A \in (F I G)) \land x \in B) \to A (x) (1^{st} (F) (x) Inv (D) 1^{st} (G) (x)) (F Inv (Q) G) (A) (x)$
44	17 18 19 25 30 7 43	inviso1	$⊢ ((φ \land A \in (F I G)) \land x \in B) \to A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x))$
45	44	ralrimiva	$⊢ (φ \land A \in (F I G)) \to \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x))$
46	16 45	jca	$⊢ (φ \land A \in (F I G)) \to (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))$
47	14	adantr	$⊢ (φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \to Q \in Cat$
48	4	adantr	$⊢ (φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \to F \in (C Func D)$
49	5	adantr	$⊢ (φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \to G \in (C Func D)$
50		simprl	$⊢ (φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \to A \in (F N G)$
51	13	ad2antrr	$⊢ ((φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \land y \in B) \to D \in Cat$
52	23	adantr	$⊢ (φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \to 1^{st} (F) : B ⟶ {Base}_{D}$
53	52	ffvelcdmda	$⊢ ((φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \land y \in B) \to 1^{st} (F) (y) \in {Base}_{D}$
54	28	adantr	$⊢ (φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \to 1^{st} (G) : B ⟶ {Base}_{D}$
55	54	ffvelcdmda	$⊢ ((φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \land y \in B) \to 1^{st} (G) (y) \in {Base}_{D}$
56		simprr	$⊢ (φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \to \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x))$
57		fveq2	$⊢ x = y \to A (x) = A (y)$
58		fveq2	$⊢ x = y \to 1^{st} (F) (x) = 1^{st} (F) (y)$
59		fveq2	$⊢ x = y \to 1^{st} (G) (x) = 1^{st} (G) (y)$
60	58 59	oveq12d	$⊢ x = y \to 1^{st} (F) (x) J 1^{st} (G) (x) = 1^{st} (F) (y) J 1^{st} (G) (y)$
61	57 60	eleq12d	$⊢ x = y \to (A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)) \leftrightarrow A (y) \in (1^{st} (F) (y) J 1^{st} (G) (y)))$
62	61	rspccva	$⊢ (\forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)) \land y \in B) \to A (y) \in (1^{st} (F) (y) J 1^{st} (G) (y))$
63	56 62	sylan	$⊢ ((φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \land y \in B) \to A (y) \in (1^{st} (F) (y) J 1^{st} (G) (y))$
64	17 7 18 51 53 55 63	invisoinvr	$⊢ ((φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \land y \in B) \to A (y) (1^{st} (F) (y) Inv (D) 1^{st} (G) (y)) (1^{st} (F) (y) Inv (D) 1^{st} (G) (y)) (A (y))$
65	1 2 3 48 49 31 18 50 64	invfuc	$⊢ (φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \to A (F Inv (Q) G) (y \in B ⟼ (1^{st} (F) (y) Inv (D) 1^{st} (G) (y)) (A (y)))$
66	8 31 47 48 49 6 65	inviso1	$⊢ (φ \land (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x)))) \to A \in (F I G)$
67	46 66	impbida	$⊢ φ \to (A \in (F I G) \leftrightarrow (A \in (F N G) \land \forall x \in B A (x) \in (1^{st} (F) (x) J 1^{st} (G) (x))))$

Metamath Proof Explorer

Theorem fuciso

Proof