Step |
Hyp |
Ref |
Expression |
1 |
|
simpl2l |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> B e. On ) |
2 |
|
eloni |
|- ( B e. On -> Ord B ) |
3 |
1 2
|
syl |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> Ord B ) |
4 |
|
simpl3l |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> D e. On ) |
5 |
|
eloni |
|- ( D e. On -> Ord D ) |
6 |
4 5
|
syl |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> Ord D ) |
7 |
|
ordtri3or |
|- ( ( Ord B /\ Ord D ) -> ( B e. D \/ B = D \/ D e. B ) ) |
8 |
3 6 7
|
syl2anc |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( B e. D \/ B = D \/ D e. B ) ) |
9 |
|
simpr |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) |
10 |
|
simpl1l |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> A e. On ) |
11 |
|
omcl |
|- ( ( A e. On /\ D e. On ) -> ( A .o D ) e. On ) |
12 |
10 4 11
|
syl2anc |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( A .o D ) e. On ) |
13 |
|
simpl3r |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> E e. A ) |
14 |
|
onelon |
|- ( ( A e. On /\ E e. A ) -> E e. On ) |
15 |
10 13 14
|
syl2anc |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> E e. On ) |
16 |
|
oacl |
|- ( ( ( A .o D ) e. On /\ E e. On ) -> ( ( A .o D ) +o E ) e. On ) |
17 |
12 15 16
|
syl2anc |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( ( A .o D ) +o E ) e. On ) |
18 |
|
eloni |
|- ( ( ( A .o D ) +o E ) e. On -> Ord ( ( A .o D ) +o E ) ) |
19 |
|
ordirr |
|- ( Ord ( ( A .o D ) +o E ) -> -. ( ( A .o D ) +o E ) e. ( ( A .o D ) +o E ) ) |
20 |
17 18 19
|
3syl |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> -. ( ( A .o D ) +o E ) e. ( ( A .o D ) +o E ) ) |
21 |
9 20
|
eqneltrd |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> -. ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) |
22 |
|
orc |
|- ( B e. D -> ( B e. D \/ ( B = D /\ C e. E ) ) ) |
23 |
|
omeulem2 |
|- ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( B e. D \/ ( B = D /\ C e. E ) ) -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) ) |
24 |
23
|
adantr |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( ( B e. D \/ ( B = D /\ C e. E ) ) -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) ) |
25 |
22 24
|
syl5 |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( B e. D -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) ) |
26 |
21 25
|
mtod |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> -. B e. D ) |
27 |
26
|
pm2.21d |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( B e. D -> B = D ) ) |
28 |
|
idd |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( B = D -> B = D ) ) |
29 |
20 9
|
neleqtrrd |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> -. ( ( A .o D ) +o E ) e. ( ( A .o B ) +o C ) ) |
30 |
|
orc |
|- ( D e. B -> ( D e. B \/ ( D = B /\ E e. C ) ) ) |
31 |
|
simpl1r |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> A =/= (/) ) |
32 |
|
simpl2r |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> C e. A ) |
33 |
|
omeulem2 |
|- ( ( ( A e. On /\ A =/= (/) ) /\ ( D e. On /\ E e. A ) /\ ( B e. On /\ C e. A ) ) -> ( ( D e. B \/ ( D = B /\ E e. C ) ) -> ( ( A .o D ) +o E ) e. ( ( A .o B ) +o C ) ) ) |
34 |
10 31 4 13 1 32 33
|
syl222anc |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( ( D e. B \/ ( D = B /\ E e. C ) ) -> ( ( A .o D ) +o E ) e. ( ( A .o B ) +o C ) ) ) |
35 |
30 34
|
syl5 |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( D e. B -> ( ( A .o D ) +o E ) e. ( ( A .o B ) +o C ) ) ) |
36 |
29 35
|
mtod |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> -. D e. B ) |
37 |
36
|
pm2.21d |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( D e. B -> B = D ) ) |
38 |
27 28 37
|
3jaod |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( ( B e. D \/ B = D \/ D e. B ) -> B = D ) ) |
39 |
8 38
|
mpd |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> B = D ) |
40 |
|
onelon |
|- ( ( A e. On /\ C e. A ) -> C e. On ) |
41 |
|
eloni |
|- ( C e. On -> Ord C ) |
42 |
40 41
|
syl |
|- ( ( A e. On /\ C e. A ) -> Ord C ) |
43 |
10 32 42
|
syl2anc |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> Ord C ) |
44 |
|
eloni |
|- ( E e. On -> Ord E ) |
45 |
14 44
|
syl |
|- ( ( A e. On /\ E e. A ) -> Ord E ) |
46 |
10 13 45
|
syl2anc |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> Ord E ) |
47 |
|
ordtri3or |
|- ( ( Ord C /\ Ord E ) -> ( C e. E \/ C = E \/ E e. C ) ) |
48 |
43 46 47
|
syl2anc |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( C e. E \/ C = E \/ E e. C ) ) |
49 |
|
olc |
|- ( ( B = D /\ C e. E ) -> ( B e. D \/ ( B = D /\ C e. E ) ) ) |
50 |
49 24
|
syl5 |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( ( B = D /\ C e. E ) -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) ) |
51 |
39 50
|
mpand |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( C e. E -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) ) |
52 |
21 51
|
mtod |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> -. C e. E ) |
53 |
52
|
pm2.21d |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( C e. E -> C = E ) ) |
54 |
|
idd |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( C = E -> C = E ) ) |
55 |
39
|
eqcomd |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> D = B ) |
56 |
|
olc |
|- ( ( D = B /\ E e. C ) -> ( D e. B \/ ( D = B /\ E e. C ) ) ) |
57 |
56 34
|
syl5 |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( ( D = B /\ E e. C ) -> ( ( A .o D ) +o E ) e. ( ( A .o B ) +o C ) ) ) |
58 |
55 57
|
mpand |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( E e. C -> ( ( A .o D ) +o E ) e. ( ( A .o B ) +o C ) ) ) |
59 |
29 58
|
mtod |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> -. E e. C ) |
60 |
59
|
pm2.21d |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( E e. C -> C = E ) ) |
61 |
53 54 60
|
3jaod |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( ( C e. E \/ C = E \/ E e. C ) -> C = E ) ) |
62 |
48 61
|
mpd |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> C = E ) |
63 |
39 62
|
jca |
|- ( ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) /\ ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) -> ( B = D /\ C = E ) ) |
64 |
63
|
ex |
|- ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) -> ( B = D /\ C = E ) ) ) |
65 |
|
oveq2 |
|- ( B = D -> ( A .o B ) = ( A .o D ) ) |
66 |
|
id |
|- ( C = E -> C = E ) |
67 |
65 66
|
oveqan12d |
|- ( ( B = D /\ C = E ) -> ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) ) |
68 |
64 67
|
impbid1 |
|- ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) <-> ( B = D /\ C = E ) ) ) |