Metamath Proof Explorer

Theorem naddssim

Description: Ordinal less-than-or-equal is preserved by natural addition. (Contributed by Scott Fenton, 7-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( c = d -> ( A +no c ) = ( A +no d ) )
2 oveq2 
 |-  ( c = d -> ( B +no c ) = ( B +no d ) )
3 1 2 sseq12d 
 |-  ( c = d -> ( ( A +no c ) C_ ( B +no c ) <-> ( A +no d ) C_ ( B +no d ) ) )
4 3 imbi2d 
 |-  ( c = d -> ( ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) <-> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) )
5 4 imbi2d 
 |-  ( c = d -> ( ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) ) )
6 oveq2 
 |-  ( c = C -> ( A +no c ) = ( A +no C ) )
7 oveq2 
 |-  ( c = C -> ( B +no c ) = ( B +no C ) )
8 6 7 sseq12d 
 |-  ( c = C -> ( ( A +no c ) C_ ( B +no c ) <-> ( A +no C ) C_ ( B +no C ) ) )
9 8 imbi2d 
 |-  ( c = C -> ( ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) <-> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) )
10 9 imbi2d 
 |-  ( c = C -> ( ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) ) )
11 r19.21v 
 |-  ( A. d e. c ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) <-> ( ( A e. On /\ B e. On ) -> A. d e. c ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) )
12 r19.21v 
 |-  ( A. d e. c ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) <-> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) )
13 12 imbi2i 
 |-  ( ( ( A e. On /\ B e. On ) -> A. d e. c ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) )
14 11 13 bitri 
 |-  ( A. d e. c ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) <-> ( ( A e. On /\ B e. On ) -> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) )
15 oveq2 
 |-  ( d = w -> ( A +no d ) = ( A +no w ) )
16 oveq2 
 |-  ( d = w -> ( B +no d ) = ( B +no w ) )
17 15 16 sseq12d 
 |-  ( d = w -> ( ( A +no d ) C_ ( B +no d ) <-> ( A +no w ) C_ ( B +no w ) ) )
18 17 rspccva 
 |-  ( ( A. d e. c ( A +no d ) C_ ( B +no d ) /\ w e. c ) -> ( A +no w ) C_ ( B +no w ) )
19 18 ad4ant24 
 |-  ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( A +no w ) C_ ( B +no w ) )
20 simprrl 
 |-  ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. y e. c ( B +no y ) e. x )
21 oveq2 
 |-  ( y = w -> ( B +no y ) = ( B +no w ) )
22 21 eleq1d 
 |-  ( y = w -> ( ( B +no y ) e. x <-> ( B +no w ) e. x ) )
23 22 rspccva 
 |-  ( ( A. y e. c ( B +no y ) e. x /\ w e. c ) -> ( B +no w ) e. x )
24 20 23 sylan 
 |-  ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( B +no w ) e. x )
25 simplrl 
 |-  ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) -> A e. On )
26 25 adantr 
 |-  ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> A e. On )
27 26 adantr 
 |-  ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A e. On )
28 27 adantr 
 |-  ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> A e. On )
29 simp-4l 
 |-  ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> c e. On )
30 onelon 
 |-  ( ( c e. On /\ w e. c ) -> w e. On )
31 29 30 sylan 
 |-  ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> w e. On )
32 naddcl 
 |-  ( ( A e. On /\ w e. On ) -> ( A +no w ) e. On )
33 28 31 32 syl2anc 
 |-  ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( A +no w ) e. On )
34 simplrl 
 |-  ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> x e. On )
35 ontr2 
 |-  ( ( ( A +no w ) e. On /\ x e. On ) -> ( ( ( A +no w ) C_ ( B +no w ) /\ ( B +no w ) e. x ) -> ( A +no w ) e. x ) )
36 33 34 35 syl2anc 
 |-  ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( ( ( A +no w ) C_ ( B +no w ) /\ ( B +no w ) e. x ) -> ( A +no w ) e. x ) )
37 19 24 36 mp2and 
 |-  ( ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) /\ w e. c ) -> ( A +no w ) e. x )
38 37 ralrimiva 
 |-  ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. w e. c ( A +no w ) e. x )
39 simpllr 
 |-  ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A C_ B )
40 simprrr 
 |-  ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. z e. B ( z +no c ) e. x )
41 ssralv 
 |-  ( A C_ B -> ( A. z e. B ( z +no c ) e. x -> A. z e. A ( z +no c ) e. x ) )
42 39 40 41 sylc 
 |-  ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> A. z e. A ( z +no c ) e. x )
43 38 42 jca 
 |-  ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ ( x e. On /\ ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) ) ) -> ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) )
44 43 expr 
 |-  ( ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) /\ x e. On ) -> ( ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) -> ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) ) )
45 44 ss2rabdv 
 |-  ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } C_ { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } )
46 intss 
 |-  ( { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } C_ { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } -> |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } C_ |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } )
47 45 46 syl 
 |-  ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } C_ |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } )
48 simplll 
 |-  ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> c e. On )
49 naddov2 
 |-  ( ( A e. On /\ c e. On ) -> ( A +no c ) = |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } )
50 26 48 49 syl2anc 
 |-  ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A +no c ) = |^| { x e. On | ( A. w e. c ( A +no w ) e. x /\ A. z e. A ( z +no c ) e. x ) } )
51 simplrr 
 |-  ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) -> B e. On )
52 51 adantr 
 |-  ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> B e. On )
53 naddov2 
 |-  ( ( B e. On /\ c e. On ) -> ( B +no c ) = |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } )
54 52 48 53 syl2anc 
 |-  ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( B +no c ) = |^| { x e. On | ( A. y e. c ( B +no y ) e. x /\ A. z e. B ( z +no c ) e. x ) } )
55 47 50 54 3sstr4d 
 |-  ( ( ( ( c e. On /\ ( A e. On /\ B e. On ) ) /\ A C_ B ) /\ A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A +no c ) C_ ( B +no c ) )
56 55 exp31 
 |-  ( ( c e. On /\ ( A e. On /\ B e. On ) ) -> ( A C_ B -> ( A. d e. c ( A +no d ) C_ ( B +no d ) -> ( A +no c ) C_ ( B +no c ) ) ) )
57 56 a2d 
 |-  ( ( c e. On /\ ( A e. On /\ B e. On ) ) -> ( ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) )
58 57 ex 
 |-  ( c e. On -> ( ( A e. On /\ B e. On ) -> ( ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) )
59 58 a2d 
 |-  ( c e. On -> ( ( ( A e. On /\ B e. On ) -> ( A C_ B -> A. d e. c ( A +no d ) C_ ( B +no d ) ) ) -> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) )
60 14 59 syl5bi 
 |-  ( c e. On -> ( A. d e. c ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no d ) C_ ( B +no d ) ) ) -> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no c ) C_ ( B +no c ) ) ) ) )
61 5 10 60 tfis3 
 |-  ( C e. On -> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) )
62 61 com12 
 |-  ( ( A e. On /\ B e. On ) -> ( C e. On -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) ) )
63 62 3impia 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( A +no C ) C_ ( B +no C ) ) )