Metamath Proof Explorer


Theorem omopth2

Description: An ordered pair-like theorem for ordinal multiplication. (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion omopth2
|- ( ( ( 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 ) ) )

Proof

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 ) ) )