Metamath Proof Explorer

Theorem ltnadd

Description: Condition for bounding a natural sum below. (Contributed by Scott Fenton, 21-Jul-2026)

Ref Expression
Assertion ltnadd 
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. ( B +no C ) <-> ( E. b e. B A C_ ( b +no C ) \/ E. c e. C A C_ ( B +no c ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( x = A -> ( ( B +no c ) e. x <-> ( B +no c ) e. A ) )
2 1 ralbidv 
 |-  ( x = A -> ( A. c e. C ( B +no c ) e. x <-> A. c e. C ( B +no c ) e. A ) )
3 eleq2 
 |-  ( x = A -> ( ( b +no C ) e. x <-> ( b +no C ) e. A ) )
4 3 ralbidv 
 |-  ( x = A -> ( A. b e. B ( b +no C ) e. x <-> A. b e. B ( b +no C ) e. A ) )
5 2 4 anbi12d 
 |-  ( x = A -> ( ( A. c e. C ( B +no c ) e. x /\ A. b e. B ( b +no C ) e. x ) <-> ( A. c e. C ( B +no c ) e. A /\ A. b e. B ( b +no C ) e. A ) ) )
6 5 onnminsb 
 |-  ( A e. On -> ( A e. |^| { x e. On | ( A. c e. C ( B +no c ) e. x /\ A. b e. B ( b +no C ) e. x ) } -> -. ( A. c e. C ( B +no c ) e. A /\ A. b e. B ( b +no C ) e. A ) ) )
7 6 3ad2ant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. |^| { x e. On | ( A. c e. C ( B +no c ) e. x /\ A. b e. B ( b +no C ) e. x ) } -> -. ( A. c e. C ( B +no c ) e. A /\ A. b e. B ( b +no C ) e. A ) ) )
8 naddov2 
 |-  ( ( B e. On /\ C e. On ) -> ( B +no C ) = |^| { x e. On | ( A. c e. C ( B +no c ) e. x /\ A. b e. B ( b +no C ) e. x ) } )
9 8 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) = |^| { x e. On | ( A. c e. C ( B +no c ) e. x /\ A. b e. B ( b +no C ) e. x ) } )
10 9 eleq2d 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. ( B +no C ) <-> A e. |^| { x e. On | ( A. c e. C ( B +no c ) e. x /\ A. b e. B ( b +no C ) e. x ) } ) )
11 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ b e. B ) -> A e. On )
12 onss 
 |-  ( B e. On -> B C_ On )
13 12 3ad2ant2 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> B C_ On )
14 13 sselda 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ b e. B ) -> b e. On )
15 simpl3 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ b e. B ) -> C e. On )
16 14 15 naddcld 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ b e. B ) -> ( b +no C ) e. On )
17 ontri1 
 |-  ( ( A e. On /\ ( b +no C ) e. On ) -> ( A C_ ( b +no C ) <-> -. ( b +no C ) e. A ) )
18 11 16 17 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ b e. B ) -> ( A C_ ( b +no C ) <-> -. ( b +no C ) e. A ) )
19 18 rexbidva 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. b e. B A C_ ( b +no C ) <-> E. b e. B -. ( b +no C ) e. A ) )
20 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ c e. C ) -> A e. On )
21 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ c e. C ) -> B e. On )
22 onss 
 |-  ( C e. On -> C C_ On )
23 22 3ad2ant3 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> C C_ On )
24 23 sselda 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ c e. C ) -> c e. On )
25 21 24 naddcld 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ c e. C ) -> ( B +no c ) e. On )
26 ontri1 
 |-  ( ( A e. On /\ ( B +no c ) e. On ) -> ( A C_ ( B +no c ) <-> -. ( B +no c ) e. A ) )
27 20 25 26 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ c e. C ) -> ( A C_ ( B +no c ) <-> -. ( B +no c ) e. A ) )
28 27 rexbidva 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. c e. C A C_ ( B +no c ) <-> E. c e. C -. ( B +no c ) e. A ) )
29 19 28 orbi12d 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( E. b e. B A C_ ( b +no C ) \/ E. c e. C A C_ ( B +no c ) ) <-> ( E. b e. B -. ( b +no C ) e. A \/ E. c e. C -. ( B +no c ) e. A ) ) )
30 orcom 
 |-  ( ( -. A. b e. B ( b +no C ) e. A \/ -. A. c e. C ( B +no c ) e. A ) <-> ( -. A. c e. C ( B +no c ) e. A \/ -. A. b e. B ( b +no C ) e. A ) )
31 rexnal 
 |-  ( E. b e. B -. ( b +no C ) e. A <-> -. A. b e. B ( b +no C ) e. A )
