Theorem isfunc

Description: Value of the set of functors between two categories. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	isfunc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	isfunc.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
	isfunc.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	isfunc.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
	isfunc.1	⊢ 1 = ( Id ‘ 𝐷 )
	isfunc.i	⊢ 𝐼 = ( Id ‘ 𝐸 )
	isfunc.x	⊢ · = ( comp ‘ 𝐷 )
	isfunc.o	⊢ 𝑂 = ( comp ‘ 𝐸 )
	isfunc.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	isfunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
Assertion	isfunc	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfunc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		isfunc.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
3		isfunc.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
4		isfunc.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
5		isfunc.1	⊢ 1 = ( Id ‘ 𝐷 )
6		isfunc.i	⊢ 𝐼 = ( Id ‘ 𝐸 )
7		isfunc.x	⊢ · = ( comp ‘ 𝐷 )
8		isfunc.o	⊢ 𝑂 = ( comp ‘ 𝐸 )
9		isfunc.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
10		isfunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
11		fvexd	⊢ ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) → ( Base ‘ 𝑑 ) ∈ V )
12		simpl	⊢ ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) → 𝑑 = 𝐷 )
13	12	fveq2d	⊢ ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) → ( Base ‘ 𝑑 ) = ( Base ‘ 𝐷 ) )
14	13 1	eqtr4di	⊢ ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) → ( Base ‘ 𝑑 ) = 𝐵 )
15		simpr	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
16		simplr	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → 𝑒 = 𝐸 )
17	16	fveq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Base ‘ 𝑒 ) = ( Base ‘ 𝐸 ) )
18	17 2	eqtr4di	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Base ‘ 𝑒 ) = 𝐶 )
19	15 18	feq23d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑒 ) ↔ 𝑓 : 𝐵 ⟶ 𝐶 ) )
20	2	fvexi	⊢ 𝐶 ∈ V
21	1	fvexi	⊢ 𝐵 ∈ V
22	20 21	elmap	⊢ ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ↔ 𝑓 : 𝐵 ⟶ 𝐶 )
23	19 22	bitr4di	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑒 ) ↔ 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ) )
24	15	sqxpeqd	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑏 × 𝑏 ) = ( 𝐵 × 𝐵 ) )
25	24	ixpeq1d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) = X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) )
26	16	fveq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑒 ) = ( Hom ‘ 𝐸 ) )
27	26 4	eqtr4di	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑒 ) = 𝐽 )
28	27	oveqd	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) = ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) )
29		simpll	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → 𝑑 = 𝐷 )
30	29	fveq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑑 ) = ( Hom ‘ 𝐷 ) )
31	30 3	eqtr4di	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑑 ) = 𝐻 )
32	31	fveq1d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) = ( 𝐻 ‘ 𝑧 ) )
33	28 32	oveq12d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) = ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) )
34	33	ixpeq2dv	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) = X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) )
35	25 34	eqtrd	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) = X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) )
36	35	eleq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) ↔ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) )
37	29	fveq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Id ‘ 𝑑 ) = ( Id ‘ 𝐷 ) )
38	37 5	eqtr4di	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Id ‘ 𝑑 ) = 1 )
39	38	fveq1d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( Id ‘ 𝑑 ) ‘ 𝑥 ) = ( 1 ‘ 𝑥 ) )
40	39	fveq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑑 ) ‘ 𝑥 ) ) = ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) )
41	16	fveq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Id ‘ 𝑒 ) = ( Id ‘ 𝐸 ) )
42	41 6	eqtr4di	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( Id ‘ 𝑒 ) = 𝐼 )
43	42	fveq1d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( Id ‘ 𝑒 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) )
44	40 43	eqeq12d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑑 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑒 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
45	31	oveqd	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
46	31	oveqd	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) = ( 𝑦 𝐻 𝑧 ) )
47	29	fveq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( comp ‘ 𝑑 ) = ( comp ‘ 𝐷 ) )
48	47 7	eqtr4di	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( comp ‘ 𝑑 ) = · )
49	48	oveqd	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) )
50	49	oveqd	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) = ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) )
51	50	fveq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) )
52	16	fveq2d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( comp ‘ 𝑒 ) = ( comp ‘ 𝐸 ) )
53	52 8	eqtr4di	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( comp ‘ 𝑒 ) = 𝑂 )
54	53	oveqd	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) = ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) )
55	54	oveqd	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) )
56	51 55	eqeq12d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
57	46 56	raleqbidv	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
58	45 57	raleqbidv	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
59	15 58	raleqbidv	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
60	15 59	raleqbidv	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
61	44 60	anbi12d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑑 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑒 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ↔ ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) )
62	15 61	raleqbidv	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑑 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑒 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) )
63	23 36 62	3anbi123d	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑒 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑑 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑒 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
64		df-3an	⊢ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) )
65	63 64	bitrdi	⊢ ( ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑒 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑑 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑒 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
66	11 14 65	sbcied2	⊢ ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) → ( [ ( Base ‘ 𝑑 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑒 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑑 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑒 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
67	66	opabbidv	⊢ ( ( 𝑑 = 𝐷 ∧ 𝑒 = 𝐸 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Base ‘ 𝑑 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑒 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑑 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑒 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )
68		df-func	⊢ Func = ( 𝑑 ∈ Cat , 𝑒 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Base ‘ 𝑑 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑒 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑒 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑑 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑑 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑒 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑑 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑑 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑒 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )
69		ovex	⊢ ( 𝐶 ↑m 𝐵 ) ∈ V
70		vsnex	⊢ { 𝑓 } ∈ V
71		ovex	⊢ ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∈ V
72	71	rgenw	⊢ ∀ 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∈ V
73		ixpexg	⊢ ( ∀ 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∈ V → X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∈ V )
74	72 73	ax-mp	⊢ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∈ V
75	70 74	xpex	⊢ ( { 𝑓 } × X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∈ V
76	69 75	iunex	⊢ ∪ 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ( { 𝑓 } × X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∈ V
77		simpl	⊢ ( ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) → ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) )
78	77	anim2i	⊢ ( ( 𝑑 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) → ( 𝑑 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ) )
79	78	2eximi	⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑑 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑑 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ) )
80		elopab	⊢ ( 𝑑 ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } ↔ ∃ 𝑓 ∃ 𝑔 ( 𝑑 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
81		eliunxp	⊢ ( 𝑑 ∈ ∪ 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ( { 𝑓 } × X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ↔ ∃ 𝑓 ∃ 𝑔 ( 𝑑 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ) )
82	79 80 81	3imtr4i	⊢ ( 𝑑 ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } → 𝑑 ∈ ∪ 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ( { 𝑓 } × X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) )
83	82	ssriv	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } ⊆ ∪ 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ( { 𝑓 } × X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) )
84	76 83	ssexi	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } ∈ V
85	67 68 84	ovmpoa	⊢ ( ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) → ( 𝐷 Func 𝐸 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )
86	9 10 85	syl2anc	⊢ ( 𝜑 → ( 𝐷 Func 𝐸 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )
87	86	breqd	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } 𝐺 ) )
88		brabv	⊢ ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } 𝐺 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
89		elex	⊢ ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) → 𝐹 ∈ V )
90		elex	⊢ ( 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) → 𝐺 ∈ V )
91	89 90	anim12i	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
92	91	3adant3	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
93		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
94	93	eleq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ↔ 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ) )
95		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
96	93	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) )
97	93	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) )
98	96 97	oveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) = ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) )
99	98	oveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) )
100	99	ixpeq2dv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) = X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) )
101	95 100	eleq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ↔ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) )
102	95	oveqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑥 𝑔 𝑥 ) = ( 𝑥 𝐺 𝑥 ) )
103	102	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) )
104	93	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
105	104	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) )
106	103 105	eqeq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
107	95	oveqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑥 𝑔 𝑧 ) = ( 𝑥 𝐺 𝑧 ) )
108	107	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) )
109	93	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
110	104 109	opeq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
111	93	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
112	110 111	oveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) = ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) )
113	95	oveqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑦 𝑔 𝑧 ) = ( 𝑦 𝐺 𝑧 ) )
114	113	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) = ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) )
115	95	oveqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
116	115	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) = ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) )
117	112 114 116	oveq123d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) )
118	108 117	eqeq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) )
119	118	2ralbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) )
120	119	2ralbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) )
121	106 120	anbi12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ↔ ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) )
122	121	ralbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) )
123	94 101 122	3anbi123d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
124	64 123	bitr3id	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
125		eqid	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) }
126	124 125	brabga	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } 𝐺 ↔ ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
127	88 92 126	pm5.21nii	⊢ ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } 𝐺 ↔ ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) )
128	20 21	elmap	⊢ ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ↔ 𝐹 : 𝐵 ⟶ 𝐶 )
129	128	3anbi1i	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) )
130	127 129	bitri	⊢ ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ 𝑂 ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } 𝐺 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) )
131	87 130	bitrdi	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )