xpmapenlem

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

	Ref	Expression
Hypotheses	xpmapen.1	$⊢ A \in V$
	xpmapen.2	$⊢ B \in V$
	xpmapen.3	$⊢ C \in V$
	xpmapenlem.4	$⊢ D = (z \in C ⟼ 1^{st} (x (z)))$
	xpmapenlem.5	$⊢ R = (z \in C ⟼ 2^{nd} (x (z)))$
	xpmapenlem.6	$⊢ S = (z \in C ⟼ ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩)$
Assertion	xpmapenlem	$⊢ ({(A \times B)}^{C}) \approx ((A^{C}) \times (B^{C}))$

Proof

Step	Hyp	Ref	Expression
1		xpmapen.1	$⊢ A \in V$
2		xpmapen.2	$⊢ B \in V$
3		xpmapen.3	$⊢ C \in V$
4		xpmapenlem.4	$⊢ D = (z \in C ⟼ 1^{st} (x (z)))$
5		xpmapenlem.5	$⊢ R = (z \in C ⟼ 2^{nd} (x (z)))$
6		xpmapenlem.6	$⊢ S = (z \in C ⟼ ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩)$
7		ovex	$⊢ {(A \times B)}^{C} \in V$
8		ovex	$⊢ A^{C} \in V$
9		ovex	$⊢ B^{C} \in V$
10	8 9	xpex	$⊢ (A^{C}) \times (B^{C}) \in V$
11	1 2	xpex	$⊢ A \times B \in V$
12	11 3	elmap	$⊢ x \in ({(A \times B)}^{C}) \leftrightarrow x : C ⟶ A \times B$
13		ffvelrn	$⊢ (x : C ⟶ A \times B \land z \in C) \to x (z) \in (A \times B)$
14	12 13	sylanb	$⊢ (x \in ({(A \times B)}^{C}) \land z \in C) \to x (z) \in (A \times B)$
15		xp1st	$⊢ x (z) \in (A \times B) \to 1^{st} (x (z)) \in A$
16	14 15	syl	$⊢ (x \in ({(A \times B)}^{C}) \land z \in C) \to 1^{st} (x (z)) \in A$
17	16 4	fmptd	$⊢ x \in ({(A \times B)}^{C}) \to D : C ⟶ A$
18	1 3	elmap	$⊢ D \in (A^{C}) \leftrightarrow D : C ⟶ A$
19	17 18	sylibr	$⊢ x \in ({(A \times B)}^{C}) \to D \in (A^{C})$
20		xp2nd	$⊢ x (z) \in (A \times B) \to 2^{nd} (x (z)) \in B$
21	14 20	syl	$⊢ (x \in ({(A \times B)}^{C}) \land z \in C) \to 2^{nd} (x (z)) \in B$
22	21 5	fmptd	$⊢ x \in ({(A \times B)}^{C}) \to R : C ⟶ B$
23	2 3	elmap	$⊢ R \in (B^{C}) \leftrightarrow R : C ⟶ B$
24	22 23	sylibr	$⊢ x \in ({(A \times B)}^{C}) \to R \in (B^{C})$
25	19 24	opelxpd	$⊢ x \in ({(A \times B)}^{C}) \to ⟨D, R⟩ \in ((A^{C}) \times (B^{C}))$
26		xp1st	$⊢ y \in ((A^{C}) \times (B^{C})) \to 1^{st} (y) \in (A^{C})$
27	1 3	elmap	$⊢ 1^{st} (y) \in (A^{C}) \leftrightarrow 1^{st} (y) : C ⟶ A$
28	26 27	sylib	$⊢ y \in ((A^{C}) \times (B^{C})) \to 1^{st} (y) : C ⟶ A$
29	28	ffvelrnda	$⊢ (y \in ((A^{C}) \times (B^{C})) \land z \in C) \to 1^{st} (y) (z) \in A$
30		xp2nd	$⊢ y \in ((A^{C}) \times (B^{C})) \to 2^{nd} (y) \in (B^{C})$
31	2 3	elmap	$⊢ 2^{nd} (y) \in (B^{C}) \leftrightarrow 2^{nd} (y) : C ⟶ B$
32	30 31	sylib	$⊢ y \in ((A^{C}) \times (B^{C})) \to 2^{nd} (y) : C ⟶ B$
33	32	ffvelrnda	$⊢ (y \in ((A^{C}) \times (B^{C})) \land z \in C) \to 2^{nd} (y) (z) \in B$
34	29 33	opelxpd	$⊢ (y \in ((A^{C}) \times (B^{C})) \land z \in C) \to ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩ \in (A \times B)$
35	34 6	fmptd	$⊢ y \in ((A^{C}) \times (B^{C})) \to S : C ⟶ A \times B$
36	11 3	elmap	$⊢ S \in ({(A \times B)}^{C}) \leftrightarrow S : C ⟶ A \times B$
37	35 36	sylibr	$⊢ y \in ((A^{C}) \times (B^{C})) \to S \in ({(A \times B)}^{C})$
38		1st2nd2	$⊢ y \in ((A^{C}) \times (B^{C})) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
39	38	ad2antlr	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
40	28	feqmptd	$⊢ y \in ((A^{C}) \times (B^{C})) \to 1^{st} (y) = (z \in C ⟼ 1^{st} (y) (z))$
41	40	ad2antlr	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to 1^{st} (y) = (z \in C ⟼ 1^{st} (y) (z))$
42		simplr	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \land z \in C) \to x = S$
43	42	fveq1d	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \land z \in C) \to x (z) = S (z)$
44		opex	$⊢ ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩ \in V$
45	6	fvmpt2	$⊢ (z \in C \land ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩ \in V) \to S (z) = ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩$
46	44 45	mpan2	$⊢ z \in C \to S (z) = ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩$
47	46	adantl	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \land z \in C) \to S (z) = ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩$
48	43 47	eqtrd	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \land z \in C) \to x (z) = ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩$
49	48	fveq2d	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \land z \in C) \to 1^{st} (x (z)) = 1^{st} (⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩)$
50		fvex	$⊢ 1^{st} (y) (z) \in V$
51		fvex	$⊢ 2^{nd} (y) (z) \in V$
52	50 51	op1st	$⊢ 1^{st} (⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩) = 1^{st} (y) (z)$
53	49 52	eqtrdi	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \land z \in C) \to 1^{st} (x (z)) = 1^{st} (y) (z)$
54	53	mpteq2dva	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to (z \in C ⟼ 1^{st} (x (z))) = (z \in C ⟼ 1^{st} (y) (z))$
55	4 54	syl5eq	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to D = (z \in C ⟼ 1^{st} (y) (z))$
56	41 55	eqtr4d	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to 1^{st} (y) = D$
57	32	feqmptd	$⊢ y \in ((A^{C}) \times (B^{C})) \to 2^{nd} (y) = (z \in C ⟼ 2^{nd} (y) (z))$
58	57	ad2antlr	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to 2^{nd} (y) = (z \in C ⟼ 2^{nd} (y) (z))$
59	48	fveq2d	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \land z \in C) \to 2^{nd} (x (z)) = 2^{nd} (⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩)$
60	50 51	op2nd	$⊢ 2^{nd} (⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩) = 2^{nd} (y) (z)$
61	59 60	eqtrdi	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \land z \in C) \to 2^{nd} (x (z)) = 2^{nd} (y) (z)$
62	61	mpteq2dva	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to (z \in C ⟼ 2^{nd} (x (z))) = (z \in C ⟼ 2^{nd} (y) (z))$
63	5 62	syl5eq	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to R = (z \in C ⟼ 2^{nd} (y) (z))$
64	58 63	eqtr4d	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to 2^{nd} (y) = R$
65	56 64	opeq12d	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to ⟨1^{st} (y), 2^{nd} (y)⟩ = ⟨D, R⟩$
66	39 65	eqtrd	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land x = S) \to y = ⟨D, R⟩$
67		simpll	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to x \in ({(A \times B)}^{C})$
68	67 12	sylib	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to x : C ⟶ A \times B$
69	68	feqmptd	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to x = (z \in C ⟼ x (z))$
70		simpr	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to y = ⟨D, R⟩$
71	70	fveq2d	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to 1^{st} (y) = 1^{st} (⟨D, R⟩)$
72	19	ad2antrr	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to D \in (A^{C})$
73	24	ad2antrr	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to R \in (B^{C})$
74		op1stg	$⊢ (D \in (A^{C}) \land R \in (B^{C})) \to 1^{st} (⟨D, R⟩) = D$
75	72 73 74	syl2anc	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to 1^{st} (⟨D, R⟩) = D$
76	71 75	eqtrd	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to 1^{st} (y) = D$
77	76	fveq1d	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to 1^{st} (y) (z) = D (z)$
78		fvex	$⊢ 1^{st} (x (z)) \in V$
79	4	fvmpt2	$⊢ (z \in C \land 1^{st} (x (z)) \in V) \to D (z) = 1^{st} (x (z))$
80	78 79	mpan2	$⊢ z \in C \to D (z) = 1^{st} (x (z))$
81	77 80	sylan9eq	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \land z \in C) \to 1^{st} (y) (z) = 1^{st} (x (z))$
82	70	fveq2d	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to 2^{nd} (y) = 2^{nd} (⟨D, R⟩)$
83		op2ndg	$⊢ (D \in (A^{C}) \land R \in (B^{C})) \to 2^{nd} (⟨D, R⟩) = R$
84	72 73 83	syl2anc	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to 2^{nd} (⟨D, R⟩) = R$
85	82 84	eqtrd	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to 2^{nd} (y) = R$
86	85	fveq1d	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to 2^{nd} (y) (z) = R (z)$
87		fvex	$⊢ 2^{nd} (x (z)) \in V$
88	5	fvmpt2	$⊢ (z \in C \land 2^{nd} (x (z)) \in V) \to R (z) = 2^{nd} (x (z))$
89	87 88	mpan2	$⊢ z \in C \to R (z) = 2^{nd} (x (z))$
90	86 89	sylan9eq	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \land z \in C) \to 2^{nd} (y) (z) = 2^{nd} (x (z))$
91	81 90	opeq12d	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \land z \in C) \to ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩ = ⟨1^{st} (x (z)), 2^{nd} (x (z))⟩$
92	68	ffvelrnda	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \land z \in C) \to x (z) \in (A \times B)$
93		1st2nd2	$⊢ x (z) \in (A \times B) \to x (z) = ⟨1^{st} (x (z)), 2^{nd} (x (z))⟩$
94	92 93	syl	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \land z \in C) \to x (z) = ⟨1^{st} (x (z)), 2^{nd} (x (z))⟩$
95	91 94	eqtr4d	$⊢ (((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \land z \in C) \to ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩ = x (z)$
96	95	mpteq2dva	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to (z \in C ⟼ ⟨1^{st} (y) (z), 2^{nd} (y) (z)⟩) = (z \in C ⟼ x (z))$
97	6 96	syl5eq	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to S = (z \in C ⟼ x (z))$
98	69 97	eqtr4d	$⊢ ((x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \land y = ⟨D, R⟩) \to x = S$
99	66 98	impbida	$⊢ (x \in ({(A \times B)}^{C}) \land y \in ((A^{C}) \times (B^{C}))) \to (x = S \leftrightarrow y = ⟨D, R⟩)$
100	7 10 25 37 99	en3i	$⊢ ({(A \times B)}^{C}) \approx ((A^{C}) \times (B^{C}))$

Metamath Proof Explorer

Theorem xpmapenlem

Proof