32 rexnal 
 |-  ( E. c e. C -. ( B +no c ) e. A <-> -. A. c e. C ( B +no c ) e. A )
33 31 32 orbi12i 
 |-  ( ( E. b e. B -. ( b +no C ) e. A \/ E. c e. C -. ( B +no c ) e. A ) <-> ( -. A. b e. B ( b +no C ) e. A \/ -. A. c e. C ( B +no c ) e. A ) )
34 ianor 
 |-  ( -. ( A. c e. C ( B +no c ) e. A /\ A. b e. B ( b +no C ) e. A ) <-> ( -. A. c e. C ( B +no c ) e. A \/ -. A. b e. B ( b +no C ) e. A ) )
35 30 33 34 3bitr4i 
 |-  ( ( E. b e. B -. ( b +no C ) e. A \/ E. c e. C -. ( B +no c ) e. A ) <-> -. ( A. c e. C ( B +no c ) e. A /\ A. b e. B ( b +no C ) e. A ) )
36 29 35 bitrdi 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( E. b e. B A C_ ( b +no C ) \/ E. c e. C A C_ ( B +no c ) ) <-> -. ( A. c e. C ( B +no c ) e. A /\ A. b e. B ( b +no C ) e. A ) ) )
37 7 10 36 3imtr4d 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. ( B +no C ) -> ( E. b e. B A C_ ( b +no C ) \/ E. c e. C A C_ ( B +no c ) ) ) )
38 simprr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> A C_ ( b +no C ) )
39 simprl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> b e. B )
40 14 adantrr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> b e. On )
41 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> B e. On )
42 simpl3 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> C e. On )
43 naddel1 
 |-  ( ( b e. On /\ B e. On /\ C e. On ) -> ( b e. B <-> ( b +no C ) e. ( B +no C ) ) )
44 40 41 42 43 syl3anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> ( b e. B <-> ( b +no C ) e. ( B +no C ) ) )
45 39 44 mpbid 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> ( b +no C ) e. ( B +no C ) )
46 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> A e. On )
47 naddcl 
 |-  ( ( B e. On /\ C e. On ) -> ( B +no C ) e. On )
48 47 3adant1 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) e. On )
49 48 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> ( B +no C ) e. On )
50 ontr2 
 |-  ( ( A e. On /\ ( B +no C ) e. On ) -> ( ( A C_ ( b +no C ) /\ ( b +no C ) e. ( B +no C ) ) -> A e. ( B +no C ) ) )
51 46 49 50 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> ( ( A C_ ( b +no C ) /\ ( b +no C ) e. ( B +no C ) ) -> A e. ( B +no C ) ) )
52 38 45 51 mp2and 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( b e. B /\ A C_ ( b +no C ) ) ) -> A e. ( B +no C ) )
53 52 rexlimdvaa 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. b e. B A C_ ( b +no C ) -> A e. ( B +no C ) ) )
54 simprr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> A C_ ( B +no c ) )
55 simprl 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> c e. C )
56 24 adantrr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> c e. On )
57 simpl3 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> C e. On )
58 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> B e. On )
59 naddel2 
 |-  ( ( c e. On /\ C e. On /\ B e. On ) -> ( c e. C <-> ( B +no c ) e. ( B +no C ) ) )
60 56 57 58 59 syl3anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> ( c e. C <-> ( B +no c ) e. ( B +no C ) ) )
61 55 60 mpbid 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> ( B +no c ) e. ( B +no C ) )
62 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> A e. On )
63 48 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> ( B +no C ) e. On )
64 ontr2 
 |-  ( ( A e. On /\ ( B +no C ) e. On ) -> ( ( A C_ ( B +no c ) /\ ( B +no c ) e. ( B +no C ) ) -> A e. ( B +no C ) ) )
65 62 63 64 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> ( ( A C_ ( B +no c ) /\ ( B +no c ) e. ( B +no C ) ) -> A e. ( B +no C ) ) )
66 54 61 65 mp2and 
 |-  ( ( ( A e. On /\ B e. On /\ C e. On ) /\ ( c e. C /\ A C_ ( B +no c ) ) ) -> A e. ( B +no C ) )
67 66 rexlimdvaa 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. c e. C A C_ ( B +no c ) -> A e. ( B +no C ) ) )
68 53 67 jaod 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( E. b e. B A C_ ( b +no C ) \/ E. c e. C A C_ ( B +no c ) ) -> A e. ( B +no C ) ) )
69 37 68 impbid 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. ( B +no C ) <-> ( E. b e. B A C_ ( b +no C ) \/ E. c e. C A C_ ( B +no c ) ) ) )