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