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	ffvelrnda	⊢ ( ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝐴 ↑m 𝐵 ) )
5		elmapi	⊢ ( ( 𝑓 ‘ 𝑦 ) ∈ ( 𝐴 ↑m 𝐵 ) → ( 𝑓 ‘ 𝑦 ) : 𝐵 ⟶ 𝐴 )
6	4 5	syl	⊢ ( ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑓 ‘ 𝑦 ) : 𝐵 ⟶ 𝐴 )
7	6	ffvelrnda	⊢ ( ( ( 𝑓 ∈ ( ( 𝐴 ↑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	syl5ibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑓 ∈ ( ( 𝐴 ↑m 𝐵 ) ↑m 𝐶 ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) )
20		elmapi	⊢ ( 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) → 𝑔 : ( 𝐵 × 𝐶 ) ⟶ 𝐴 )
21	20	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝑔 ∈ ( 𝐴 ↑m ( 𝐵 × 𝐶 ) ) ) → 𝑔 : ( 𝐵 × 𝐶 ) ⟶ 𝐴 )
22		fovrn	⊢ ( ( 𝑔 : ( 𝐵 × 𝐶 ) ⟶ 𝐴 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 𝑔 𝑦 ) ∈ 𝐴 )
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	syl5ibr	⊢ ( 𝑔 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑦 ) ‘ 𝑥 ) ) )
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 ( 𝐵 × 𝐶 ) ) )