Metamath Proof Explorer

Theorem upixp

Description: Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypotheses upixp.1 ⊢ 𝑋 = X 𝑏 ∈ 𝐴 ( 𝐶 ‘ 𝑏 )
upixp.2 ⊢ 𝑃 = ( 𝑤 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑤 ) ) )
Assertion upixp ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) → ∃! ℎ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) )

Proof

Step Hyp Ref Expression
1 upixp.1 ⊢ 𝑋 = X 𝑏 ∈ 𝐴 ( 𝐶 ‘ 𝑏 )
2 upixp.2 ⊢ 𝑃 = ( 𝑤 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑤 ) ) )
3 mptexg ⊢ ( 𝐵 ∈ 𝑆 → ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ∈ V )
4 3 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) → ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ∈ V )
5 ffvelcdm ⊢ ( ( ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑎 ) )
6 5 expcom ⊢ ( 𝑢 ∈ 𝐵 → ( ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) → ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑎 ) ) )
7 6 ralimdv ⊢ ( 𝑢 ∈ 𝐵 → ( ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) → ∀ 𝑎 ∈ 𝐴 ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑎 ) ) )
8 7 impcom ⊢ ( ( ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ∧ 𝑢 ∈ 𝐵 ) → ∀ 𝑎 ∈ 𝐴 ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑎 ) )
9 8 3ad2antl3 ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑢 ∈ 𝐵 ) → ∀ 𝑎 ∈ 𝐴 ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑎 ) )
10 fveq2 ⊢ ( 𝑎 = 𝑠 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑠 ) )
11 10 fveq1d ⊢ ( 𝑎 = 𝑠 → ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) = ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) )
12 fveq2 ⊢ ( 𝑎 = 𝑠 → ( 𝐶 ‘ 𝑎 ) = ( 𝐶 ‘ 𝑠 ) )
13 11 12 eleq12d ⊢ ( 𝑎 = 𝑠 → ( ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑎 ) ↔ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑠 ) ) )
14 13 cbvralvw ⊢ ( ∀ 𝑎 ∈ 𝐴 ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑎 ) ↔ ∀ 𝑠 ∈ 𝐴 ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑠 ) )
15 9 14 sylib ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑢 ∈ 𝐵 ) → ∀ 𝑠 ∈ 𝐴 ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑠 ) )
16 simpl1 ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑢 ∈ 𝐵 ) → 𝐴 ∈ 𝑅 )
17 mptelixpg ⊢ ( 𝐴 ∈ 𝑅 → ( ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ∈ X 𝑠 ∈ 𝐴 ( 𝐶 ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝐴 ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑠 ) ) )
18 16 17 syl ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ∈ X 𝑠 ∈ 𝐴 ( 𝐶 ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝐴 ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ∈ ( 𝐶 ‘ 𝑠 ) ) )
19 15 18 mpbird ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ∈ X 𝑠 ∈ 𝐴 ( 𝐶 ‘ 𝑠 ) )
20 fveq2 ⊢ ( 𝑏 = 𝑠 → ( 𝐶 ‘ 𝑏 ) = ( 𝐶 ‘ 𝑠 ) )
21 20 cbvixpv ⊢ X 𝑏 ∈ 𝐴 ( 𝐶 ‘ 𝑏 ) = X 𝑠 ∈ 𝐴 ( 𝐶 ‘ 𝑠 )
22 1 21 eqtri ⊢ 𝑋 = X 𝑠 ∈ 𝐴 ( 𝐶 ‘ 𝑠 )
23 19 22 eleqtrrdi ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ∈ 𝑋 )
24 23 fmpttd ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) → ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) : 𝐵 ⟶ 𝑋 )
25 nfv ⊢ Ⅎ 𝑎 𝐴 ∈ 𝑅
26 nfv ⊢ Ⅎ 𝑎 𝐵 ∈ 𝑆
27 nfra1 ⊢ Ⅎ 𝑎 ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 )
28 25 26 27 nf3an ⊢ Ⅎ 𝑎 ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) )
29 fveq2 ⊢ ( 𝑠 = 𝑎 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑎 ) )
30 29 fveq1d ⊢ ( 𝑠 = 𝑎 → ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) = ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) )
31 eqid ⊢ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) = ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) )
32 fvex ⊢ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ∈ V
33 30 31 32 fvmpt3i ⊢ ( 𝑎 ∈ 𝐴 → ( ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ‘ 𝑎 ) = ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) )
34 33 adantl ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ‘ 𝑎 ) = ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) )
35 34 mpteq2dv ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ‘ 𝑎 ) ) = ( 𝑢 ∈ 𝐵 ↦ ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) ) )
36 23 adantlr ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ∈ 𝑋 )
37 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) = ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) )
38 fveq2 ⊢ ( 𝑤 = 𝑎 → ( 𝑥 ‘ 𝑤 ) = ( 𝑥 ‘ 𝑎 ) )
39 38 mpteq2dv ⊢ ( 𝑤 = 𝑎 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑎 ) ) )
40 fvex ⊢ ( 𝐶 ‘ 𝑏 ) ∈ V
41 40 rgenw ⊢ ∀ 𝑏 ∈ 𝐴 ( 𝐶 ‘ 𝑏 ) ∈ V
42 ixpexg ⊢ ( ∀ 𝑏 ∈ 𝐴 ( 𝐶 ‘ 𝑏 ) ∈ V → X 𝑏 ∈ 𝐴 ( 𝐶 ‘ 𝑏 ) ∈ V )
43 41 42 ax-mp ⊢ X 𝑏 ∈ 𝐴 ( 𝐶 ‘ 𝑏 ) ∈ V
44 1 43 eqeltri ⊢ 𝑋 ∈ V
45 44 mptex ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑤 ) ) ∈ V
46 39 2 45 fvmpt3i ⊢ ( 𝑎 ∈ 𝐴 → ( 𝑃 ‘ 𝑎 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑎 ) ) )
47 46 adantl ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑃 ‘ 𝑎 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑎 ) ) )
48 fveq1 ⊢ ( 𝑥 = ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) → ( 𝑥 ‘ 𝑎 ) = ( ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ‘ 𝑎 ) )
49 36 37 47 48 fmptco ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑃 ‘ 𝑎 ) ∘ ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) = ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ‘ 𝑎 ) ) )
50 rsp ⊢ ( ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) → ( 𝑎 ∈ 𝐴 → ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) )
51 50 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) → ( 𝑎 ∈ 𝐴 → ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) )
52 51 imp ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) )
53 52 feqmptd ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝑢 ∈ 𝐵 ↦ ( ( 𝐹 ‘ 𝑎 ) ‘ 𝑢 ) ) )
54 35 49 53 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) )
55 54 ex ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) → ( 𝑎 ∈ 𝐴 → ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) ) )
56 28 55 ralrimi ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) )
57 simprl ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) → ℎ : 𝐵 ⟶ 𝑋 )
58 57 feqmptd ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) → ℎ = ( 𝑢 ∈ 𝐵 ↦ ( ℎ ‘ 𝑢 ) ) )
59 simplrr ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) )
60 fveq2 ⊢ ( 𝑎 = 𝑠 → ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑠 ) )
61 60 coeq1d ⊢ ( 𝑎 = 𝑠 → ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) = ( ( 𝑃 ‘ 𝑠 ) ∘ ℎ ) )
62 10 61 eqeq12d ⊢ ( 𝑎 = 𝑠 → ( ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ↔ ( 𝐹 ‘ 𝑠 ) = ( ( 𝑃 ‘ 𝑠 ) ∘ ℎ ) ) )
63 62 rspccva ⊢ ( ( ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑠 ) = ( ( 𝑃 ‘ 𝑠 ) ∘ ℎ ) )
64 59 63 sylan ⊢ ( ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑠 ) = ( ( 𝑃 ‘ 𝑠 ) ∘ ℎ ) )
65 64 fveq1d ⊢ ( ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) = ( ( ( 𝑃 ‘ 𝑠 ) ∘ ℎ ) ‘ 𝑢 ) )
66 fvco3 ⊢ ( ( ℎ : 𝐵 ⟶ 𝑋 ∧ 𝑢 ∈ 𝐵 ) → ( ( ( 𝑃 ‘ 𝑠 ) ∘ ℎ ) ‘ 𝑢 ) = ( ( 𝑃 ‘ 𝑠 ) ‘ ( ℎ ‘ 𝑢 ) ) )
67 57 66 sylan ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ( ( 𝑃 ‘ 𝑠 ) ∘ ℎ ) ‘ 𝑢 ) = ( ( 𝑃 ‘ 𝑠 ) ‘ ( ℎ ‘ 𝑢 ) ) )
68 67 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝑃 ‘ 𝑠 ) ∘ ℎ ) ‘ 𝑢 ) = ( ( 𝑃 ‘ 𝑠 ) ‘ ( ℎ ‘ 𝑢 ) ) )
69 fveq2 ⊢ ( 𝑤 = 𝑠 → ( 𝑥 ‘ 𝑤 ) = ( 𝑥 ‘ 𝑠 ) )
70 69 mpteq2dv ⊢ ( 𝑤 = 𝑠 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑠 ) ) )
71 70 2 45 fvmpt3i ⊢ ( 𝑠 ∈ 𝐴 → ( 𝑃 ‘ 𝑠 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑠 ) ) )
72 71 adantl ⊢ ( ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑃 ‘ 𝑠 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑠 ) ) )
73 72 fveq1d ⊢ ( ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑃 ‘ 𝑠 ) ‘ ( ℎ ‘ 𝑢 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑠 ) ) ‘ ( ℎ ‘ 𝑢 ) ) )
74 ffvelcdm ⊢ ( ( ℎ : 𝐵 ⟶ 𝑋 ∧ 𝑢 ∈ 𝐵 ) → ( ℎ ‘ 𝑢 ) ∈ 𝑋 )
75 57 74 sylan ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ℎ ‘ 𝑢 ) ∈ 𝑋 )
76 fveq1 ⊢ ( 𝑥 = ( ℎ ‘ 𝑢 ) → ( 𝑥 ‘ 𝑠 ) = ( ( ℎ ‘ 𝑢 ) ‘ 𝑠 ) )
77 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑠 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑠 ) )
78 fvex ⊢ ( 𝑥 ‘ 𝑠 ) ∈ V
79 76 77 78 fvmpt3i ⊢ ( ( ℎ ‘ 𝑢 ) ∈ 𝑋 → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑠 ) ) ‘ ( ℎ ‘ 𝑢 ) ) = ( ( ℎ ‘ 𝑢 ) ‘ 𝑠 ) )
80 75 79 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑠 ) ) ‘ ( ℎ ‘ 𝑢 ) ) = ( ( ℎ ‘ 𝑢 ) ‘ 𝑠 ) )
81 80 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ‘ 𝑠 ) ) ‘ ( ℎ ‘ 𝑢 ) ) = ( ( ℎ ‘ 𝑢 ) ‘ 𝑠 ) )
82 73 81 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑃 ‘ 𝑠 ) ‘ ( ℎ ‘ 𝑢 ) ) = ( ( ℎ ‘ 𝑢 ) ‘ 𝑠 ) )
83 65 68 82 3eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) = ( ( ℎ ‘ 𝑢 ) ‘ 𝑠 ) )
84 83 mpteq2dva ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) = ( 𝑠 ∈ 𝐴 ↦ ( ( ℎ ‘ 𝑢 ) ‘ 𝑠 ) ) )
85 75 1 eleqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ℎ ‘ 𝑢 ) ∈ X 𝑏 ∈ 𝐴 ( 𝐶 ‘ 𝑏 ) )
86 ixpfn ⊢ ( ( ℎ ‘ 𝑢 ) ∈ X 𝑏 ∈ 𝐴 ( 𝐶 ‘ 𝑏 ) → ( ℎ ‘ 𝑢 ) Fn 𝐴 )
87 85 86 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ℎ ‘ 𝑢 ) Fn 𝐴 )
88 dffn5 ⊢ ( ( ℎ ‘ 𝑢 ) Fn 𝐴 ↔ ( ℎ ‘ 𝑢 ) = ( 𝑠 ∈ 𝐴 ↦ ( ( ℎ ‘ 𝑢 ) ‘ 𝑠 ) ) )
89 87 88 sylib ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ℎ ‘ 𝑢 ) = ( 𝑠 ∈ 𝐴 ↦ ( ( ℎ ‘ 𝑢 ) ‘ 𝑠 ) ) )
90 84 89 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) = ( ℎ ‘ 𝑢 ) )
91 90 mpteq2dva ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) → ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) = ( 𝑢 ∈ 𝐵 ↦ ( ℎ ‘ 𝑢 ) ) )
92 58 91 eqtr4d ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) ∧ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ) → ℎ = ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) )
93 92 ex ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) → ( ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) → ℎ = ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) )
94 93 alrimiv ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) → ∀ ℎ ( ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) → ℎ = ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) )
95 feq1 ⊢ ( ℎ = ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) → ( ℎ : 𝐵 ⟶ 𝑋 ↔ ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) : 𝐵 ⟶ 𝑋 ) )
96 coeq2 ⊢ ( ℎ = ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) → ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) )
97 96 eqeq2d ⊢ ( ℎ = ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ↔ ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) ) )
98 97 ralbidv ⊢ ( ℎ = ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) → ( ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ↔ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) ) )
99 95 98 anbi12d ⊢ ( ℎ = ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) → ( ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) ↔ ( ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) ) ) )
100 99 eqeu ⊢ ( ( ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ∈ V ∧ ( ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) ) ∧ ∀ ℎ ( ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) → ℎ = ( 𝑢 ∈ 𝐵 ↦ ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑠 ) ‘ 𝑢 ) ) ) ) ) → ∃! ℎ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) )
101 4 24 56 94 100 syl121anc ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) : 𝐵 ⟶ ( 𝐶 ‘ 𝑎 ) ) → ∃! ℎ ( ℎ : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( 𝑃 ‘ 𝑎 ) ∘ ℎ ) ) )