Metamath Proof Explorer

Theorem omeulem2

Description: Lemma for omeu : uniqueness part. (Contributed by Mario Carneiro, 28-Feb-2013) (Revised by Mario Carneiro, 29-May-2015)

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

Proof

Step Hyp Ref Expression
1 simp3l 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> D e. On )
2 eloni 
 |-  ( D e. On -> Ord D )
3 ordsucss 
 |-  ( Ord D -> ( B e. D -> suc B C_ D ) )
4 1 2 3 3syl 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( B e. D -> suc B C_ D ) )
5 simp2l 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> B e. On )
6 onsuc 
 |-  ( B e. On -> suc B e. On )
7 5 6 syl 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> suc B e. On )
8 simp1l 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> A e. On )
9 simp1r 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> A =/= (/) )
10 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
11 8 10 syl 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( (/) e. A <-> A =/= (/) ) )
12 9 11 mpbird 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> (/) e. A )
13 omword 
 |-  ( ( ( suc B e. On /\ D e. On /\ A e. On ) /\ (/) e. A ) -> ( suc B C_ D <-> ( A .o suc B ) C_ ( A .o D ) ) )
14 7 1 8 12 13 syl31anc 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( suc B C_ D <-> ( A .o suc B ) C_ ( A .o D ) ) )
15 4 14 sylibd 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( B e. D -> ( A .o suc B ) C_ ( A .o D ) ) )
16 omcl 
 |-  ( ( A e. On /\ D e. On ) -> ( A .o D ) e. On )
17 8 1 16 syl2anc 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( A .o D ) e. On )
18 simp3r 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> E e. A )
19 onelon 
 |-  ( ( A e. On /\ E e. A ) -> E e. On )
20 8 18 19 syl2anc 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> E e. On )
21 oaword1 
 |-  ( ( ( A .o D ) e. On /\ E e. On ) -> ( A .o D ) C_ ( ( A .o D ) +o E ) )
22 sstr 
 |-  ( ( ( A .o suc B ) C_ ( A .o D ) /\ ( A .o D ) C_ ( ( A .o D ) +o E ) ) -> ( A .o suc B ) C_ ( ( A .o D ) +o E ) )
23 22 expcom 
 |-  ( ( A .o D ) C_ ( ( A .o D ) +o E ) -> ( ( A .o suc B ) C_ ( A .o D ) -> ( A .o suc B ) C_ ( ( A .o D ) +o E ) ) )
24 21 23 syl 
 |-  ( ( ( A .o D ) e. On /\ E e. On ) -> ( ( A .o suc B ) C_ ( A .o D ) -> ( A .o suc B ) C_ ( ( A .o D ) +o E ) ) )
25 17 20 24 syl2anc 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( A .o suc B ) C_ ( A .o D ) -> ( A .o suc B ) C_ ( ( A .o D ) +o E ) ) )
26 15 25 syld 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( B e. D -> ( A .o suc B ) C_ ( ( A .o D ) +o E ) ) )
27 simp2r 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> C e. A )
28 onelon 
 |-  ( ( A e. On /\ C e. A ) -> C e. On )
29 8 27 28 syl2anc 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> C e. On )
30 omcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
31 8 5 30 syl2anc 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( A .o B ) e. On )
32 oaord 
 |-  ( ( C e. On /\ A e. On /\ ( A .o B ) e. On ) -> ( C e. A <-> ( ( A .o B ) +o C ) e. ( ( A .o B ) +o A ) ) )
33 32 biimpa 
 |-  ( ( ( C e. On /\ A e. On /\ ( A .o B ) e. On ) /\ C e. A ) -> ( ( A .o B ) +o C ) e. ( ( A .o B ) +o A ) )
34 29 8 31 27 33 syl31anc 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( A .o B ) +o C ) e. ( ( A .o B ) +o A ) )
35 omsuc 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
36 8 5 35 syl2anc 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
37 34 36 eleqtrrd 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( A .o B ) +o C ) e. ( A .o suc B ) )
38 ssel 
 |-  ( ( A .o suc B ) C_ ( ( A .o D ) +o E ) -> ( ( ( A .o B ) +o C ) e. ( A .o suc B ) -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) )
39 26 37 38 syl6ci 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( B e. D -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) )
40 simpr 
 |-  ( ( B = D /\ C e. E ) -> C e. E )
41 oaord 
 |-  ( ( C e. On /\ E e. On /\ ( A .o B ) e. On ) -> ( C e. E <-> ( ( A .o B ) +o C ) e. ( ( A .o B ) +o E ) ) )
42 40 41 imbitrid 
 |-  ( ( C e. On /\ E e. On /\ ( A .o B ) e. On ) -> ( ( B = D /\ C e. E ) -> ( ( A .o B ) +o C ) e. ( ( A .o B ) +o E ) ) )
43 oveq2 
 |-  ( B = D -> ( A .o B ) = ( A .o D ) )
44 43 oveq1d 
 |-  ( B = D -> ( ( A .o B ) +o E ) = ( ( A .o D ) +o E ) )
45 44 adantr 
 |-  ( ( B = D /\ C e. E ) -> ( ( A .o B ) +o E ) = ( ( A .o D ) +o E ) )
46 45 eleq2d 
 |-  ( ( B = D /\ C e. E ) -> ( ( ( A .o B ) +o C ) e. ( ( A .o B ) +o E ) <-> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) )
47 42 46 mpbidi 
 |-  ( ( C e. On /\ E e. On /\ ( A .o B ) e. On ) -> ( ( B = D /\ C e. E ) -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) )
48 29 20 31 47 syl3anc 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( B = D /\ C e. E ) -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) )
49 39 48 jaod 
 |-  ( ( ( 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 ) ) )