Step |
Hyp |
Ref |
Expression |
1 |
|
reu3op.a |
|- ( p = <. a , b >. -> ( ps <-> ch ) ) |
2 |
|
reuop.x |
|- ( p = <. x , y >. -> ( ps <-> th ) ) |
3 |
|
nfsbc1v |
|- F/ p [. q / p ]. ps |
4 |
|
nfsbc1v |
|- F/ p [. w / p ]. ps |
5 |
|
sbceq1a |
|- ( p = w -> ( ps <-> [. w / p ]. ps ) ) |
6 |
|
dfsbcq |
|- ( w = q -> ( [. w / p ]. ps <-> [. q / p ]. ps ) ) |
7 |
3 4 5 6
|
reu8nf |
|- ( E! p e. ( X X. Y ) ps <-> E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) ) |
8 |
|
elxp2 |
|- ( p e. ( X X. Y ) <-> E. a e. X E. b e. Y p = <. a , b >. ) |
9 |
1
|
biimpcd |
|- ( ps -> ( p = <. a , b >. -> ch ) ) |
10 |
9
|
adantr |
|- ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> ( p = <. a , b >. -> ch ) ) |
11 |
10
|
adantr |
|- ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) -> ( p = <. a , b >. -> ch ) ) |
12 |
11
|
imp |
|- ( ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) /\ p = <. a , b >. ) -> ch ) |
13 |
|
opelxpi |
|- ( ( x e. X /\ y e. Y ) -> <. x , y >. e. ( X X. Y ) ) |
14 |
|
dfsbcq |
|- ( q = <. x , y >. -> ( [. q / p ]. ps <-> [. <. x , y >. / p ]. ps ) ) |
15 |
|
eqeq2 |
|- ( q = <. x , y >. -> ( p = q <-> p = <. x , y >. ) ) |
16 |
14 15
|
imbi12d |
|- ( q = <. x , y >. -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) ) ) |
17 |
16
|
adantl |
|- ( ( ( x e. X /\ y e. Y ) /\ q = <. x , y >. ) -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) ) ) |
18 |
13 17
|
rspcdv |
|- ( ( x e. X /\ y e. Y ) -> ( A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) -> ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) ) ) |
19 |
18
|
adantr |
|- ( ( ( x e. X /\ y e. Y ) /\ ps ) -> ( A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) -> ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) ) ) |
20 |
|
opex |
|- <. x , y >. e. _V |
21 |
20 2
|
sbcie |
|- ( [. <. x , y >. / p ]. ps <-> th ) |
22 |
|
pm2.27 |
|- ( [. <. x , y >. / p ]. ps -> ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> p = <. x , y >. ) ) |
23 |
21 22
|
sylbir |
|- ( th -> ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> p = <. x , y >. ) ) |
24 |
|
eqcom |
|- ( <. x , y >. = p <-> p = <. x , y >. ) |
25 |
23 24
|
syl6ibr |
|- ( th -> ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> <. x , y >. = p ) ) |
26 |
25
|
com12 |
|- ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> ( th -> <. x , y >. = p ) ) |
27 |
|
eqeq2 |
|- ( <. a , b >. = p -> ( <. x , y >. = <. a , b >. <-> <. x , y >. = p ) ) |
28 |
27
|
eqcoms |
|- ( p = <. a , b >. -> ( <. x , y >. = <. a , b >. <-> <. x , y >. = p ) ) |
29 |
28
|
imbi2d |
|- ( p = <. a , b >. -> ( ( th -> <. x , y >. = <. a , b >. ) <-> ( th -> <. x , y >. = p ) ) ) |
30 |
26 29
|
syl5ibrcom |
|- ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> ( p = <. a , b >. -> ( th -> <. x , y >. = <. a , b >. ) ) ) |
31 |
30
|
a1d |
|- ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> ( ( a e. X /\ b e. Y ) -> ( p = <. a , b >. -> ( th -> <. x , y >. = <. a , b >. ) ) ) ) |
32 |
19 31
|
syl6 |
|- ( ( ( x e. X /\ y e. Y ) /\ ps ) -> ( A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) -> ( ( a e. X /\ b e. Y ) -> ( p = <. a , b >. -> ( th -> <. x , y >. = <. a , b >. ) ) ) ) ) |
33 |
32
|
expimpd |
|- ( ( x e. X /\ y e. Y ) -> ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> ( ( a e. X /\ b e. Y ) -> ( p = <. a , b >. -> ( th -> <. x , y >. = <. a , b >. ) ) ) ) ) |
34 |
33
|
imp4c |
|- ( ( x e. X /\ y e. Y ) -> ( ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) /\ p = <. a , b >. ) -> ( th -> <. x , y >. = <. a , b >. ) ) ) |
35 |
34
|
impcom |
|- ( ( ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) /\ p = <. a , b >. ) /\ ( x e. X /\ y e. Y ) ) -> ( th -> <. x , y >. = <. a , b >. ) ) |
36 |
35
|
ralrimivva |
|- ( ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) /\ p = <. a , b >. ) -> A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) |
37 |
12 36
|
jca |
|- ( ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) /\ p = <. a , b >. ) -> ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) |
38 |
37
|
ex |
|- ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) -> ( p = <. a , b >. -> ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) ) |
39 |
38
|
reximdvva |
|- ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> ( E. a e. X E. b e. Y p = <. a , b >. -> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) ) |
40 |
39
|
com12 |
|- ( E. a e. X E. b e. Y p = <. a , b >. -> ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) ) |
41 |
8 40
|
sylbi |
|- ( p e. ( X X. Y ) -> ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) ) |
42 |
41
|
rexlimiv |
|- ( E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) |
43 |
|
opelxpi |
|- ( ( a e. X /\ b e. Y ) -> <. a , b >. e. ( X X. Y ) ) |
44 |
43
|
adantr |
|- ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> <. a , b >. e. ( X X. Y ) ) |
45 |
|
simprl |
|- ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> ch ) |
46 |
|
nfsbc1v |
|- F/ x [. c / x ]. th |
47 |
|
nfv |
|- F/ x <. c , y >. = <. a , b >. |
48 |
46 47
|
nfim |
|- F/ x ( [. c / x ]. th -> <. c , y >. = <. a , b >. ) |
49 |
|
nfsbc1v |
|- F/ y [. d / y ]. [. c / x ]. th |
50 |
|
nfv |
|- F/ y <. c , d >. = <. a , b >. |
51 |
49 50
|
nfim |
|- F/ y ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) |
52 |
|
sbceq1a |
|- ( x = c -> ( th <-> [. c / x ]. th ) ) |
53 |
|
opeq1 |
|- ( x = c -> <. x , y >. = <. c , y >. ) |
54 |
53
|
eqeq1d |
|- ( x = c -> ( <. x , y >. = <. a , b >. <-> <. c , y >. = <. a , b >. ) ) |
55 |
52 54
|
imbi12d |
|- ( x = c -> ( ( th -> <. x , y >. = <. a , b >. ) <-> ( [. c / x ]. th -> <. c , y >. = <. a , b >. ) ) ) |
56 |
|
sbceq1a |
|- ( y = d -> ( [. c / x ]. th <-> [. d / y ]. [. c / x ]. th ) ) |
57 |
|
opeq2 |
|- ( y = d -> <. c , y >. = <. c , d >. ) |
58 |
57
|
eqeq1d |
|- ( y = d -> ( <. c , y >. = <. a , b >. <-> <. c , d >. = <. a , b >. ) ) |
59 |
56 58
|
imbi12d |
|- ( y = d -> ( ( [. c / x ]. th -> <. c , y >. = <. a , b >. ) <-> ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) ) ) |
60 |
48 51 55 59
|
rspc2 |
|- ( ( c e. X /\ d e. Y ) -> ( A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) -> ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) ) ) |
61 |
60
|
ad2antlr |
|- ( ( ( ( a e. X /\ b e. Y ) /\ ( c e. X /\ d e. Y ) ) /\ ch ) -> ( A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) -> ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) ) ) |
62 |
2
|
sbcop |
|- ( [. d / y ]. [. c / x ]. th <-> [. <. c , d >. / p ]. ps ) |
63 |
|
pm2.27 |
|- ( [. d / y ]. [. c / x ]. th -> ( ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) -> <. c , d >. = <. a , b >. ) ) |
64 |
62 63
|
sylbir |
|- ( [. <. c , d >. / p ]. ps -> ( ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) -> <. c , d >. = <. a , b >. ) ) |
65 |
|
eqcom |
|- ( <. a , b >. = <. c , d >. <-> <. c , d >. = <. a , b >. ) |
66 |
64 65
|
syl6ibr |
|- ( [. <. c , d >. / p ]. ps -> ( ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) -> <. a , b >. = <. c , d >. ) ) |
67 |
66
|
com12 |
|- ( ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) |
68 |
61 67
|
syl6 |
|- ( ( ( ( a e. X /\ b e. Y ) /\ ( c e. X /\ d e. Y ) ) /\ ch ) -> ( A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) ) |
69 |
68
|
expimpd |
|- ( ( ( a e. X /\ b e. Y ) /\ ( c e. X /\ d e. Y ) ) -> ( ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) ) |
70 |
69
|
expcom |
|- ( ( c e. X /\ d e. Y ) -> ( ( a e. X /\ b e. Y ) -> ( ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) ) ) |
71 |
70
|
impd |
|- ( ( c e. X /\ d e. Y ) -> ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) ) |
72 |
71
|
impcom |
|- ( ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) /\ ( c e. X /\ d e. Y ) ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) |
73 |
|
dfsbcq |
|- ( q = <. c , d >. -> ( [. q / p ]. ps <-> [. <. c , d >. / p ]. ps ) ) |
74 |
|
eqeq2 |
|- ( q = <. c , d >. -> ( <. a , b >. = q <-> <. a , b >. = <. c , d >. ) ) |
75 |
73 74
|
imbi12d |
|- ( q = <. c , d >. -> ( ( [. q / p ]. ps -> <. a , b >. = q ) <-> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) ) |
76 |
72 75
|
syl5ibrcom |
|- ( ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) /\ ( c e. X /\ d e. Y ) ) -> ( q = <. c , d >. -> ( [. q / p ]. ps -> <. a , b >. = q ) ) ) |
77 |
76
|
rexlimdvva |
|- ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> ( E. c e. X E. d e. Y q = <. c , d >. -> ( [. q / p ]. ps -> <. a , b >. = q ) ) ) |
78 |
|
elxp2 |
|- ( q e. ( X X. Y ) <-> E. c e. X E. d e. Y q = <. c , d >. ) |
79 |
78
|
biimpi |
|- ( q e. ( X X. Y ) -> E. c e. X E. d e. Y q = <. c , d >. ) |
80 |
77 79
|
impel |
|- ( ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) /\ q e. ( X X. Y ) ) -> ( [. q / p ]. ps -> <. a , b >. = q ) ) |
81 |
80
|
ralrimiva |
|- ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) ) |
82 |
|
nfv |
|- F/ p ch |
83 |
|
nfcv |
|- F/_ p ( X X. Y ) |
84 |
|
nfv |
|- F/ p <. a , b >. = q |
85 |
3 84
|
nfim |
|- F/ p ( [. q / p ]. ps -> <. a , b >. = q ) |
86 |
83 85
|
nfralw |
|- F/ p A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) |
87 |
82 86
|
nfan |
|- F/ p ( ch /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) ) |
88 |
|
eqeq1 |
|- ( p = <. a , b >. -> ( p = q <-> <. a , b >. = q ) ) |
89 |
88
|
imbi2d |
|- ( p = <. a , b >. -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. q / p ]. ps -> <. a , b >. = q ) ) ) |
90 |
89
|
ralbidv |
|- ( p = <. a , b >. -> ( A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) <-> A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) ) ) |
91 |
1 90
|
anbi12d |
|- ( p = <. a , b >. -> ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) <-> ( ch /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) ) ) ) |
92 |
87 91
|
rspce |
|- ( ( <. a , b >. e. ( X X. Y ) /\ ( ch /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) ) ) -> E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) ) |
93 |
44 45 81 92
|
syl12anc |
|- ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) ) |
94 |
93
|
ex |
|- ( ( a e. X /\ b e. Y ) -> ( ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) -> E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) ) ) |
95 |
94
|
rexlimivv |
|- ( E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) -> E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) ) |
96 |
42 95
|
impbii |
|- ( E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) <-> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) |
97 |
7 96
|
bitri |
|- ( E! p e. ( X X. Y ) ps <-> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) |