invfuc

Description: If V ( x ) is an inverse to U ( x ) for each x , and U is a natural transformation, then V is also a natural transformation, and they are inverse in the functor category. (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)$
	fucinv.i	$⊢ I = Inv (Q)$
	fucinv.j	$⊢ J = Inv (D)$
	invfuc.u	$⊢ φ \to U \in (F N G)$
	invfuc.v	$⊢ (φ \land x \in B) \to U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) X$
Assertion	invfuc	$⊢ φ \to U (F I G) (x \in B ⟼ 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		fucinv.i	$⊢ I = Inv (Q)$
7		fucinv.j	$⊢ J = Inv (D)$
8		invfuc.u	$⊢ φ \to U \in (F N G)$
9		invfuc.v	$⊢ (φ \land x \in B) \to U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) X$
10		eqid	$⊢ {Base}_{D} = {Base}_{D}$
11		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
12	4 11	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
13	12	simprd	$⊢ φ \to D \in Cat$
14	13	adantr	$⊢ (φ \land x \in B) \to D \in Cat$
15		relfunc	$⊢ Rel (C Func D)$
16		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
17	15 4 16	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
18	2 10 17	funcf1	$⊢ φ \to 1^{st} (F) : B ⟶ {Base}_{D}$
19	18	ffvelrnda	$⊢ (φ \land x \in B) \to 1^{st} (F) (x) \in {Base}_{D}$
20		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
21	15 5 20	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
22	2 10 21	funcf1	$⊢ φ \to 1^{st} (G) : B ⟶ {Base}_{D}$
23	22	ffvelrnda	$⊢ (φ \land x \in B) \to 1^{st} (G) (x) \in {Base}_{D}$
24		eqid	$⊢ Hom (D) = Hom (D)$
25	10 7 14 19 23 24	invss	$⊢ (φ \land x \in B) \to 1^{st} (F) (x) J 1^{st} (G) (x) \subseteq (1^{st} (F) (x) Hom (D) 1^{st} (G) (x)) \times (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))$
26	25	ssbrd	$⊢ (φ \land x \in B) \to (U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) X \to U (x) ((1^{st} (F) (x) Hom (D) 1^{st} (G) (x)) \times (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))) X)$
27	9 26	mpd	$⊢ (φ \land x \in B) \to U (x) ((1^{st} (F) (x) Hom (D) 1^{st} (G) (x)) \times (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))) X$
28		brxp	$⊢ U (x) ((1^{st} (F) (x) Hom (D) 1^{st} (G) (x)) \times (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))) X \leftrightarrow (U (x) \in (1^{st} (F) (x) Hom (D) 1^{st} (G) (x)) \land X \in (1^{st} (G) (x) Hom (D) 1^{st} (F) (x)))$
29	28	simprbi	$⊢ U (x) ((1^{st} (F) (x) Hom (D) 1^{st} (G) (x)) \times (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))) X \to X \in (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))$
30	27 29	syl	$⊢ (φ \land x \in B) \to X \in (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))$
31	30	ralrimiva	$⊢ φ \to \forall x \in B X \in (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))$
32	2	fvexi	$⊢ B \in V$
33		mptelixpg	$⊢ B \in V \to ((x \in B ⟼ X) \in \underset{x \in B}{⨉} (1^{st} (G) (x) Hom (D) 1^{st} (F) (x)) \leftrightarrow \forall x \in B X \in (1^{st} (G) (x) Hom (D) 1^{st} (F) (x)))$
34	32 33	ax-mp	$⊢ (x \in B ⟼ X) \in \underset{x \in B}{⨉} (1^{st} (G) (x) Hom (D) 1^{st} (F) (x)) \leftrightarrow \forall x \in B X \in (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))$
35	31 34	sylibr	$⊢ φ \to (x \in B ⟼ X) \in \underset{x \in B}{⨉} (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))$
36		fveq2	$⊢ x = y \to 1^{st} (G) (x) = 1^{st} (G) (y)$
37		fveq2	$⊢ x = y \to 1^{st} (F) (x) = 1^{st} (F) (y)$
38	36 37	oveq12d	$⊢ x = y \to 1^{st} (G) (x) Hom (D) 1^{st} (F) (x) = 1^{st} (G) (y) Hom (D) 1^{st} (F) (y)$
39	38	cbvixpv	$⊢ \underset{x \in B}{⨉} (1^{st} (G) (x) Hom (D) 1^{st} (F) (x)) = \underset{y \in B}{⨉} (1^{st} (G) (y) Hom (D) 1^{st} (F) (y))$
40	35 39	eleqtrdi	$⊢ φ \to (x \in B ⟼ X) \in \underset{y \in B}{⨉} (1^{st} (G) (y) Hom (D) 1^{st} (F) (y))$
41		simpr2	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to z \in B$
42		simpr	$⊢ (φ \land x \in B) \to x \in B$
43		eqid	$⊢ (x \in B ⟼ X) = (x \in B ⟼ X)$
44	43	fvmpt2	$⊢ (x \in B \land X \in (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))) \to (x \in B ⟼ X) (x) = X$
45	42 30 44	syl2anc	$⊢ (φ \land x \in B) \to (x \in B ⟼ X) (x) = X$
46	9 45	breqtrrd	$⊢ (φ \land x \in B) \to U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) (x \in B ⟼ X) (x)$
47	46	ralrimiva	$⊢ φ \to \forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) (x \in B ⟼ X) (x)$
48	47	adantr	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to \forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) (x \in B ⟼ X) (x)$
49		nfcv	$⊢ \underline{Ⅎ} x U (z)$
50		nfcv	$⊢ \underline{Ⅎ} x (1^{st} (F) (z) J 1^{st} (G) (z))$
51		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in B ⟼ X) (z)$
52	49 50 51	nfbr	$⊢ Ⅎ x U (z) (1^{st} (F) (z) J 1^{st} (G) (z)) (x \in B ⟼ X) (z)$
53		fveq2	$⊢ x = z \to U (x) = U (z)$
54		fveq2	$⊢ x = z \to 1^{st} (F) (x) = 1^{st} (F) (z)$
55		fveq2	$⊢ x = z \to 1^{st} (G) (x) = 1^{st} (G) (z)$
56	54 55	oveq12d	$⊢ x = z \to 1^{st} (F) (x) J 1^{st} (G) (x) = 1^{st} (F) (z) J 1^{st} (G) (z)$
57		fveq2	$⊢ x = z \to (x \in B ⟼ X) (x) = (x \in B ⟼ X) (z)$
58	53 56 57	breq123d	$⊢ x = z \to (U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) (x \in B ⟼ X) (x) \leftrightarrow U (z) (1^{st} (F) (z) J 1^{st} (G) (z)) (x \in B ⟼ X) (z))$
59	52 58	rspc	$⊢ z \in B \to (\forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) (x \in B ⟼ X) (x) \to U (z) (1^{st} (F) (z) J 1^{st} (G) (z)) (x \in B ⟼ X) (z))$
60	41 48 59	sylc	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to U (z) (1^{st} (F) (z) J 1^{st} (G) (z)) (x \in B ⟼ X) (z)$
61	13	adantr	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to D \in Cat$
62	18	adantr	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to 1^{st} (F) : B ⟶ {Base}_{D}$
63	62 41	ffvelrnd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to 1^{st} (F) (z) \in {Base}_{D}$
64	22	adantr	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to 1^{st} (G) : B ⟶ {Base}_{D}$
65	64 41	ffvelrnd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to 1^{st} (G) (z) \in {Base}_{D}$
66		eqid	$⊢ Sect (D) = Sect (D)$
67	10 7 61 63 65 66	isinv	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (U (z) (1^{st} (F) (z) J 1^{st} (G) (z)) (x \in B ⟼ X) (z) \leftrightarrow (U (z) (1^{st} (F) (z) Sect (D) 1^{st} (G) (z)) (x \in B ⟼ X) (z) \land (x \in B ⟼ X) (z) (1^{st} (G) (z) Sect (D) 1^{st} (F) (z)) U (z)))$
68	60 67	mpbid	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (U (z) (1^{st} (F) (z) Sect (D) 1^{st} (G) (z)) (x \in B ⟼ X) (z) \land (x \in B ⟼ X) (z) (1^{st} (G) (z) Sect (D) 1^{st} (F) (z)) U (z))$
69	68	simpld	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to U (z) (1^{st} (F) (z) Sect (D) 1^{st} (G) (z)) (x \in B ⟼ X) (z)$
70		eqid	$⊢ comp (D) = comp (D)$
71		eqid	$⊢ Id (D) = Id (D)$
72	10 24 70 71 66 61 63 65	issect	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (U (z) (1^{st} (F) (z) Sect (D) 1^{st} (G) (z)) (x \in B ⟼ X) (z) \leftrightarrow (U (z) \in (1^{st} (F) (z) Hom (D) 1^{st} (G) (z)) \land (x \in B ⟼ X) (z) \in (1^{st} (G) (z) Hom (D) 1^{st} (F) (z)) \land (x \in B ⟼ X) (z) (⟨1^{st} (F) (z), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) U (z) = Id (D) (1^{st} (F) (z))))$
73	69 72	mpbid	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (U (z) \in (1^{st} (F) (z) Hom (D) 1^{st} (G) (z)) \land (x \in B ⟼ X) (z) \in (1^{st} (G) (z) Hom (D) 1^{st} (F) (z)) \land (x \in B ⟼ X) (z) (⟨1^{st} (F) (z), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) U (z) = Id (D) (1^{st} (F) (z)))$
74	73	simp3d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (x \in B ⟼ X) (z) (⟨1^{st} (F) (z), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) U (z) = Id (D) (1^{st} (F) (z))$
75	74	oveq1d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to ((x \in B ⟼ X) (z) (⟨1^{st} (F) (z), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) U (z)) (⟨1^{st} (F) (y), 1^{st} (F) (z)⟩ comp (D) 1^{st} (F) (z)) (y 2^{nd} (F) z) (f) = Id (D) (1^{st} (F) (z)) (⟨1^{st} (F) (y), 1^{st} (F) (z)⟩ comp (D) 1^{st} (F) (z)) (y 2^{nd} (F) z) (f)$
76		simpr1	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to y \in B$
77	62 76	ffvelrnd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to 1^{st} (F) (y) \in {Base}_{D}$
78		eqid	$⊢ Hom (C) = Hom (C)$
79	17	adantr	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
80	2 78 24 79 76 41	funcf2	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (y 2^{nd} (F) z) : y Hom (C) z ⟶ 1^{st} (F) (y) Hom (D) 1^{st} (F) (z)$
81		simpr3	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to f \in (y Hom (C) z)$
82	80 81	ffvelrnd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (y 2^{nd} (F) z) (f) \in (1^{st} (F) (y) Hom (D) 1^{st} (F) (z))$
83	10 24 71 61 77 70 63 82	catlid	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to Id (D) (1^{st} (F) (z)) (⟨1^{st} (F) (y), 1^{st} (F) (z)⟩ comp (D) 1^{st} (F) (z)) (y 2^{nd} (F) z) (f) = (y 2^{nd} (F) z) (f)$
84	75 83	eqtr2d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (y 2^{nd} (F) z) (f) = ((x \in B ⟼ X) (z) (⟨1^{st} (F) (z), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) U (z)) (⟨1^{st} (F) (y), 1^{st} (F) (z)⟩ comp (D) 1^{st} (F) (z)) (y 2^{nd} (F) z) (f)$
85	8	adantr	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to U \in (F N G)$
86	3 85	nat1st2nd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to U \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
87	3 86 2 24 41	natcl	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to U (z) \in (1^{st} (F) (z) Hom (D) 1^{st} (G) (z))$
88	73	simp2d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (x \in B ⟼ X) (z) \in (1^{st} (G) (z) Hom (D) 1^{st} (F) (z))$
89	10 24 70 61 77 63 65 82 87 63 88	catass	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to ((x \in B ⟼ X) (z) (⟨1^{st} (F) (z), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) U (z)) (⟨1^{st} (F) (y), 1^{st} (F) (z)⟩ comp (D) 1^{st} (F) (z)) (y 2^{nd} (F) z) (f) = (x \in B ⟼ X) (z) (⟨1^{st} (F) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) (U (z) (⟨1^{st} (F) (y), 1^{st} (F) (z)⟩ comp (D) 1^{st} (G) (z)) (y 2^{nd} (F) z) (f))$
90	3 86 2 78 70 76 41 81	nati	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to U (z) (⟨1^{st} (F) (y), 1^{st} (F) (z)⟩ comp (D) 1^{st} (G) (z)) (y 2^{nd} (F) z) (f) = (y 2^{nd} (G) z) (f) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) U (y)$
91	90	oveq2d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (x \in B ⟼ X) (z) (⟨1^{st} (F) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) (U (z) (⟨1^{st} (F) (y), 1^{st} (F) (z)⟩ comp (D) 1^{st} (G) (z)) (y 2^{nd} (F) z) (f)) = (x \in B ⟼ X) (z) (⟨1^{st} (F) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) ((y 2^{nd} (G) z) (f) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) U (y))$
92	84 89 91	3eqtrd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (y 2^{nd} (F) z) (f) = (x \in B ⟼ X) (z) (⟨1^{st} (F) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) ((y 2^{nd} (G) z) (f) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) U (y))$
93	92	oveq1d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (y 2^{nd} (F) z) (f) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x \in B ⟼ X) (y) = ((x \in B ⟼ X) (z) (⟨1^{st} (F) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) ((y 2^{nd} (G) z) (f) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) U (y))) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x \in B ⟼ X) (y)$
94	64 76	ffvelrnd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to 1^{st} (G) (y) \in {Base}_{D}$
95		nfcv	$⊢ \underline{Ⅎ} x U (y)$
96		nfcv	$⊢ \underline{Ⅎ} x (1^{st} (F) (y) J 1^{st} (G) (y))$
97		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in B ⟼ X) (y)$
98	95 96 97	nfbr	$⊢ Ⅎ x U (y) (1^{st} (F) (y) J 1^{st} (G) (y)) (x \in B ⟼ X) (y)$
99		fveq2	$⊢ x = y \to U (x) = U (y)$
100	37 36	oveq12d	$⊢ x = y \to 1^{st} (F) (x) J 1^{st} (G) (x) = 1^{st} (F) (y) J 1^{st} (G) (y)$
101		fveq2	$⊢ x = y \to (x \in B ⟼ X) (x) = (x \in B ⟼ X) (y)$
102	99 100 101	breq123d	$⊢ x = y \to (U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) (x \in B ⟼ X) (x) \leftrightarrow U (y) (1^{st} (F) (y) J 1^{st} (G) (y)) (x \in B ⟼ X) (y))$
103	98 102	rspc	$⊢ y \in B \to (\forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) (x \in B ⟼ X) (x) \to U (y) (1^{st} (F) (y) J 1^{st} (G) (y)) (x \in B ⟼ X) (y))$
104	76 48 103	sylc	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to U (y) (1^{st} (F) (y) J 1^{st} (G) (y)) (x \in B ⟼ X) (y)$
105	10 7 61 77 94 66	isinv	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (U (y) (1^{st} (F) (y) J 1^{st} (G) (y)) (x \in B ⟼ X) (y) \leftrightarrow (U (y) (1^{st} (F) (y) Sect (D) 1^{st} (G) (y)) (x \in B ⟼ X) (y) \land (x \in B ⟼ X) (y) (1^{st} (G) (y) Sect (D) 1^{st} (F) (y)) U (y)))$
106	104 105	mpbid	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (U (y) (1^{st} (F) (y) Sect (D) 1^{st} (G) (y)) (x \in B ⟼ X) (y) \land (x \in B ⟼ X) (y) (1^{st} (G) (y) Sect (D) 1^{st} (F) (y)) U (y))$
107	106	simprd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (x \in B ⟼ X) (y) (1^{st} (G) (y) Sect (D) 1^{st} (F) (y)) U (y)$
108	10 24 70 71 66 61 94 77	issect	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to ((x \in B ⟼ X) (y) (1^{st} (G) (y) Sect (D) 1^{st} (F) (y)) U (y) \leftrightarrow ((x \in B ⟼ X) (y) \in (1^{st} (G) (y) Hom (D) 1^{st} (F) (y)) \land U (y) \in (1^{st} (F) (y) Hom (D) 1^{st} (G) (y)) \land U (y) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (y)) (x \in B ⟼ X) (y) = Id (D) (1^{st} (G) (y))))$
109	107 108	mpbid	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to ((x \in B ⟼ X) (y) \in (1^{st} (G) (y) Hom (D) 1^{st} (F) (y)) \land U (y) \in (1^{st} (F) (y) Hom (D) 1^{st} (G) (y)) \land U (y) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (y)) (x \in B ⟼ X) (y) = Id (D) (1^{st} (G) (y)))$
110	109	simp1d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (x \in B ⟼ X) (y) \in (1^{st} (G) (y) Hom (D) 1^{st} (F) (y))$
111	109	simp2d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to U (y) \in (1^{st} (F) (y) Hom (D) 1^{st} (G) (y))$
112	21	adantr	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
113	2 78 24 112 76 41	funcf2	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (y 2^{nd} (G) z) : y Hom (C) z ⟶ 1^{st} (G) (y) Hom (D) 1^{st} (G) (z)$
114	113 81	ffvelrnd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (y 2^{nd} (G) z) (f) \in (1^{st} (G) (y) Hom (D) 1^{st} (G) (z))$
115	10 24 70 61 77 94 65 111 114	catcocl	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (y 2^{nd} (G) z) (f) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) U (y) \in (1^{st} (F) (y) Hom (D) 1^{st} (G) (z))$
116	10 24 70 61 94 77 65 110 115 63 88	catass	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to ((x \in B ⟼ X) (z) (⟨1^{st} (F) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) ((y 2^{nd} (G) z) (f) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) U (y))) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x \in B ⟼ X) (y) = (x \in B ⟼ X) (z) (⟨1^{st} (G) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) (((y 2^{nd} (G) z) (f) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) U (y)) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (z)) (x \in B ⟼ X) (y))$
117	3 86 2 24 76	natcl	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to U (y) \in (1^{st} (F) (y) Hom (D) 1^{st} (G) (y))$
118	10 24 70 61 94 77 94 110 117 65 114	catass	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to ((y 2^{nd} (G) z) (f) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) U (y)) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (z)) (x \in B ⟼ X) (y) = (y 2^{nd} (G) z) (f) (⟨1^{st} (G) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) (U (y) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (y)) (x \in B ⟼ X) (y))$
119	109	simp3d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to U (y) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (y)) (x \in B ⟼ X) (y) = Id (D) (1^{st} (G) (y))$
120	119	oveq2d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (y 2^{nd} (G) z) (f) (⟨1^{st} (G) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) (U (y) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (y)) (x \in B ⟼ X) (y)) = (y 2^{nd} (G) z) (f) (⟨1^{st} (G) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) Id (D) (1^{st} (G) (y))$
121	10 24 71 61 94 70 65 114	catrid	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (y 2^{nd} (G) z) (f) (⟨1^{st} (G) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) Id (D) (1^{st} (G) (y)) = (y 2^{nd} (G) z) (f)$
122	118 120 121	3eqtrd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to ((y 2^{nd} (G) z) (f) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) U (y)) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (z)) (x \in B ⟼ X) (y) = (y 2^{nd} (G) z) (f)$
123	122	oveq2d	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (x \in B ⟼ X) (z) (⟨1^{st} (G) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) (((y 2^{nd} (G) z) (f) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (G) (z)) U (y)) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (z)) (x \in B ⟼ X) (y)) = (x \in B ⟼ X) (z) (⟨1^{st} (G) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) (y 2^{nd} (G) z) (f)$
124	93 116 123	3eqtrrd	$⊢ (φ \land (y \in B \land z \in B \land f \in (y Hom (C) z))) \to (x \in B ⟼ X) (z) (⟨1^{st} (G) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) (y 2^{nd} (G) z) (f) = (y 2^{nd} (F) z) (f) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x \in B ⟼ X) (y)$
125	124	ralrimivvva	$⊢ φ \to \forall y \in B \forall z \in B \forall f \in (y Hom (C) z) (x \in B ⟼ X) (z) (⟨1^{st} (G) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) (y 2^{nd} (G) z) (f) = (y 2^{nd} (F) z) (f) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x \in B ⟼ X) (y)$
126	3 2 78 24 70 5 4	isnat2	$⊢ φ \to ((x \in B ⟼ X) \in (G N F) \leftrightarrow ((x \in B ⟼ X) \in \underset{y \in B}{⨉} (1^{st} (G) (y) Hom (D) 1^{st} (F) (y)) \land \forall y \in B \forall z \in B \forall f \in (y Hom (C) z) (x \in B ⟼ X) (z) (⟨1^{st} (G) (y), 1^{st} (G) (z)⟩ comp (D) 1^{st} (F) (z)) (y 2^{nd} (G) z) (f) = (y 2^{nd} (F) z) (f) (⟨1^{st} (G) (y), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x \in B ⟼ X) (y)))$
127	40 125 126	mpbir2and	$⊢ φ \to (x \in B ⟼ X) \in (G N F)$
128		nfv	$⊢ Ⅎ y U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) (x \in B ⟼ X) (x)$
129	128 98 102	cbvralw	$⊢ \forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) (x \in B ⟼ X) (x) \leftrightarrow \forall y \in B U (y) (1^{st} (F) (y) J 1^{st} (G) (y)) (x \in B ⟼ X) (y)$
130	47 129	sylib	$⊢ φ \to \forall y \in B U (y) (1^{st} (F) (y) J 1^{st} (G) (y)) (x \in B ⟼ X) (y)$
131	1 2 3 4 5 6 7	fucinv	$⊢ φ \to (U (F I G) (x \in B ⟼ X) \leftrightarrow (U \in (F N G) \land (x \in B ⟼ X) \in (G N F) \land \forall y \in B U (y) (1^{st} (F) (y) J 1^{st} (G) (y)) (x \in B ⟼ X) (y)))$
132	8 127 130 131	mpbir3and	$⊢ φ \to U (F I G) (x \in B ⟼ X)$

Metamath Proof Explorer

Theorem invfuc

Proof