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	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fuciso.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	fuciso.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fuciso.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	fuciso.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
	fucinv.i	⊢ 𝐼 = ( Inv ‘ 𝑄 )
	fucinv.j	⊢ 𝐽 = ( Inv ‘ 𝐷 )
Assertion	fucinv	⊢ ( 𝜑 → ( 𝑈 ( 𝐹 𝐼 𝐺 ) 𝑉 ↔ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuciso.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fuciso.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		fuciso.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
4		fuciso.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		fuciso.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
6		fucinv.i	⊢ 𝐼 = ( Inv ‘ 𝑄 )
7		fucinv.j	⊢ 𝐽 = ( Inv ‘ 𝐷 )
8		eqid	⊢ ( Sect ‘ 𝑄 ) = ( Sect ‘ 𝑄 )
9		eqid	⊢ ( Sect ‘ 𝐷 ) = ( Sect ‘ 𝐷 )
10	1 2 3 4 5 8 9	fucsect	⊢ ( 𝜑 → ( 𝑈 ( 𝐹 ( Sect ‘ 𝑄 ) 𝐺 ) 𝑉 ↔ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ) )
11	1 2 3 5 4 8 9	fucsect	⊢ ( 𝜑 → ( 𝑉 ( 𝐺 ( Sect ‘ 𝑄 ) 𝐹 ) 𝑈 ↔ ( 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) )
12	10 11	anbi12d	⊢ ( 𝜑 → ( ( 𝑈 ( 𝐹 ( Sect ‘ 𝑄 ) 𝐺 ) 𝑉 ∧ 𝑉 ( 𝐺 ( Sect ‘ 𝑄 ) 𝐹 ) 𝑈 ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ∧ ( 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) ) )
13	1	fucbas	⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
14		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
15	4 14	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
16	15	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
17	15	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
18	1 16 17	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
19	13 6 18 4 5 8	isinv	⊢ ( 𝜑 → ( 𝑈 ( 𝐹 𝐼 𝐺 ) 𝑉 ↔ ( 𝑈 ( 𝐹 ( Sect ‘ 𝑄 ) 𝐺 ) 𝑉 ∧ 𝑉 ( 𝐺 ( Sect ‘ 𝑄 ) 𝐹 ) 𝑈 ) ) )
20		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
21	17	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ Cat )
22		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
23		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
24	22 4 23	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
25	2 20 24	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
26	25	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
27		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
28	22 5 27	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
29	2 20 28	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
30	29	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
31	20 7 21 26 30 9	isinv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ↔ ( ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ∧ ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) )
32	31	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ∧ ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) )
33		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ∧ ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) )
34	32 33	bitrdi	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ↔ ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) )
35	34	anbi2d	⊢ ( 𝜑 → ( ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) ) )
36		df-3an	⊢ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) )
37		df-3an	⊢ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) )
38		3ancoma	⊢ ( ( 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ↔ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) )
39		df-3an	⊢ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) )
40	38 39	bitri	⊢ ( ( 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) )
41	37 40	anbi12i	⊢ ( ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ∧ ( 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) ↔ ( ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ∧ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) )
42		anandi	⊢ ( ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) ↔ ( ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ∧ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) )
43	41 42	bitr4i	⊢ ( ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ∧ ( 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) )
44	35 36 43	3bitr4g	⊢ ( 𝜑 → ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ∧ ( 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑉 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) ) )
45	12 19 44	3bitr4d	⊢ ( 𝜑 → ( 𝑈 ( 𝐹 𝐼 𝐺 ) 𝑉 ↔ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem fucinv

Proof