This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mapxpen

Description: Equinumerosity law for double set exponentiation. Proposition 10.45 of TakeutiZaring p. 96. (Contributed by NM, 21-Feb-2004) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion mapxpen ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ≈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ovexd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∈ V )
2 ovexd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ∈ V )
3 elmapi ⊢ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) → 𝑓 : 𝐶 ⟶ ( 𝐴 ↑m 𝐵 ) )
4 3 ffvelcdmda ⊢ ( ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝐴 ↑m 𝐵 ) )
5 elmapi ⊢ ( ( 𝑓 ‘ 𝑦 ) ∈ ( 𝐴 ↑m 𝐵 ) → ( 𝑓 ‘ 𝑦 ) : 𝐵 ⟶ 𝐴 )
6 4 5 syl ⊢ ( ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑓 ‘ 𝑦 ) : 𝐵 ⟶ 𝐴 )
7 6 ffvelcdmda ⊢ ( ( ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ∈ 𝐴 )
8 7 an32s ⊢ ( ( ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ∈ 𝐴 )
9 8 ralrimiva ⊢ ( ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐶 ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ∈ 𝐴 )
10 9 ralrimiva ⊢ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ∈ 𝐴 )
11 eqid ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) )
12 11 fmpo ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) : ( 𝐵 × 𝐶 ) ⟶ 𝐴 )
13 10 12 sylib ⊢ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) : ( 𝐵 × 𝐶 ) ⟶ 𝐴 )
14 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ∈ 𝑉 )
15 xpexg ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 × 𝐶 ) ∈ V )
16 15 3adant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 × 𝐶 ) ∈ V )
17 elmapg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 × 𝐶 ) ∈ V ) → ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) : ( 𝐵 × 𝐶 ) ⟶ 𝐴 ) )
18 14 16 17 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) : ( 𝐵 × 𝐶 ) ⟶ 𝐴 ) )
19 13 18 imbitrrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) )
20 elmapi ⊢ ( 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) → 𝑔 : ( 𝐵 × 𝐶 ) ⟶ 𝐴 )
21 20 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) → 𝑔 : ( 𝐵 × 𝐶 ) ⟶ 𝐴 )
22 fovcdm ⊢ ( ( 𝑔 : ( 𝐵 × 𝐶 ) ⟶ 𝐴 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 𝑔 𝑦 ) ∈ 𝐴 )
23 22 3expa ⊢ ( ( ( 𝑔 : ( 𝐵 × 𝐶 ) ⟶ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 𝑔 𝑦 ) ∈ 𝐴 )
24 23 an32s ⊢ ( ( ( 𝑔 : ( 𝐵 × 𝐶 ) ⟶ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝑔 𝑦 ) ∈ 𝐴 )
25 21 24 sylanl1 ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝑔 𝑦 ) ∈ 𝐴 )
26 25 fmpttd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) : 𝐵 ⟶ 𝐴 )
27 elmapg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ∈ ( 𝐴 ↑m 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) : 𝐵 ⟶ 𝐴 ) )
28 27 3adant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ∈ ( 𝐴 ↑m 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) : 𝐵 ⟶ 𝐴 ) )
29 28 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ∈ ( 𝐴 ↑m 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) : 𝐵 ⟶ 𝐴 ) )
30 26 29 mpbird ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ∈ ( 𝐴 ↑m 𝐵 ) )
31 30 fmpttd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) → ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) : 𝐶 ⟶ ( 𝐴 ↑m 𝐵 ) )
32 31 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) → ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) : 𝐶 ⟶ ( 𝐴 ↑m 𝐵 ) ) )
33 ovex ⊢ ( 𝐴 ↑m 𝐵 ) ∈ V
34 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ 𝑋 )
35 elmapg ⊢ ( ( ( 𝐴 ↑m 𝐵 ) ∈ V ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ↔ ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) : 𝐶 ⟶ ( 𝐴 ↑m 𝐵 ) ) )
36 33 34 35 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ↔ ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) : 𝐶 ⟶ ( 𝐴 ↑m 𝐵 ) ) )
37 32 36 sylibrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) → ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ) )
38 elmapfn ⊢ ( 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) → 𝑔 Fn ( 𝐵 × 𝐶 ) )
39 38 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → 𝑔 Fn ( 𝐵 × 𝐶 ) )
40 fnov ⊢ ( 𝑔 Fn ( 𝐵 × 𝐶 ) ↔ 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑔 𝑦 ) ) )
41 39 40 sylib ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑔 𝑦 ) ) )
42 simp3 ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ 𝐶 )
43 26 adantlrl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) : 𝐵 ⟶ 𝐴 )
44 43 3adant2 ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) : 𝐵 ⟶ 𝐴 )
45 simp1l2 ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → 𝐵 ∈ 𝑊 )
46 simp1l1 ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝑉 )
47 fex2 ⊢ ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) : 𝐵 ⟶ 𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ∈ V )
48 44 45 46 47 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ∈ V )
49 eqid ⊢ ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) )
50 49 fvmpt2 ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ∈ V ) → ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) )
51 42 48 50 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) )
52 51 fveq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ‘ 𝑥 ) )
53 simp2 ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → 𝑥 ∈ 𝐵 )
54 ovex ⊢ ( 𝑥 𝑔 𝑦 ) ∈ V
55 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) )
56 55 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 𝑔 𝑦 ) ∈ V ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ‘ 𝑥 ) = ( 𝑥 𝑔 𝑦 ) )
57 53 54 56 sylancl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ‘ 𝑥 ) = ( 𝑥 𝑔 𝑦 ) )
58 52 57 eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) = ( 𝑥 𝑔 𝑦 ) )
59 58 mpoeq3dva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑔 𝑦 ) ) )
60 41 59 eqtr4d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) ) )
61 eqid ⊢ 𝐵 = 𝐵
62 nfcv ⊢ Ⅎ 𝑥 𝐶
63 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) )
64 62 63 nfmpt ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) )
65 64 nfeq2 ⊢ Ⅎ 𝑥 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) )
66 nfmpt1 ⊢ Ⅎ 𝑦 ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) )
67 66 nfeq2 ⊢ Ⅎ 𝑦 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) )
68 fveq1 ⊢ ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) )
69 68 fveq1d ⊢ ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) → ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) = ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) )
70 69 a1d ⊢ ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) → ( 𝑦 ∈ 𝐶 → ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) = ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) ) )
71 67 70 ralrimi ⊢ ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) → ∀ 𝑦 ∈ 𝐶 ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) = ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) )
72 eqid ⊢ 𝐶 = 𝐶
73 71 72 jctil ⊢ ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) → ( 𝐶 = 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) = ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) ) )
74 73 a1d ⊢ ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) → ( 𝑥 ∈ 𝐵 → ( 𝐶 = 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) = ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) ) ) )
75 65 74 ralrimi ⊢ ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝐶 = 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) = ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) ) )
76 mpoeq123 ⊢ ( ( 𝐵 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐶 = 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) = ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) ) ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) ) )
77 61 75 76 sylancr ⊢ ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) ) )
78 77 eqeq2d ⊢ ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) → ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ↔ 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ‘ 𝑦 ) ‘ 𝑥 ) ) ) )
79 60 78 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) → 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) )
80 3 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → 𝑓 : 𝐶 ⟶ ( 𝐴 ↑m 𝐵 ) )
81 80 feqmptd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑓 ‘ 𝑦 ) ) )
82 simprl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) )
83 82 6 sylan ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑓 ‘ 𝑦 ) : 𝐵 ⟶ 𝐴 )
84 83 feqmptd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑓 ‘ 𝑦 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) )
85 84 mpteq2dva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → ( 𝑦 ∈ 𝐶 ↦ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) )
86 81 85 eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) )
87 nfmpo2 ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) )
88 87 nfeq2 ⊢ Ⅎ 𝑦 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) )
89 eqidd ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → 𝐵 = 𝐵 )
90 nfmpo1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) )
91 90 nfeq2 ⊢ Ⅎ 𝑥 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) )
92 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐶
93 fvex ⊢ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ∈ V
94 11 ovmpt4g ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ∧ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ∈ V ) → ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) 𝑦 ) = ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) )
95 93 94 mp3an3 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) 𝑦 ) = ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) )
96 oveq ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) 𝑦 ) )
97 96 eqeq1d ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ( ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ↔ ( 𝑥 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) 𝑦 ) = ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) )
98 95 97 imbitrrid ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) )
99 98 expcomd ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ( 𝑦 ∈ 𝐶 → ( 𝑥 ∈ 𝐵 → ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) )
100 91 92 99 ralrimd ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ( 𝑦 ∈ 𝐶 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) )
101 mpteq12 ⊢ ( ( 𝐵 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) )
102 89 100 101 syl6an ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ( 𝑦 ∈ 𝐶 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) )
103 88 102 ralrimi ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ∀ 𝑦 ∈ 𝐶 ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) )
104 mpteq12 ⊢ ( ( 𝐶 = 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) → ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) )
105 72 103 104 sylancr ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) )
106 105 eqeq2d ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ↔ 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) ) )
107 86 106 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ) )
108 79 107 impbid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) ) → ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ↔ 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) )
109 108 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) → ( 𝑓 = ( 𝑦 ∈ 𝐶 ↦ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 𝑔 𝑦 ) ) ) ↔ 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ) ) )
110 1 2 19 37 109 en3d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ≈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) )