Metamath Proof Explorer

Theorem naddgeoa

Description: Natural addition results in a value greater than or equal than that of ordinal addition. (Contributed by RP, 1-Jan-2025)

Ref Expression
Assertion naddgeoa 
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) C_ ( A +no B ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = c -> ( a +o b ) = ( c +o b ) )
2 oveq1 
 |-  ( a = c -> ( a +no b ) = ( c +no b ) )
3 1 2 sseq12d 
 |-  ( a = c -> ( ( a +o b ) C_ ( a +no b ) <-> ( c +o b ) C_ ( c +no b ) ) )
4 oveq2 
 |-  ( b = d -> ( c +o b ) = ( c +o d ) )
5 oveq2 
 |-  ( b = d -> ( c +no b ) = ( c +no d ) )
6 4 5 sseq12d 
 |-  ( b = d -> ( ( c +o b ) C_ ( c +no b ) <-> ( c +o d ) C_ ( c +no d ) ) )
7 oveq1 
 |-  ( a = c -> ( a +o d ) = ( c +o d ) )
8 oveq1 
 |-  ( a = c -> ( a +no d ) = ( c +no d ) )
9 7 8 sseq12d 
 |-  ( a = c -> ( ( a +o d ) C_ ( a +no d ) <-> ( c +o d ) C_ ( c +no d ) ) )
10 oveq1 
 |-  ( a = A -> ( a +o b ) = ( A +o b ) )
11 oveq1 
 |-  ( a = A -> ( a +no b ) = ( A +no b ) )
12 10 11 sseq12d 
 |-  ( a = A -> ( ( a +o b ) C_ ( a +no b ) <-> ( A +o b ) C_ ( A +no b ) ) )
13 oveq2 
 |-  ( b = B -> ( A +o b ) = ( A +o B ) )
14 oveq2 
 |-  ( b = B -> ( A +no b ) = ( A +no B ) )
15 13 14 sseq12d 
 |-  ( b = B -> ( ( A +o b ) C_ ( A +no b ) <-> ( A +o B ) C_ ( A +no B ) ) )
16 simplll 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> a e. On )
17 simpllr 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> b e. On )
18 simplr 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> Lim b )
19 17 18 jca 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> ( b e. On /\ Lim b ) )
20 oalim 
 |-  ( ( a e. On /\ ( b e. On /\ Lim b ) ) -> ( a +o b ) = U_ d e. b ( a +o d ) )
21 16 19 20 syl2anc 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) = U_ d e. b ( a +o d ) )
22 simpl 
 |-  ( ( ( a e. On /\ b e. On ) /\ Lim b ) -> ( a e. On /\ b e. On ) )
23 simp3 
 |-  ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> A. d e. b ( a +o d ) C_ ( a +no d ) )
24 simpr 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +o d ) C_ ( a +no d ) )
25 simpr 
 |-  ( ( a e. On /\ b e. On ) -> b e. On )
26 onelss 
 |-  ( b e. On -> ( d e. b -> d C_ b ) )
27 25 26 syl 
 |-  ( ( a e. On /\ b e. On ) -> ( d e. b -> d C_ b ) )
28 27 imp 
 |-  ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> d C_ b )
29 simplr 
 |-  ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> b e. On )
30 simpr 
 |-  ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> d e. b )
31 onelon 
 |-  ( ( b e. On /\ d e. b ) -> d e. On )
32 29 30 31 syl2anc 
 |-  ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> d e. On )
33 simpll 
 |-  ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> a e. On )
34 naddss2 
 |-  ( ( d e. On /\ b e. On /\ a e. On ) -> ( d C_ b <-> ( a +no d ) C_ ( a +no b ) ) )
35 32 29 33 34 syl3anc 
 |-  ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( d C_ b <-> ( a +no d ) C_ ( a +no b ) ) )
36 28 35 mpbid 
 |-  ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( a +no d ) C_ ( a +no b ) )
37 36 adantr 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +no d ) C_ ( a +no b ) )
38 24 37 sstrd 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +o d ) C_ ( a +no b ) )
39 38 ex 
 |-  ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( ( a +o d ) C_ ( a +no d ) -> ( a +o d ) C_ ( a +no b ) ) )
