Metamath Proof Explorer


Theorem prf1st

Description: Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses prf1st.p 𝑃 = ( 𝐹 ⟨,⟩F 𝐺 )
prf1st.c ( 𝜑𝐹 ∈ ( 𝐶 Func 𝐷 ) )
prf1st.d ( 𝜑𝐺 ∈ ( 𝐶 Func 𝐸 ) )
Assertion prf1st ( 𝜑 → ( ( 𝐷 1stF 𝐸 ) ∘func 𝑃 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 prf1st.p 𝑃 = ( 𝐹 ⟨,⟩F 𝐺 )
2 prf1st.c ( 𝜑𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3 prf1st.d ( 𝜑𝐺 ∈ ( 𝐶 Func 𝐸 ) )
4 eqid ( 𝐷 ×c 𝐸 ) = ( 𝐷 ×c 𝐸 )
5 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
6 eqid ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
7 4 5 6 xpcbas ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) = ( Base ‘ ( 𝐷 ×c 𝐸 ) )
8 eqid ( Hom ‘ ( 𝐷 ×c 𝐸 ) ) = ( Hom ‘ ( 𝐷 ×c 𝐸 ) )
9 funcrcl ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
10 2 9 syl ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
11 10 simprd ( 𝜑𝐷 ∈ Cat )
12 11 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
13 funcrcl ( 𝐺 ∈ ( 𝐶 Func 𝐸 ) → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
14 3 13 syl ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
15 14 simprd ( 𝜑𝐸 ∈ Cat )
16 15 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
17 eqid ( 𝐷 1stF 𝐸 ) = ( 𝐷 1stF 𝐸 )
18 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
19 relfunc Rel ( 𝐶 Func 𝐷 )
20 1st2ndbr ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐹 ) )
21 19 2 20 sylancr ( 𝜑 → ( 1st𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐹 ) )
22 18 5 21 funcf1 ( 𝜑 → ( 1st𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
23 22 ffvelrnda ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
24 relfunc Rel ( 𝐶 Func 𝐸 )
25 1st2ndbr ( ( Rel ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) → ( 1st𝐺 ) ( 𝐶 Func 𝐸 ) ( 2nd𝐺 ) )
26 24 3 25 sylancr ( 𝜑 → ( 1st𝐺 ) ( 𝐶 Func 𝐸 ) ( 2nd𝐺 ) )
27 18 6 26 funcf1 ( 𝜑 → ( 1st𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
28 27 ffvelrnda ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
29 23 28 opelxpd ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
30 4 7 8 12 16 17 29 1stf1 ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) = ( 1st ‘ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) )
31 fvex ( ( 1st𝐹 ) ‘ 𝑥 ) ∈ V
32 fvex ( ( 1st𝐺 ) ‘ 𝑥 ) ∈ V
33 31 32 op1st ( 1st ‘ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) = ( ( 1st𝐹 ) ‘ 𝑥 )
34 30 33 eqtrdi ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) = ( ( 1st𝐹 ) ‘ 𝑥 ) )
35 34 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1st𝐹 ) ‘ 𝑥 ) ) )
36 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
37 1 18 36 2 3 prfval ( 𝜑𝑃 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ )
38 fvex ( Base ‘ 𝐶 ) ∈ V
39 38 mptex ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) ∈ V
40 38 38 mpoex ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ∈ V
41 39 40 op1std ( 𝑃 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ ) ⟩ ) ) ⟩ → ( 1st𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) )
42 37 41 syl ( 𝜑 → ( 1st𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) )
43 relfunc Rel ( ( 𝐷 ×c 𝐸 ) Func 𝐷 )
44 4 11 15 17 1stfcl ( 𝜑 → ( 𝐷 1stF 𝐸 ) ∈ ( ( 𝐷 ×c 𝐸 ) Func 𝐷 ) )
45 1st2ndbr ( ( Rel ( ( 𝐷 ×c 𝐸 ) Func 𝐷 ) ∧ ( 𝐷 1stF 𝐸 ) ∈ ( ( 𝐷 ×c 𝐸 ) Func 𝐷 ) ) → ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 𝐷 ×c 𝐸 ) Func 𝐷 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) )
46 43 44 45 sylancr ( 𝜑 → ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 𝐷 ×c 𝐸 ) Func 𝐷 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) )
47 7 5 46 funcf1 ( 𝜑 → ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) : ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) ⟶ ( Base ‘ 𝐷 ) )
48 47 feqmptd ( 𝜑 → ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) ↦ ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ 𝑢 ) ) )
49 fveq2 ( 𝑢 = ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ → ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ 𝑢 ) = ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) )
50 29 42 48 49 fmptco ( 𝜑 → ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ∘ ( 1st𝑃 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ ) ) )
51 22 feqmptd ( 𝜑 → ( 1st𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1st𝐹 ) ‘ 𝑥 ) ) )
52 35 50 51 3eqtr4d ( 𝜑 → ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ∘ ( 1st𝑃 ) ) = ( 1st𝐹 ) )
53 11 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐷 ∈ Cat )
54 15 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐸 ∈ Cat )
55 relfunc Rel ( 𝐶 Func ( 𝐷 ×c 𝐸 ) )
56 1 4 2 3 prfcl ( 𝜑𝑃 ∈ ( 𝐶 Func ( 𝐷 ×c 𝐸 ) ) )
57 1st2ndbr ( ( Rel ( 𝐶 Func ( 𝐷 ×c 𝐸 ) ) ∧ 𝑃 ∈ ( 𝐶 Func ( 𝐷 ×c 𝐸 ) ) ) → ( 1st𝑃 ) ( 𝐶 Func ( 𝐷 ×c 𝐸 ) ) ( 2nd𝑃 ) )
58 55 56 57 sylancr ( 𝜑 → ( 1st𝑃 ) ( 𝐶 Func ( 𝐷 ×c 𝐸 ) ) ( 2nd𝑃 ) )
59 18 7 58 funcf1 ( 𝜑 → ( 1st𝑃 ) : ( Base ‘ 𝐶 ) ⟶ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
60 59 ffvelrnda ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st𝑃 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
61 60 adantrr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st𝑃 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
62 61 adantr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 1st𝑃 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
63 59 ffvelrnda ( ( 𝜑𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st𝑃 ) ‘ 𝑦 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
64 63 adantrl ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st𝑃 ) ‘ 𝑦 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
65 64 adantr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 1st𝑃 ) ‘ 𝑦 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
66 4 7 8 53 54 17 62 65 1stf2 ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) = ( 1st ↾ ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×c 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ) )
67 66 fveq1d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 1st ↾ ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×c 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ) ‘ ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ) )
68 58 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st𝑃 ) ( 𝐶 Func ( 𝐷 ×c 𝐸 ) ) ( 2nd𝑃 ) )
69 simprl ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
70 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
71 18 36 8 68 69 70 funcf2 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd𝑃 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×c 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) )
72 71 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×c 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) )
73 72 fvresd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 1st ↾ ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×c 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ) ‘ ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( 1st ‘ ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ) )
74 2 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
75 3 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
76 69 adantr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
77 70 adantr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
78 simpr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
79 1 18 36 74 75 76 77 78 prf2 ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) = ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ )
80 79 fveq2d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1st ‘ ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( 1st ‘ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ ) )
81 fvex ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑓 ) ∈ V
82 fvex ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ 𝑓 ) ∈ V
83 81 82 op1st ( 1st ‘ ⟨ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2nd𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ ) = ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑓 )
84 80 83 eqtrdi ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1st ‘ ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑓 ) )
85 67 73 84 3eqtrd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑓 ) )
86 85 mpteq2dva ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ) ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
87 eqid ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
88 46 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 𝐷 ×c 𝐸 ) Func 𝐷 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) )
89 7 8 87 88 61 64 funcf2 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) : ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×c 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ⟶ ( ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ ( ( 1st𝑃 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ ( ( 1st𝑃 ) ‘ 𝑦 ) ) ) )
90 fcompt ( ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) : ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×c 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ⟶ ( ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ ( ( 1st𝑃 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ‘ ( ( 1st𝑃 ) ‘ 𝑦 ) ) ) ∧ ( 𝑥 ( 2nd𝑃 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×c 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ) → ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ) ) )
91 89 71 90 syl2anc ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ‘ 𝑓 ) ) ) )
92 21 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐹 ) )
93 18 36 87 92 69 70 funcf2 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st𝐹 ) ‘ 𝑦 ) ) )
94 93 feqmptd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd𝐹 ) 𝑦 ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
95 86 91 94 3eqtr4d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ) = ( 𝑥 ( 2nd𝐹 ) 𝑦 ) )
96 95 3impb ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ) = ( 𝑥 ( 2nd𝐹 ) 𝑦 ) )
97 96 mpoeq3dva ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ) )
98 18 21 funcfn2 ( 𝜑 → ( 2nd𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
99 fnov ( ( 2nd𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 2nd𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ) )
100 98 99 sylib ( 𝜑 → ( 2nd𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2nd𝐹 ) 𝑦 ) ) )
101 97 100 eqtr4d ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ) ) = ( 2nd𝐹 ) )
102 52 101 opeq12d ( 𝜑 → ⟨ ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ∘ ( 1st𝑃 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ) ) ⟩ = ⟨ ( 1st𝐹 ) , ( 2nd𝐹 ) ⟩ )
103 18 56 44 cofuval ( 𝜑 → ( ( 𝐷 1stF 𝐸 ) ∘func 𝑃 ) = ⟨ ( ( 1st ‘ ( 𝐷 1stF 𝐸 ) ) ∘ ( 1st𝑃 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1st𝑃 ) ‘ 𝑥 ) ( 2nd ‘ ( 𝐷 1stF 𝐸 ) ) ( ( 1st𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd𝑃 ) 𝑦 ) ) ) ⟩ )
104 1st2nd ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1st𝐹 ) , ( 2nd𝐹 ) ⟩ )
105 19 2 104 sylancr ( 𝜑𝐹 = ⟨ ( 1st𝐹 ) , ( 2nd𝐹 ) ⟩ )
106 102 103 105 3eqtr4d ( 𝜑 → ( ( 𝐷 1stF 𝐸 ) ∘func 𝑃 ) = 𝐹 )