fucinv

Description: Two natural transformations are inverses of each other iff all the components are inverse. (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)$
Assertion	fucinv	$⊢ φ \to (U (F I G) V \leftrightarrow (U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) V (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		eqid	$⊢ Sect (Q) = Sect (Q)$
9		eqid	$⊢ Sect (D) = Sect (D)$
10	1 2 3 4 5 8 9	fucsect	$⊢ φ \to (U (F Sect (Q) G) V \leftrightarrow (U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x)))$
11	1 2 3 5 4 8 9	fucsect	$⊢ φ \to (V (G Sect (Q) F) U \leftrightarrow (V \in (G N F) \land U \in (F N G) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)))$
12	10 11	anbi12d	$⊢ φ \to ((U (F Sect (Q) G) V \land V (G Sect (Q) F) U) \leftrightarrow ((U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x)) \land (V \in (G N F) \land U \in (F N G) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x))))$
13	1	fucbas	$⊢ C Func D = {Base}_{Q}$
14		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
15	4 14	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
16	15	simpld	$⊢ φ \to C \in Cat$
17	15	simprd	$⊢ φ \to D \in Cat$
18	1 16 17	fuccat	$⊢ φ \to Q \in Cat$
19	13 6 18 4 5 8	isinv	$⊢ φ \to (U (F I G) V \leftrightarrow (U (F Sect (Q) G) V \land V (G Sect (Q) F) U))$
20		eqid	$⊢ {Base}_{D} = {Base}_{D}$
21	17	adantr	$⊢ (φ \land x \in B) \to D \in Cat$
22		relfunc	$⊢ Rel (C Func D)$
23		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
24	22 4 23	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
25	2 20 24	funcf1	$⊢ φ \to 1^{st} (F) : B ⟶ {Base}_{D}$
26	25	ffvelcdmda	$⊢ (φ \land x \in B) \to 1^{st} (F) (x) \in {Base}_{D}$
27		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
28	22 5 27	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
29	2 20 28	funcf1	$⊢ φ \to 1^{st} (G) : B ⟶ {Base}_{D}$
30	29	ffvelcdmda	$⊢ (φ \land x \in B) \to 1^{st} (G) (x) \in {Base}_{D}$
31	20 7 21 26 30 9	isinv	$⊢ (φ \land x \in B) \to (U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) V (x) \leftrightarrow (U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x) \land V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)))$
32	31	ralbidva	$⊢ φ \to (\forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) V (x) \leftrightarrow \forall x \in B (U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x) \land V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)))$
33		r19.26	$⊢ \forall x \in B (U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x) \land V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)) \leftrightarrow (\forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x))$
34	32 33	bitrdi	$⊢ φ \to (\forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) V (x) \leftrightarrow (\forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)))$
35	34	anbi2d	$⊢ φ \to (((U \in (F N G) \land V \in (G N F)) \land \forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) V (x)) \leftrightarrow ((U \in (F N G) \land V \in (G N F)) \land (\forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x))))$
36		df-3an	$⊢ (U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) V (x)) \leftrightarrow ((U \in (F N G) \land V \in (G N F)) \land \forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) V (x))$
37		df-3an	$⊢ (U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x)) \leftrightarrow ((U \in (F N G) \land V \in (G N F)) \land \forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x))$
38		3ancoma	$⊢ (V \in (G N F) \land U \in (F N G) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)) \leftrightarrow (U \in (F N G) \land V \in (G N F) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x))$
39		df-3an	$⊢ (U \in (F N G) \land V \in (G N F) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)) \leftrightarrow ((U \in (F N G) \land V \in (G N F)) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x))$
40	38 39	bitri	$⊢ (V \in (G N F) \land U \in (F N G) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)) \leftrightarrow ((U \in (F N G) \land V \in (G N F)) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x))$
41	37 40	anbi12i	$⊢ ((U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x)) \land (V \in (G N F) \land U \in (F N G) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x))) \leftrightarrow (((U \in (F N G) \land V \in (G N F)) \land \forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x)) \land ((U \in (F N G) \land V \in (G N F)) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)))$
42		anandi	$⊢ ((U \in (F N G) \land V \in (G N F)) \land (\forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x))) \leftrightarrow (((U \in (F N G) \land V \in (G N F)) \land \forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x)) \land ((U \in (F N G) \land V \in (G N F)) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)))$
43	41 42	bitr4i	$⊢ ((U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x)) \land (V \in (G N F) \land U \in (F N G) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x))) \leftrightarrow ((U \in (F N G) \land V \in (G N F)) \land (\forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x)))$
44	35 36 43	3bitr4g	$⊢ φ \to ((U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) V (x)) \leftrightarrow ((U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) Sect (D) 1^{st} (G) (x)) V (x)) \land (V \in (G N F) \land U \in (F N G) \land \forall x \in B V (x) (1^{st} (G) (x) Sect (D) 1^{st} (F) (x)) U (x))))$
45	12 19 44	3bitr4d	$⊢ φ \to (U (F I G) V \leftrightarrow (U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) J 1^{st} (G) (x)) V (x)))$

Metamath Proof Explorer

Theorem fucinv

Proof