40 39 ralimdva 
 |-  ( ( a e. On /\ b e. On ) -> ( A. d e. b ( a +o d ) C_ ( a +no d ) -> A. d e. b ( a +o d ) C_ ( a +no b ) ) )
41 40 imp 
 |-  ( ( ( a e. On /\ b e. On ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> A. d e. b ( a +o d ) C_ ( a +no b ) )
42 iunss 
 |-  ( U_ d e. b ( a +o d ) C_ ( a +no b ) <-> A. d e. b ( a +o d ) C_ ( a +no b ) )
43 41 42 sylibr 
 |-  ( ( ( a e. On /\ b e. On ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> U_ d e. b ( a +o d ) C_ ( a +no b ) )
44 22 23 43 syl2an 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> U_ d e. b ( a +o d ) C_ ( a +no b ) )
45 21 44 eqsstrd 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) C_ ( a +no b ) )
46 45 exp31 
 |-  ( ( a e. On /\ b e. On ) -> ( Lim b -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) )
47 dflim3 
 |-  ( Lim b <-> ( Ord b /\ -. ( b = (/) \/ E. d e. On b = suc d ) ) )
48 47 notbii 
 |-  ( -. Lim b <-> -. ( Ord b /\ -. ( b = (/) \/ E. d e. On b = suc d ) ) )
49 iman 
 |-  ( ( Ord b -> ( b = (/) \/ E. d e. On b = suc d ) ) <-> -. ( Ord b /\ -. ( b = (/) \/ E. d e. On b = suc d ) ) )
50 48 49 bitr4i 
 |-  ( -. Lim b <-> ( Ord b -> ( b = (/) \/ E. d e. On b = suc d ) ) )
51 eloni 
 |-  ( b e. On -> Ord b )
52 pm5.5 
 |-  ( Ord b -> ( ( Ord b -> ( b = (/) \/ E. d e. On b = suc d ) ) <-> ( b = (/) \/ E. d e. On b = suc d ) ) )
53 25 51 52 3syl 
 |-  ( ( a e. On /\ b e. On ) -> ( ( Ord b -> ( b = (/) \/ E. d e. On b = suc d ) ) <-> ( b = (/) \/ E. d e. On b = suc d ) ) )
54 50 53 bitrid 
 |-  ( ( a e. On /\ b e. On ) -> ( -. Lim b <-> ( b = (/) \/ E. d e. On b = suc d ) ) )
55 ssidd 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> a C_ a )
56 simpr 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> b = (/) )
57 56 oveq2d 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +o b ) = ( a +o (/) ) )
58 simpll 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> a e. On )
59 oa0 
 |-  ( a e. On -> ( a +o (/) ) = a )
60 58 59 syl 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +o (/) ) = a )
61 57 60 eqtrd 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +o b ) = a )
62 56 oveq2d 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +no b ) = ( a +no (/) ) )
63 naddrid 
 |-  ( a e. On -> ( a +no (/) ) = a )
64 58 63 syl 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +no (/) ) = a )
65 62 64 eqtrd 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +no b ) = a )
66 55 61 65 3sstr4d 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +o b ) C_ ( a +no b ) )
67 66 a1d 
 |-  ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) )
68 67 ex 
 |-  ( ( a e. On /\ b e. On ) -> ( b = (/) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) )
69 vex 
 |-  d e. _V
70 69 sucid 
 |-  d e. suc d
71 simpr 
 |-  ( ( d e. On /\ b = suc d ) -> b = suc d )
72 70 71 eleqtrrid 
 |-  ( ( d e. On /\ b = suc d ) -> d e. b )
73 72 71 jca 
 |-  ( ( d e. On /\ b = suc d ) -> ( d e. b /\ b = suc d ) )
74 73 a1i 
 |-  ( ( a e. On /\ b e. On ) -> ( ( d e. On /\ b = suc d ) -> ( d e. b /\ b = suc d ) ) )
