Metamath Proof Explorer

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 snex ⊢ { 𝑓 } ∈ 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 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )