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 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
9	8	a1i	⊢ ( 𝜑 → 𝑁 = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) )
10		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → ( 1^st ‘ 𝑓 ) ∈ V )
11		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → ( 1^st ‘ 𝑓 ) = ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
13		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
14		brrelex12	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
15	13 6 14	sylancr	⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
16		op1stg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
17	15 16	syl	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
18	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
19	12 18	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → ( 1^st ‘ 𝑓 ) = 𝐹 )
20		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → ( 1^st ‘ 𝑔 ) ∈ V )
21		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ )
22	21	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → ( 1^st ‘ 𝑔 ) = ( 1^st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) )
23		brrelex12	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐾 ( 𝐶 Func 𝐷 ) 𝐿 ) → ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) )
24	13 7 23	sylancr	⊢ ( 𝜑 → ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) )
25		op1stg	⊢ ( ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) → ( 1^st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
26	24 25	syl	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
27	26	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → ( 1^st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
28	22 27	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → ( 1^st ‘ 𝑔 ) = 𝐾 )
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	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2^nd ‘ 𝑓 ) = ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
42		op2ndg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
43	15 42	syl	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
44	43	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
45	41 44	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2^nd ‘ 𝑓 ) = 𝐺 )
46	45	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
47	46	fveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) = ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) )
48	38 39 47	oveq123d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) )
49	30 32	opeq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ )
50	49 37	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) = ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) )
51	21	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ )
52	51	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2^nd ‘ 𝑔 ) = ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) )
53		op2ndg	⊢ ( ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) → ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
54	24 53	syl	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
55	54	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
56	52 55	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 2^nd ‘ 𝑔 ) = 𝐿 )
57	56	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) = ( 𝑥 𝐿 𝑦 ) )
58	57	fveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) = ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) )
59		eqidd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑥 ) )
60	50 58 59	oveq123d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) )
61	48 60	eqeq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
62	61	ralbidv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
63	62	2ralbidv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
64	34 63	rabeqbidv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) ∧ 𝑠 = 𝐾 ) → { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
65	20 28 64	csbied2	⊢ ( ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) ∧ 𝑟 = 𝐹 ) → ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
66	10 19 65	csbied2	⊢ ( ( 𝜑 ∧ ( 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ∧ 𝑔 = ⟨ 𝐾 , 𝐿 ⟩ ) ) → ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ 𝐵 ( ( 𝑟 ‘ 𝑥 ) 𝐽 ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ · ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = { 𝑎 ∈ 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 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )

Metamath Proof Explorer

Theorem isnat

Proof