Metamath Proof Explorer


Theorem isnat

Description: Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses natfval.1 𝑁 = ( 𝐶 Nat 𝐷 )
natfval.b 𝐵 = ( Base ‘ 𝐶 )
natfval.h 𝐻 = ( Hom ‘ 𝐶 )
natfval.j 𝐽 = ( Hom ‘ 𝐷 )
natfval.o · = ( comp ‘ 𝐷 )
isnat.f ( 𝜑𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
isnat.g ( 𝜑𝐾 ( 𝐶 Func 𝐷 ) 𝐿 )
Assertion isnat ( 𝜑 → ( 𝐴 ∈ ( ⟨ 𝐹 , 𝐺𝑁𝐾 , 𝐿 ⟩ ) ↔ ( 𝐴X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∧ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝐴𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 natfval.1 𝑁 = ( 𝐶 Nat 𝐷 )
2 natfval.b 𝐵 = ( Base ‘ 𝐶 )
3 natfval.h 𝐻 = ( Hom ‘ 𝐶 )
4 natfval.j 𝐽 = ( Hom ‘ 𝐷 )
5 natfval.o · = ( comp ‘ 𝐷 )
6 isnat.f ( 𝜑𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
7 isnat.g ( 𝜑𝐾 ( 𝐶 Func 𝐷 ) 𝐿 )
8 1 2 3 4 5 natfval 𝑁 = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1st𝑓 ) / 𝑟 ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥𝐵 ( ( 𝑟𝑥 ) 𝐽 ( 𝑠𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ · ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ · ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } )
9 8 a1i ( 𝜑𝑁 = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1st𝑓 ) / 𝑟 ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥𝐵 ( ( 𝑟𝑥 ) 𝐽 ( 𝑠𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ · ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ · ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } ) )
10 fvexd ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → ( 1st𝑓 ) ∈ V )
11 simprl ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ )
12 11 fveq2d ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → ( 1st𝑓 ) = ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
13 relfunc Rel ( 𝐶 Func 𝐷 )
14 brrelex12 ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
15 13 6 14 sylancr ( 𝜑 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
16 op1stg ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
17 15 16 syl ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
18 17 adantr ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
19 12 18 eqtrd ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → ( 1st𝑓 ) = 𝐹 )
20 fvexd ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → ( 1st𝑔 ) ∈ V )
21 simplrr ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ )
22 21 fveq2d ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → ( 1st𝑔 ) = ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) )
23 brrelex12 ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐾 ( 𝐶 Func 𝐷 ) 𝐿 ) → ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) )
24 13 7 23 sylancr ( 𝜑 → ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) )
25 op1stg ( ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
26 24 25 syl ( 𝜑 → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
27 26 ad2antrr ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
28 22 27 eqtrd ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → ( 1st𝑔 ) = 𝐾 )
29 simplr ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → 𝑟 = 𝐹 )
30 29 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑟𝑥 ) = ( 𝐹𝑥 ) )
31 simpr ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → 𝑠 = 𝐾 )
32 31 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑠𝑥 ) = ( 𝐾𝑥 ) )
33 30 32 oveq12d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( 𝑟𝑥 ) 𝐽 ( 𝑠𝑥 ) ) = ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) )
34 33 ixpeq2dv ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → X 𝑥𝐵 ( ( 𝑟𝑥 ) 𝐽 ( 𝑠𝑥 ) ) = X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) )
35 29 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑟𝑦 ) = ( 𝐹𝑦 ) )
36 30 35 opeq12d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ = ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ )
37 31 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑠𝑦 ) = ( 𝐾𝑦 ) )
38 36 37 oveq12d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ · ( 𝑠𝑦 ) ) = ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) )
39 eqidd ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑎𝑦 ) = ( 𝑎𝑦 ) )
40 11 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ )
41 40 fveq2d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2nd𝑓 ) = ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
42 op2ndg ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
43 15 42 syl ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
44 43 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
45 41 44 eqtrd ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2nd𝑓 ) = 𝐺 )
46 45 oveqd ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑥 ( 2nd𝑓 ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
47 46 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) = ( ( 𝑥 𝐺 𝑦 ) ‘ ) )
48 38 39 47 oveq123d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ · ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) ) = ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) )
49 30 32 opeq12d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ = ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ )
50 49 37 oveq12d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ · ( 𝑠𝑦 ) ) = ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) )
51 21 adantr ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ )
52 51 fveq2d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2nd𝑔 ) = ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) )
53 op2ndg ( ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) → ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
54 24 53 syl ( 𝜑 → ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
55 54 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
56 52 55 eqtrd ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2nd𝑔 ) = 𝐿 )
57 56 oveqd ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑥 ( 2nd𝑔 ) 𝑦 ) = ( 𝑥 𝐿 𝑦 ) )
58 57 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) = ( ( 𝑥 𝐿 𝑦 ) ‘ ) )
59 eqidd ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑎𝑥 ) = ( 𝑎𝑥 ) )
60 50 58 59 oveq123d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ · ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) )
61 48 60 eqeq12d ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ · ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ · ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) ↔ ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) ) )
62 61 ralbidv ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ∀ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ · ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ · ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) ↔ ∀ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) ) )
63 62 2ralbidv ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ · ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ · ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) ↔ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) ) )
64 34 63 rabeqbidv ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → { 𝑎X 𝑥𝐵 ( ( 𝑟𝑥 ) 𝐽 ( 𝑠𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ · ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ · ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } = { 𝑎X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) } )
65 20 28 64 csbied2 ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥𝐵 ( ( 𝑟𝑥 ) 𝐽 ( 𝑠𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ · ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ · ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } = { 𝑎X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) } )
66 10 19 65 csbied2 ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → ( 1st𝑓 ) / 𝑟 ( 1st𝑔 ) / 𝑠 { 𝑎X 𝑥𝐵 ( ( 𝑟𝑥 ) 𝐽 ( 𝑠𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑟𝑦 ) ⟩ · ( 𝑠𝑦 ) ) ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) ) = ( ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ( ⟨ ( 𝑟𝑥 ) , ( 𝑠𝑥 ) ⟩ · ( 𝑠𝑦 ) ) ( 𝑎𝑥 ) ) } = { 𝑎X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) } )
67 df-br ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
68 6 67 sylib ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
69 df-br ( 𝐾 ( 𝐶 Func 𝐷 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
70 7 69 sylib ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
71 ovex ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∈ V
72 71 rgenw 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∈ V
73 ixpexg ( ∀ 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∈ V → X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∈ V )
74 72 73 ax-mp X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∈ V
75 74 rabex { 𝑎X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ V
76 75 a1i ( 𝜑 → { 𝑎X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) } ∈ V )
77 9 66 68 70 76 ovmpod ( 𝜑 → ( ⟨ 𝐹 , 𝐺𝑁𝐾 , 𝐿 ⟩ ) = { 𝑎X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) } )
78 77 eleq2d ( 𝜑 → ( 𝐴 ∈ ( ⟨ 𝐹 , 𝐺𝑁𝐾 , 𝐿 ⟩ ) ↔ 𝐴 ∈ { 𝑎X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) } ) )
79 fveq1 ( 𝑎 = 𝐴 → ( 𝑎𝑦 ) = ( 𝐴𝑦 ) )
80 79 oveq1d ( 𝑎 = 𝐴 → ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( 𝐴𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) )
81 fveq1 ( 𝑎 = 𝐴 → ( 𝑎𝑥 ) = ( 𝐴𝑥 ) )
82 81 oveq2d ( 𝑎 = 𝐴 → ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝐴𝑥 ) ) )
83 80 82 eqeq12d ( 𝑎 = 𝐴 → ( ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) ↔ ( ( 𝐴𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝐴𝑥 ) ) ) )
84 83 ralbidv ( 𝑎 = 𝐴 → ( ∀ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) ↔ ∀ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝐴𝑥 ) ) ) )
85 84 2ralbidv ( 𝑎 = 𝐴 → ( ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) ↔ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝐴𝑥 ) ) ) )
86 85 elrab ( 𝐴 ∈ { 𝑎X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∣ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝑎𝑥 ) ) } ↔ ( 𝐴X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∧ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝐴𝑥 ) ) ) )
87 78 86 bitrdi ( 𝜑 → ( 𝐴 ∈ ( ⟨ 𝐹 , 𝐺𝑁𝐾 , 𝐿 ⟩ ) ↔ ( 𝐴X 𝑥𝐵 ( ( 𝐹𝑥 ) 𝐽 ( 𝐾𝑥 ) ) ∧ ∀ 𝑥𝐵𝑦𝐵 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴𝑦 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ · ( 𝐾𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐾𝑥 ) ⟩ · ( 𝐾𝑦 ) ) ( 𝐴𝑥 ) ) ) ) )