Metamath Proof Explorer


Theorem xpmapenlem

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

Ref Expression
Hypotheses xpmapen.1 A V
xpmapen.2 B V
xpmapen.3 C V
xpmapenlem.4 D = z C 1 st x z
xpmapenlem.5 R = z C 2 nd x z
xpmapenlem.6 S = z C 1 st y z 2 nd y z
Assertion xpmapenlem A × B C A C × B C

Proof

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