Metamath Proof Explorer


Theorem prfval

Description: Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses prfval.k 𝑃 = ( 𝐹 ⟨,⟩F 𝐺 )
prfval.b 𝐵 = ( Base ‘ 𝐶 )
prfval.h 𝐻 = ( Hom ‘ 𝐶 )
prfval.c ( 𝜑𝐹 ∈ ( 𝐶 Func 𝐷 ) )
prfval.d ( 𝜑𝐺 ∈ ( 𝐶 Func 𝐸 ) )
Assertion prfval ( 𝜑𝑃 = ⟨ ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ )

Proof

Step Hyp Ref Expression
1 prfval.k 𝑃 = ( 𝐹 ⟨,⟩F 𝐺 )
2 prfval.b 𝐵 = ( Base ‘ 𝐶 )
3 prfval.h 𝐻 = ( Hom ‘ 𝐶 )
4 prfval.c ( 𝜑𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5 prfval.d ( 𝜑𝐺 ∈ ( 𝐶 Func 𝐸 ) )
6 df-prf ⟨,⟩F = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ dom ( 1st𝑓 ) / 𝑏 ⟨ ( 𝑥𝑏 ↦ ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ )
7 6 a1i ( 𝜑 → ⟨,⟩F = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ dom ( 1st𝑓 ) / 𝑏 ⟨ ( 𝑥𝑏 ↦ ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ ) )
8 fvex ( 1st𝑓 ) ∈ V
9 8 dmex dom ( 1st𝑓 ) ∈ V
10 9 a1i ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → dom ( 1st𝑓 ) ∈ V )
11 simprl ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → 𝑓 = 𝐹 )
12 11 fveq2d ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → ( 1st𝑓 ) = ( 1st𝐹 ) )
13 12 dmeqd ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → dom ( 1st𝑓 ) = dom ( 1st𝐹 ) )
14 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
15 relfunc Rel ( 𝐶 Func 𝐷 )
16 1st2ndbr ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐹 ) )
17 15 4 16 sylancr ( 𝜑 → ( 1st𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐹 ) )
18 2 14 17 funcf1 ( 𝜑 → ( 1st𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
19 18 fdmd ( 𝜑 → dom ( 1st𝐹 ) = 𝐵 )
20 19 adantr ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → dom ( 1st𝐹 ) = 𝐵 )
21 13 20 eqtrd ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → dom ( 1st𝑓 ) = 𝐵 )
22 simpr ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
23 simplrl ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → 𝑓 = 𝐹 )
24 23 fveq2d ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 1st𝑓 ) = ( 1st𝐹 ) )
25 24 fveq1d ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( ( 1st𝑓 ) ‘ 𝑥 ) = ( ( 1st𝐹 ) ‘ 𝑥 ) )
26 simplrr ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → 𝑔 = 𝐺 )
27 26 fveq2d ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 1st𝑔 ) = ( 1st𝐺 ) )
28 27 fveq1d ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( ( 1st𝑔 ) ‘ 𝑥 ) = ( ( 1st𝐺 ) ‘ 𝑥 ) )
29 25 28 opeq12d ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ )
30 22 29 mpteq12dv ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑥𝑏 ↦ ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) )
31 eqidd ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) = ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) )
32 22 22 31 mpoeq123dv ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑥𝑏 , 𝑦𝑏 ↦ ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) ) )
33 23 ad2antrr ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → 𝑓 = 𝐹 )
34 33 fveq2d ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( 2nd𝑓 ) = ( 2nd𝐹 ) )
35 34 oveqd ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( 𝑥 ( 2nd𝑓 ) 𝑦 ) = ( 𝑥 ( 2nd𝐹 ) 𝑦 ) )
36 35 dmeqd ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) = dom ( 𝑥 ( 2nd𝐹 ) 𝑦 ) )
37 eqid ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
38 17 ad4antr ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( 1st𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐹 ) )
39 simplr ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → 𝑥𝐵 )
40 simpr ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → 𝑦𝐵 )
41 2 3 37 38 39 40 funcf2 ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( 𝑥 ( 2nd𝐹 ) 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( ( 1st𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st𝐹 ) ‘ 𝑦 ) ) )
42 41 fdmd ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → dom ( 𝑥 ( 2nd𝐹 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
43 36 42 eqtrd ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
44 35 fveq1d ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) = ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) )
45 26 ad2antrr ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → 𝑔 = 𝐺 )
46 45 fveq2d ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( 2nd𝑔 ) = ( 2nd𝐺 ) )
47 46 oveqd ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( 𝑥 ( 2nd𝑔 ) 𝑦 ) = ( 𝑥 ( 2nd𝐺 ) 𝑦 ) )
48 47 fveq1d ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) = ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) )
49 44 48 opeq12d ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ = ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ )
50 43 49 mpteq12dv ( ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑦𝐵 ) → ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) = ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) )
51 50 3impa ( ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) ∧ 𝑥𝐵𝑦𝐵 ) → ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) = ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) )
52 51 mpoeq3dva ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) )
53 32 52 eqtrd ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑥𝑏 , 𝑦𝑏 ↦ ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) )
54 30 53 opeq12d ( ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) ∧ 𝑏 = 𝐵 ) → ⟨ ( 𝑥𝑏 ↦ ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ = ⟨ ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ )
55 10 21 54 csbied2 ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → dom ( 1st𝑓 ) / 𝑏 ⟨ ( 𝑥𝑏 ↦ ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝑏 , 𝑦𝑏 ↦ ( ∈ dom ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝑔 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ = ⟨ ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ )
56 4 elexd ( 𝜑𝐹 ∈ V )
57 5 elexd ( 𝜑𝐺 ∈ V )
58 opex ⟨ ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ ∈ V
59 58 a1i ( 𝜑 → ⟨ ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ ∈ V )
60 7 55 56 57 59 ovmpod ( 𝜑 → ( 𝐹 ⟨,⟩F 𝐺 ) = ⟨ ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ )
61 1 60 eqtrid ( 𝜑𝑃 = ⟨ ( 𝑥𝐵 ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( ∈ ( 𝑥 𝐻 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ )