Step |
Hyp |
Ref |
Expression |
1 |
|
omeulem1 |
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. x e. On E. y e. A ( ( A .o x ) +o y ) = B ) |
2 |
|
opex |
|- <. x , y >. e. _V |
3 |
2
|
isseti |
|- E. z z = <. x , y >. |
4 |
|
19.41v |
|- ( E. z ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> ( E. z z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) |
5 |
3 4
|
mpbiran |
|- ( E. z ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> ( ( A .o x ) +o y ) = B ) |
6 |
5
|
rexbii |
|- ( E. y e. A E. z ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> E. y e. A ( ( A .o x ) +o y ) = B ) |
7 |
|
rexcom4 |
|- ( E. y e. A E. z ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> E. z E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) |
8 |
6 7
|
bitr3i |
|- ( E. y e. A ( ( A .o x ) +o y ) = B <-> E. z E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) |
9 |
8
|
rexbii |
|- ( E. x e. On E. y e. A ( ( A .o x ) +o y ) = B <-> E. x e. On E. z E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) |
10 |
|
rexcom4 |
|- ( E. x e. On E. z E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> E. z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) |
11 |
9 10
|
bitri |
|- ( E. x e. On E. y e. A ( ( A .o x ) +o y ) = B <-> E. z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) |
12 |
1 11
|
sylib |
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) |
13 |
|
simp2rl |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> z = <. x , y >. ) |
14 |
|
simp3rl |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> t = <. r , s >. ) |
15 |
|
simp2rr |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> ( ( A .o x ) +o y ) = B ) |
16 |
|
simp3rr |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> ( ( A .o r ) +o s ) = B ) |
17 |
15 16
|
eqtr4d |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> ( ( A .o x ) +o y ) = ( ( A .o r ) +o s ) ) |
18 |
|
simp11 |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> A e. On ) |
19 |
|
simp13 |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> A =/= (/) ) |
20 |
|
simp2ll |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> x e. On ) |
21 |
|
simp2lr |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> y e. A ) |
22 |
|
simp3ll |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> r e. On ) |
23 |
|
simp3lr |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> s e. A ) |
24 |
|
omopth2 |
|- ( ( ( A e. On /\ A =/= (/) ) /\ ( x e. On /\ y e. A ) /\ ( r e. On /\ s e. A ) ) -> ( ( ( A .o x ) +o y ) = ( ( A .o r ) +o s ) <-> ( x = r /\ y = s ) ) ) |
25 |
18 19 20 21 22 23 24
|
syl222anc |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> ( ( ( A .o x ) +o y ) = ( ( A .o r ) +o s ) <-> ( x = r /\ y = s ) ) ) |
26 |
17 25
|
mpbid |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> ( x = r /\ y = s ) ) |
27 |
|
opeq12 |
|- ( ( x = r /\ y = s ) -> <. x , y >. = <. r , s >. ) |
28 |
26 27
|
syl |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> <. x , y >. = <. r , s >. ) |
29 |
14 28
|
eqtr4d |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> t = <. x , y >. ) |
30 |
13 29
|
eqtr4d |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) /\ ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) -> z = t ) |
31 |
30
|
3expia |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) ) -> ( ( ( r e. On /\ s e. A ) /\ ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) -> z = t ) ) |
32 |
31
|
exp4b |
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( ( ( x e. On /\ y e. A ) /\ ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) -> ( ( r e. On /\ s e. A ) -> ( ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) -> z = t ) ) ) ) |
33 |
32
|
expd |
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( ( x e. On /\ y e. A ) -> ( ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) -> ( ( r e. On /\ s e. A ) -> ( ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) -> z = t ) ) ) ) ) |
34 |
33
|
rexlimdvv |
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) -> ( ( r e. On /\ s e. A ) -> ( ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) -> z = t ) ) ) ) |
35 |
34
|
imp |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) -> ( ( r e. On /\ s e. A ) -> ( ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) -> z = t ) ) ) |
36 |
35
|
rexlimdvv |
|- ( ( ( A e. On /\ B e. On /\ A =/= (/) ) /\ E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) -> ( E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) -> z = t ) ) |
37 |
36
|
expimpd |
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> ( ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) /\ E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) -> z = t ) ) |
38 |
37
|
alrimivv |
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> A. z A. t ( ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) /\ E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) -> z = t ) ) |
39 |
|
opeq1 |
|- ( x = r -> <. x , y >. = <. r , y >. ) |
40 |
39
|
eqeq2d |
|- ( x = r -> ( z = <. x , y >. <-> z = <. r , y >. ) ) |
41 |
|
oveq2 |
|- ( x = r -> ( A .o x ) = ( A .o r ) ) |
42 |
41
|
oveq1d |
|- ( x = r -> ( ( A .o x ) +o y ) = ( ( A .o r ) +o y ) ) |
43 |
42
|
eqeq1d |
|- ( x = r -> ( ( ( A .o x ) +o y ) = B <-> ( ( A .o r ) +o y ) = B ) ) |
44 |
40 43
|
anbi12d |
|- ( x = r -> ( ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> ( z = <. r , y >. /\ ( ( A .o r ) +o y ) = B ) ) ) |
45 |
|
opeq2 |
|- ( y = s -> <. r , y >. = <. r , s >. ) |
46 |
45
|
eqeq2d |
|- ( y = s -> ( z = <. r , y >. <-> z = <. r , s >. ) ) |
47 |
|
oveq2 |
|- ( y = s -> ( ( A .o r ) +o y ) = ( ( A .o r ) +o s ) ) |
48 |
47
|
eqeq1d |
|- ( y = s -> ( ( ( A .o r ) +o y ) = B <-> ( ( A .o r ) +o s ) = B ) ) |
49 |
46 48
|
anbi12d |
|- ( y = s -> ( ( z = <. r , y >. /\ ( ( A .o r ) +o y ) = B ) <-> ( z = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) |
50 |
44 49
|
cbvrex2vw |
|- ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> E. r e. On E. s e. A ( z = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) |
51 |
|
eqeq1 |
|- ( z = t -> ( z = <. r , s >. <-> t = <. r , s >. ) ) |
52 |
51
|
anbi1d |
|- ( z = t -> ( ( z = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) <-> ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) |
53 |
52
|
2rexbidv |
|- ( z = t -> ( E. r e. On E. s e. A ( z = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) <-> E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) |
54 |
50 53
|
syl5bb |
|- ( z = t -> ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) ) |
55 |
54
|
eu4 |
|- ( E! z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) <-> ( E. z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) /\ A. z A. t ( ( E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) /\ E. r e. On E. s e. A ( t = <. r , s >. /\ ( ( A .o r ) +o s ) = B ) ) -> z = t ) ) ) |
56 |
12 38 55
|
sylanbrc |
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E! z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) ) |