fucsect

Description: Two natural transformations are in a section iff all the components are in a section relation. (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 𝐷 ) )
	fucsect.s	⊢ 𝑆 = ( Sect ‘ 𝑄 )
	fucsect.t	⊢ 𝑇 = ( Sect ‘ 𝐷 )
Assertion	fucsect	⊢ ( 𝜑 → ( 𝑈 ( 𝐹 𝑆 𝐺 ) 𝑉 ↔ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 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		fucsect.s	⊢ 𝑆 = ( Sect ‘ 𝑄 )
7		fucsect.t	⊢ 𝑇 = ( Sect ‘ 𝐷 )
8	1	fucbas	⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
9	1 3	fuchom	⊢ 𝑁 = ( Hom ‘ 𝑄 )
10		eqid	⊢ ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 )
11		eqid	⊢ ( Id ‘ 𝑄 ) = ( Id ‘ 𝑄 )
12		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
13	4 12	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
14	13	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
15	13	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
16	1 14 15	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
17	8 9 10 11 6 16 4 5	issect	⊢ ( 𝜑 → ( 𝑈 ( 𝐹 𝑆 𝐺 ) 𝑉 ↔ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ( 𝑉 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐹 ) 𝑈 ) = ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) ) )
18		ovex	⊢ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ∈ V
19	18	rgenw	⊢ ∀ 𝑥 ∈ 𝐵 ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ∈ V
20		mpteqb	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ∈ V → ( ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
21	19 20	mp1i	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
22		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
23		simprl	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) )
24		simprr	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) )
25	1 3 2 22 10 23 24	fucco	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( 𝑉 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐹 ) 𝑈 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) )
26		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
27	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
28	1 11 26 27	fucid	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) = ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) )
29	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → 𝐷 ∈ Cat )
30		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
31	30 26	cidfn	⊢ ( 𝐷 ∈ Cat → ( Id ‘ 𝐷 ) Fn ( Base ‘ 𝐷 ) )
32	29 31	syl	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( Id ‘ 𝐷 ) Fn ( Base ‘ 𝐷 ) )
33		dffn2	⊢ ( ( Id ‘ 𝐷 ) Fn ( Base ‘ 𝐷 ) ↔ ( Id ‘ 𝐷 ) : ( Base ‘ 𝐷 ) ⟶ V )
34	32 33	sylib	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( Id ‘ 𝐷 ) : ( Base ‘ 𝐷 ) ⟶ V )
35		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
36		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
37	35 4 36	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
38	2 30 37	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
40		fcompt	⊢ ( ( ( Id ‘ 𝐷 ) : ( Base ‘ 𝐷 ) ⟶ V ∧ ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) ) → ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
41	34 39 40	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
42	28 41	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
43	25 42	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( ( 𝑉 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐹 ) 𝑈 ) = ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ↔ ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) )
44		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
45	29	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ Cat )
46	39	ffvelrnda	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
47		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
48	35 5 47	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
49	2 30 48	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
50	49	adantr	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( 1^st ‘ 𝐺 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
51	50	ffvelrnda	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
52	23	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) )
53	3 52	nat1st2nd	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑈 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
54		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
55	3 53 2 44 54	natcl	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
56	24	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) )
57	3 56	nat1st2nd	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑉 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
58	3 57 2 44 54	natcl	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑉 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
59	30 44 22 26 7 45 46 51 55 58	issect2	⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝑇 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ↔ ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
60	59	ralbidva	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝑇 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑉 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 𝑈 ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
61	21 43 60	3bitr4d	⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ) → ( ( 𝑉 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐹 ) 𝑈 ) = ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝑇 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) )
62	61	pm5.32da	⊢ ( 𝜑 → ( ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ( 𝑉 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐹 ) 𝑈 ) = ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝑇 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ) )
63		df-3an	⊢ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ( 𝑉 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐹 ) 𝑈 ) = ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ( 𝑉 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐹 ) 𝑈 ) = ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) )
64		df-3an	⊢ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝑇 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ↔ ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝑇 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) )
65	62 63 64	3bitr4g	⊢ ( 𝜑 → ( ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ( 𝑉 ( ⟨ 𝐹 , 𝐺 ⟩ ( comp ‘ 𝑄 ) 𝐹 ) 𝑈 ) = ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) ↔ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝑇 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ) )
66	17 65	bitrd	⊢ ( 𝜑 → ( 𝑈 ( 𝐹 𝑆 𝐺 ) 𝑉 ↔ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ 𝑉 ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝑇 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝑉 ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem fucsect

Proof