xpmapenlem

Description: Lemma for xpmapen . (Contributed by NM, 1-May-2004) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Hypotheses	xpmapen.1	⊢ 𝐴 ∈ V
	xpmapen.2	⊢ 𝐵 ∈ V
	xpmapen.3	⊢ 𝐶 ∈ V
	xpmapenlem.4	⊢ 𝐷 = ( 𝑧 ∈ 𝐶 ↦ ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) )
	xpmapenlem.5	⊢ 𝑅 = ( 𝑧 ∈ 𝐶 ↦ ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) )
	xpmapenlem.6	⊢ 𝑆 = ( 𝑧 ∈ 𝐶 ↦ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ )
Assertion	xpmapenlem	⊢ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ≈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		xpmapen.1	⊢ 𝐴 ∈ V
2		xpmapen.2	⊢ 𝐵 ∈ V
3		xpmapen.3	⊢ 𝐶 ∈ V
4		xpmapenlem.4	⊢ 𝐷 = ( 𝑧 ∈ 𝐶 ↦ ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) )
5		xpmapenlem.5	⊢ 𝑅 = ( 𝑧 ∈ 𝐶 ↦ ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) )
6		xpmapenlem.6	⊢ 𝑆 = ( 𝑧 ∈ 𝐶 ↦ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ )
7		ovex	⊢ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∈ V
8		ovex	⊢ ( 𝐴 ↑_m 𝐶 ) ∈ V
9		ovex	⊢ ( 𝐵 ↑_m 𝐶 ) ∈ V
10	8 9	xpex	⊢ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ∈ V
11	1 2	xpex	⊢ ( 𝐴 × 𝐵 ) ∈ V
12	11 3	elmap	⊢ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ↔ 𝑥 : 𝐶 ⟶ ( 𝐴 × 𝐵 ) )
13		ffvelrn	⊢ ( ( 𝑥 : 𝐶 ⟶ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ‘ 𝑧 ) ∈ ( 𝐴 × 𝐵 ) )
14	12 13	sylanb	⊢ ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ‘ 𝑧 ) ∈ ( 𝐴 × 𝐵 ) )
15		xp1st	⊢ ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝐴 × 𝐵 ) → ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) ∈ 𝐴 )
16	14 15	syl	⊢ ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑧 ∈ 𝐶 ) → ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) ∈ 𝐴 )
17	16 4	fmptd	⊢ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) → 𝐷 : 𝐶 ⟶ 𝐴 )
18	1 3	elmap	⊢ ( 𝐷 ∈ ( 𝐴 ↑_m 𝐶 ) ↔ 𝐷 : 𝐶 ⟶ 𝐴 )
19	17 18	sylibr	⊢ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) → 𝐷 ∈ ( 𝐴 ↑_m 𝐶 ) )
20		xp2nd	⊢ ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝐴 × 𝐵 ) → ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) ∈ 𝐵 )
21	14 20	syl	⊢ ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑧 ∈ 𝐶 ) → ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) ∈ 𝐵 )
22	21 5	fmptd	⊢ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) → 𝑅 : 𝐶 ⟶ 𝐵 )
23	2 3	elmap	⊢ ( 𝑅 ∈ ( 𝐵 ↑_m 𝐶 ) ↔ 𝑅 : 𝐶 ⟶ 𝐵 )
24	22 23	sylibr	⊢ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) → 𝑅 ∈ ( 𝐵 ↑_m 𝐶 ) )
25	19 24	opelxpd	⊢ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) → ⟨ 𝐷 , 𝑅 ⟩ ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) )
26		xp1st	⊢ ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) → ( 1^st ‘ 𝑦 ) ∈ ( 𝐴 ↑_m 𝐶 ) )
27	1 3	elmap	⊢ ( ( 1^st ‘ 𝑦 ) ∈ ( 𝐴 ↑_m 𝐶 ) ↔ ( 1^st ‘ 𝑦 ) : 𝐶 ⟶ 𝐴 )
28	26 27	sylib	⊢ ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) → ( 1^st ‘ 𝑦 ) : 𝐶 ⟶ 𝐴 )
29	28	ffvelrnda	⊢ ( ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ∧ 𝑧 ∈ 𝐶 ) → ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) ∈ 𝐴 )
30		xp2nd	⊢ ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) → ( 2^nd ‘ 𝑦 ) ∈ ( 𝐵 ↑_m 𝐶 ) )
31	2 3	elmap	⊢ ( ( 2^nd ‘ 𝑦 ) ∈ ( 𝐵 ↑_m 𝐶 ) ↔ ( 2^nd ‘ 𝑦 ) : 𝐶 ⟶ 𝐵 )
32	30 31	sylib	⊢ ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) → ( 2^nd ‘ 𝑦 ) : 𝐶 ⟶ 𝐵 )
33	32	ffvelrnda	⊢ ( ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ∧ 𝑧 ∈ 𝐶 ) → ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ∈ 𝐵 )
34	29 33	opelxpd	⊢ ( ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ∧ 𝑧 ∈ 𝐶 ) → ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ ∈ ( 𝐴 × 𝐵 ) )
35	34 6	fmptd	⊢ ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) → 𝑆 : 𝐶 ⟶ ( 𝐴 × 𝐵 ) )
36	11 3	elmap	⊢ ( 𝑆 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ↔ 𝑆 : 𝐶 ⟶ ( 𝐴 × 𝐵 ) )
37	35 36	sylibr	⊢ ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) → 𝑆 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) )
38		1st2nd2	⊢ ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
39	38	ad2antlr	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
40	28	feqmptd	⊢ ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) → ( 1^st ‘ 𝑦 ) = ( 𝑧 ∈ 𝐶 ↦ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) ) )
41	40	ad2antlr	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → ( 1^st ‘ 𝑦 ) = ( 𝑧 ∈ 𝐶 ↦ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) ) )
42		simplr	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) ∧ 𝑧 ∈ 𝐶 ) → 𝑥 = 𝑆 )
43	42	fveq1d	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ‘ 𝑧 ) = ( 𝑆 ‘ 𝑧 ) )
44		opex	⊢ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ ∈ V
45	6	fvmpt2	⊢ ( ( 𝑧 ∈ 𝐶 ∧ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ ∈ V ) → ( 𝑆 ‘ 𝑧 ) = ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ )
46	44 45	mpan2	⊢ ( 𝑧 ∈ 𝐶 → ( 𝑆 ‘ 𝑧 ) = ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ )
47	46	adantl	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑆 ‘ 𝑧 ) = ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ )
48	43 47	eqtrd	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ‘ 𝑧 ) = ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ )
49	48	fveq2d	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) ∧ 𝑧 ∈ 𝐶 ) → ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ ) )
50		fvex	⊢ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) ∈ V
51		fvex	⊢ ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ∈ V
52	50 51	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ ) = ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 )
53	49 52	syl6eq	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) ∧ 𝑧 ∈ 𝐶 ) → ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) )
54	53	mpteq2dva	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → ( 𝑧 ∈ 𝐶 ↦ ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐶 ↦ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) ) )
55	4 54	syl5eq	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → 𝐷 = ( 𝑧 ∈ 𝐶 ↦ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) ) )
56	41 55	eqtr4d	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → ( 1^st ‘ 𝑦 ) = 𝐷 )
57	32	feqmptd	⊢ ( 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) → ( 2^nd ‘ 𝑦 ) = ( 𝑧 ∈ 𝐶 ↦ ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ) )
58	57	ad2antlr	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → ( 2^nd ‘ 𝑦 ) = ( 𝑧 ∈ 𝐶 ↦ ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ) )
59	48	fveq2d	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) ∧ 𝑧 ∈ 𝐶 ) → ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ ) )
60	50 51	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ ) = ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 )
61	59 60	syl6eq	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) ∧ 𝑧 ∈ 𝐶 ) → ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) = ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) )
62	61	mpteq2dva	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → ( 𝑧 ∈ 𝐶 ↦ ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐶 ↦ ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ) )
63	5 62	syl5eq	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → 𝑅 = ( 𝑧 ∈ 𝐶 ↦ ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ) )
64	58 63	eqtr4d	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → ( 2^nd ‘ 𝑦 ) = 𝑅 )
65	56 64	opeq12d	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ = ⟨ 𝐷 , 𝑅 ⟩ )
66	39 65	eqtrd	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑥 = 𝑆 ) → 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ )
67		simpll	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) )
68	67 12	sylib	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → 𝑥 : 𝐶 ⟶ ( 𝐴 × 𝐵 ) )
69	68	feqmptd	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → 𝑥 = ( 𝑧 ∈ 𝐶 ↦ ( 𝑥 ‘ 𝑧 ) ) )
70		simpr	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ )
71	70	fveq2d	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → ( 1^st ‘ 𝑦 ) = ( 1^st ‘ ⟨ 𝐷 , 𝑅 ⟩ ) )
72	19	ad2antrr	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → 𝐷 ∈ ( 𝐴 ↑_m 𝐶 ) )
73	24	ad2antrr	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → 𝑅 ∈ ( 𝐵 ↑_m 𝐶 ) )
74		op1stg	⊢ ( ( 𝐷 ∈ ( 𝐴 ↑_m 𝐶 ) ∧ 𝑅 ∈ ( 𝐵 ↑_m 𝐶 ) ) → ( 1^st ‘ ⟨ 𝐷 , 𝑅 ⟩ ) = 𝐷 )
75	72 73 74	syl2anc	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → ( 1^st ‘ ⟨ 𝐷 , 𝑅 ⟩ ) = 𝐷 )
76	71 75	eqtrd	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → ( 1^st ‘ 𝑦 ) = 𝐷 )
77	76	fveq1d	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) = ( 𝐷 ‘ 𝑧 ) )
78		fvex	⊢ ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) ∈ V
79	4	fvmpt2	⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) ∈ V ) → ( 𝐷 ‘ 𝑧 ) = ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) )
80	78 79	mpan2	⊢ ( 𝑧 ∈ 𝐶 → ( 𝐷 ‘ 𝑧 ) = ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) )
81	77 80	sylan9eq	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) ∧ 𝑧 ∈ 𝐶 ) → ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) = ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) )
82	70	fveq2d	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → ( 2^nd ‘ 𝑦 ) = ( 2^nd ‘ ⟨ 𝐷 , 𝑅 ⟩ ) )
83		op2ndg	⊢ ( ( 𝐷 ∈ ( 𝐴 ↑_m 𝐶 ) ∧ 𝑅 ∈ ( 𝐵 ↑_m 𝐶 ) ) → ( 2^nd ‘ ⟨ 𝐷 , 𝑅 ⟩ ) = 𝑅 )
84	72 73 83	syl2anc	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → ( 2^nd ‘ ⟨ 𝐷 , 𝑅 ⟩ ) = 𝑅 )
85	82 84	eqtrd	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → ( 2^nd ‘ 𝑦 ) = 𝑅 )
86	85	fveq1d	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) = ( 𝑅 ‘ 𝑧 ) )
87		fvex	⊢ ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) ∈ V
88	5	fvmpt2	⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) ∈ V ) → ( 𝑅 ‘ 𝑧 ) = ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) )
89	87 88	mpan2	⊢ ( 𝑧 ∈ 𝐶 → ( 𝑅 ‘ 𝑧 ) = ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) )
90	86 89	sylan9eq	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) ∧ 𝑧 ∈ 𝐶 ) → ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) = ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) )
91	81 90	opeq12d	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) ∧ 𝑧 ∈ 𝐶 ) → ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ = ⟨ ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) ⟩ )
92	68	ffvelrnda	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ‘ 𝑧 ) ∈ ( 𝐴 × 𝐵 ) )
93		1st2nd2	⊢ ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝐴 × 𝐵 ) → ( 𝑥 ‘ 𝑧 ) = ⟨ ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) ⟩ )
94	92 93	syl	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ‘ 𝑧 ) = ⟨ ( 1^st ‘ ( 𝑥 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝑥 ‘ 𝑧 ) ) ⟩ )
95	91 94	eqtr4d	⊢ ( ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) ∧ 𝑧 ∈ 𝐶 ) → ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ = ( 𝑥 ‘ 𝑧 ) )
96	95	mpteq2dva	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → ( 𝑧 ∈ 𝐶 ↦ ⟨ ( ( 1^st ‘ 𝑦 ) ‘ 𝑧 ) , ( ( 2^nd ‘ 𝑦 ) ‘ 𝑧 ) ⟩ ) = ( 𝑧 ∈ 𝐶 ↦ ( 𝑥 ‘ 𝑧 ) ) )
97	6 96	syl5eq	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → 𝑆 = ( 𝑧 ∈ 𝐶 ↦ ( 𝑥 ‘ 𝑧 ) ) )
98	69 97	eqtr4d	⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) ∧ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) → 𝑥 = 𝑆 )
99	66 98	impbida	⊢ ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) ) ) → ( 𝑥 = 𝑆 ↔ 𝑦 = ⟨ 𝐷 , 𝑅 ⟩ ) )
100	7 10 25 37 99	en3i	⊢ ( ( 𝐴 × 𝐵 ) ↑_m 𝐶 ) ≈ ( ( 𝐴 ↑_m 𝐶 ) × ( 𝐵 ↑_m 𝐶 ) )

Metamath Proof Explorer

Theorem xpmapenlem

Proof