Theorem naddle

Description: Condition for bounding natural addition above. (Contributed by Scott Fenton, 21-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ltnadd	|- ( ( C e. On /\ A e. On /\ B e. On ) -> ( C e. ( A +no B ) <-> ( E. a e. A C C_ ( a +no B ) \/ E. b e. B C C_ ( A +no b ) ) ) )
2	1	3coml	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( C e. ( A +no B ) <-> ( E. a e. A C C_ ( a +no B ) \/ E. b e. B C C_ ( A +no b ) ) ) )
3	2	notbid	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. C e. ( A +no B ) <-> -. ( E. a e. A C C_ ( a +no B ) \/ E. b e. B C C_ ( A +no b ) ) ) )
4		naddcl	|- ( ( A e. On /\ B e. On ) -> ( A +no B ) e. On )
5	4	3adant3	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no B ) e. On )
6		simp3	|- ( ( A e. On /\ B e. On /\ C e. On ) -> C e. On )
7		ontri1	|- ( ( ( A +no B ) e. On /\ C e. On ) -> ( ( A +no B ) C_ C <-> -. C e. ( A +no B ) ) )
8	5 6 7	syl2anc	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) C_ C <-> -. C e. ( A +no B ) ) )
9		simpl3	|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ a e. A ) -> C e. On )
10		onss	|- ( A e. On -> A C_ On )
11	10	3ad2ant1	|- ( ( A e. On /\ B e. On /\ C e. On ) -> A C_ On )
12	11	sselda	|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ a e. A ) -> a e. On )
13		simpl2	|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ a e. A ) -> B e. On )
14	12 13	naddcld	|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ a e. A ) -> ( a +no B ) e. On )
15		ontri1	|- ( ( C e. On /\ ( a +no B ) e. On ) -> ( C C_ ( a +no B ) <-> -. ( a +no B ) e. C ) )
16	9 14 15	syl2anc	|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ a e. A ) -> ( C C_ ( a +no B ) <-> -. ( a +no B ) e. C ) )
17	16	rexbidva	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. a e. A C C_ ( a +no B ) <-> E. a e. A -. ( a +no B ) e. C ) )
18		simpl3	|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ b e. B ) -> C e. On )
19		simpl1	|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ b e. B ) -> A e. On )
20		onss	|- ( B e. On -> B C_ On )
21	20	3ad2ant2	|- ( ( A e. On /\ B e. On /\ C e. On ) -> B C_ On )
22	21	sselda	|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ b e. B ) -> b e. On )
23	19 22	naddcld	|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ b e. B ) -> ( A +no b ) e. On )
24		ontri1	|- ( ( C e. On /\ ( A +no b ) e. On ) -> ( C C_ ( A +no b ) <-> -. ( A +no b ) e. C ) )
25	18 23 24	syl2anc	|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ b e. B ) -> ( C C_ ( A +no b ) <-> -. ( A +no b ) e. C ) )
26	25	rexbidva	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( E. b e. B C C_ ( A +no b ) <-> E. b e. B -. ( A +no b ) e. C ) )
27	17 26	orbi12d	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( E. a e. A C C_ ( a +no B ) \/ E. b e. B C C_ ( A +no b ) ) <-> ( E. a e. A -. ( a +no B ) e. C \/ E. b e. B -. ( A +no b ) e. C ) ) )
28		rexnal	|- ( E. a e. A -. ( a +no B ) e. C <-> -. A. a e. A ( a +no B ) e. C )
29		rexnal	|- ( E. b e. B -. ( A +no b ) e. C <-> -. A. b e. B ( A +no b ) e. C )
30	28 29	orbi12i	|- ( ( E. a e. A -. ( a +no B ) e. C \/ E. b e. B -. ( A +no b ) e. C ) <-> ( -. A. a e. A ( a +no B ) e. C \/ -. A. b e. B ( A +no b ) e. C ) )
31		ianor	|- ( -. ( A. a e. A ( a +no B ) e. C /\ A. b e. B ( A +no b ) e. C ) <-> ( -. A. a e. A ( a +no B ) e. C \/ -. A. b e. B ( A +no b ) e. C ) )
32	30 31	bitr4i	|- ( ( E. a e. A -. ( a +no B ) e. C \/ E. b e. B -. ( A +no b ) e. C ) <-> -. ( A. a e. A ( a +no B ) e. C /\ A. b e. B ( A +no b ) e. C ) )
33	27 32	bitrdi	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( E. a e. A C C_ ( a +no B ) \/ E. b e. B C C_ ( A +no b ) ) <-> -. ( A. a e. A ( a +no B ) e. C /\ A. b e. B ( A +no b ) e. C ) ) )
34	33	con2bid	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A. a e. A ( a +no B ) e. C /\ A. b e. B ( A +no b ) e. C ) <-> -. ( E. a e. A C C_ ( a +no B ) \/ E. b e. B C C_ ( A +no b ) ) ) )
35	3 8 34	3bitr4d	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) C_ C <-> ( A. a e. A ( a +no B ) e. C /\ A. b e. B ( A +no b ) e. C ) ) )