75 74 reximdv2 
 |-  ( ( a e. On /\ b e. On ) -> ( E. d e. On b = suc d -> E. d e. b b = suc d ) )
76 r19.29r 
 |-  ( ( E. d e. b b = suc d /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> E. d e. b ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) )
77 simprr 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o d ) C_ ( a +no d ) )
78 33 32 jca 
 |-  ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( a e. On /\ d e. On ) )
79 oacl 
 |-  ( ( a e. On /\ d e. On ) -> ( a +o d ) e. On )
80 eloni 
 |-  ( ( a +o d ) e. On -> Ord ( a +o d ) )
81 79 80 syl 
 |-  ( ( a e. On /\ d e. On ) -> Ord ( a +o d ) )
82 naddcl 
 |-  ( ( a e. On /\ d e. On ) -> ( a +no d ) e. On )
83 eloni 
 |-  ( ( a +no d ) e. On -> Ord ( a +no d ) )
84 82 83 syl 
 |-  ( ( a e. On /\ d e. On ) -> Ord ( a +no d ) )
85 81 84 jca 
 |-  ( ( a e. On /\ d e. On ) -> ( Ord ( a +o d ) /\ Ord ( a +no d ) ) )
86 ordsucsssuc 
 |-  ( ( Ord ( a +o d ) /\ Ord ( a +no d ) ) -> ( ( a +o d ) C_ ( a +no d ) <-> suc ( a +o d ) C_ suc ( a +no d ) ) )
87 78 85 86 3syl 
 |-  ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( ( a +o d ) C_ ( a +no d ) <-> suc ( a +o d ) C_ suc ( a +no d ) ) )
88 87 adantr 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( ( a +o d ) C_ ( a +no d ) <-> suc ( a +o d ) C_ suc ( a +no d ) ) )
89 77 88 mpbid 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> suc ( a +o d ) C_ suc ( a +no d ) )
90 simprl 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> b = suc d )
91 90 oveq2d 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) = ( a +o suc d ) )
92 78 adantr 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a e. On /\ d e. On ) )
93 oasuc 
 |-  ( ( a e. On /\ d e. On ) -> ( a +o suc d ) = suc ( a +o d ) )
94 92 93 syl 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o suc d ) = suc ( a +o d ) )
95 91 94 eqtrd 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) = suc ( a +o d ) )
96 90 oveq2d 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +no b ) = ( a +no suc d ) )
97 simplll 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> a e. On )
98 31 ad4ant23 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> d e. On )
99 naddsuc2 
 |-  ( ( a e. On /\ d e. On ) -> ( a +no suc d ) = suc ( a +no d ) )
100 97 98 99 syl2anc 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +no suc d ) = suc ( a +no d ) )
101 96 100 eqtrd 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +no b ) = suc ( a +no d ) )
102 89 95 101 3sstr4d 
 |-  ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) C_ ( a +no b ) )
103 102 rexlimdva2 
 |-  ( ( a e. On /\ b e. On ) -> ( E. d e. b ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) )
104 76 103 syl5 
 |-  ( ( a e. On /\ b e. On ) -> ( ( E. d e. b b = suc d /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) )
105 104 expd 
 |-  ( ( a e. On /\ b e. On ) -> ( E. d e. b b = suc d -> ( A. d e. b ( a +o d ) C_ ( a +no d ) -> ( a +o b ) C_ ( a +no b ) ) ) )
106 23 105 syl7 
 |-  ( ( a e. On /\ b e. On ) -> ( E. d e. b b = suc d -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) )
107 75 106 syld 
 |-  ( ( a e. On /\ b e. On ) -> ( E. d e. On b = suc d -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) )
108 68 107 jaod 
 |-  ( ( a e. On /\ b e. On ) -> ( ( b = (/) \/ E. d e. On b = suc d ) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) )
109 54 108 sylbid 
 |-  ( ( a e. On /\ b e. On ) -> ( -. Lim b -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) )
110 46 109 pm2.61d 
 |-  ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) )
111 3 6 9 12 15 110 on2ind 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) C_ ( A +no B ) )