Theorem nmuladdss

Description: Ordering relationship for natural ordinal operations. (Contributed by Scott Fenton, 15-Jul-2026)

	Ref	Expression
Assertion	nmuladdss	Could not format assertion : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) /\ ( C C_ A /\ D C_ B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		onsseleq	$$⊢\left(C\in \mathrm{On}\wedge A\in \mathrm{On}\right)\to \left(C\subseteq A\leftrightarrow \left(C\in A\vee C=A\right)\right)$$
2	1	ancoms	$$⊢\left(A\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to \left(C\subseteq A\leftrightarrow \left(C\in A\vee C=A\right)\right)$$
3		onsseleq	$$⊢\left(D\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(D\subseteq B\leftrightarrow \left(D\in B\vee D=B\right)\right)$$
4	3	ancoms	$$⊢\left(B\in \mathrm{On}\wedge D\in \mathrm{On}\right)\to \left(D\subseteq B\leftrightarrow \left(D\in B\vee D=B\right)\right)$$
5	2 4	bi2anan9	$$⊢\left(\left(A\in \mathrm{On}\wedge C\in \mathrm{On}\right)\wedge \left(B\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\to \left(\left(C\subseteq A\wedge D\subseteq B\right)\leftrightarrow \left(\left(C\in A\vee C=A\right)\wedge \left(D\in B\vee D=B\right)\right)\right)$$
6	5	an4s	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\to \left(\left(C\subseteq A\wedge D\subseteq B\right)\leftrightarrow \left(\left(C\in A\vee C=A\right)\wedge \left(D\in B\vee D=B\right)\right)\right)$$
7		nmulcl	Could not format ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On ) with typecode |-
8	7	adantr	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( A .no B ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( A .no B ) e. On ) with typecode |-
9		onelon	$$⊢\left(A\in \mathrm{On}\wedge C\in A\right)\to C\in \mathrm{On}$$
10		onelon	$$⊢\left(B\in \mathrm{On}\wedge D\in B\right)\to D\in \mathrm{On}$$
11		nmulcl	Could not format ( ( C e. On /\ D e. On ) -> ( C .no D ) e. On ) : No typesetting found for |- ( ( C e. On /\ D e. On ) -> ( C .no D ) e. On ) with typecode |-
12	9 10 11	syl2an	Could not format ( ( ( A e. On /\ C e. A ) /\ ( B e. On /\ D e. B ) ) -> ( C .no D ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ C e. A ) /\ ( B e. On /\ D e. B ) ) -> ( C .no D ) e. On ) with typecode |-
13	12	an4s	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( C .no D ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( C .no D ) e. On ) with typecode |-
14	8 13	naddcld	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( A .no B ) +no ( C .no D ) ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( A .no B ) +no ( C .no D ) ) e. On ) with typecode |-
15		ontr	Could not format ( ( ( A .no B ) +no ( C .no D ) ) e. On -> Tr ( ( A .no B ) +no ( C .no D ) ) ) : No typesetting found for |- ( ( ( A .no B ) +no ( C .no D ) ) e. On -> Tr ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-
16	14 15	syl	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> Tr ( ( A .no B ) +no ( C .no D ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> Tr ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-
17		nmuladdel	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-
18		trss	Could not format ( Tr ( ( A .no B ) +no ( C .no D ) ) -> ( ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) : No typesetting found for |- ( Tr ( ( A .no B ) +no ( C .no D ) ) -> ( ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) with typecode |-
19	16 17 18	sylc	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-
20	19	adantlr	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-
21	20	expr	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( D e. B -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( D e. B -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) with typecode |-
22		simplll	$$⊢\left(\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\wedge C\in A\right)\to A\in \mathrm{On}$$
23		simpllr	$$⊢\left(\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\wedge C\in A\right)\to B\in \mathrm{On}$$
24	22 23	nmulcld	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( A .no B ) e. On ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( A .no B ) e. On ) with typecode |-
25		simplrl	$$⊢\left(\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\wedge C\in A\right)\to C\in \mathrm{On}$$
26	25 23	nmulcld	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( C .no B ) e. On ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( C .no B ) e. On ) with typecode |-
27		naddcom	Could not format ( ( ( A .no B ) e. On /\ ( C .no B ) e. On ) -> ( ( A .no B ) +no ( C .no B ) ) = ( ( C .no B ) +no ( A .no B ) ) ) : No typesetting found for |- ( ( ( A .no B ) e. On /\ ( C .no B ) e. On ) -> ( ( A .no B ) +no ( C .no B ) ) = ( ( C .no B ) +no ( A .no B ) ) ) with typecode |-
28	24 26 27	syl2anc	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( ( A .no B ) +no ( C .no B ) ) = ( ( C .no B ) +no ( A .no B ) ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( ( A .no B ) +no ( C .no B ) ) = ( ( C .no B ) +no ( A .no B ) ) ) with typecode |-
29	28	eqimsscd	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( ( C .no B ) +no ( A .no B ) ) C_ ( ( A .no B ) +no ( C .no B ) ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( ( C .no B ) +no ( A .no B ) ) C_ ( ( A .no B ) +no ( C .no B ) ) ) with typecode |-
30		oveq2	Could not format ( D = B -> ( A .no D ) = ( A .no B ) ) : No typesetting found for |- ( D = B -> ( A .no D ) = ( A .no B ) ) with typecode |-
31	30	oveq2d	Could not format ( D = B -> ( ( C .no B ) +no ( A .no D ) ) = ( ( C .no B ) +no ( A .no B ) ) ) : No typesetting found for |- ( D = B -> ( ( C .no B ) +no ( A .no D ) ) = ( ( C .no B ) +no ( A .no B ) ) ) with typecode |-
32		oveq2	Could not format ( D = B -> ( C .no D ) = ( C .no B ) ) : No typesetting found for |- ( D = B -> ( C .no D ) = ( C .no B ) ) with typecode |-
33	32	oveq2d	Could not format ( D = B -> ( ( A .no B ) +no ( C .no D ) ) = ( ( A .no B ) +no ( C .no B ) ) ) : No typesetting found for |- ( D = B -> ( ( A .no B ) +no ( C .no D ) ) = ( ( A .no B ) +no ( C .no B ) ) ) with typecode |-
34	31 33	sseq12d	Could not format ( D = B -> ( ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) <-> ( ( C .no B ) +no ( A .no B ) ) C_ ( ( A .no B ) +no ( C .no B ) ) ) ) : No typesetting found for |- ( D = B -> ( ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) <-> ( ( C .no B ) +no ( A .no B ) ) C_ ( ( A .no B ) +no ( C .no B ) ) ) ) with typecode |-
35	29 34	syl5ibrcom	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( D = B -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( D = B -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) with typecode |-
36	21 35	jaod	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) with typecode |-
37	36	ex	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( C e. A -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( C e. A -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) ) with typecode |-
38		ssid	Could not format ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) : No typesetting found for |- ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) with typecode |-
39	38	2a1i	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( D e. B \/ D = B ) -> ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( D e. B \/ D = B ) -> ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) ) ) with typecode |-
40		oveq1	Could not format ( C = A -> ( C .no B ) = ( A .no B ) ) : No typesetting found for |- ( C = A -> ( C .no B ) = ( A .no B ) ) with typecode |-
41	40	oveq1d	Could not format ( C = A -> ( ( C .no B ) +no ( A .no D ) ) = ( ( A .no B ) +no ( A .no D ) ) ) : No typesetting found for |- ( C = A -> ( ( C .no B ) +no ( A .no D ) ) = ( ( A .no B ) +no ( A .no D ) ) ) with typecode |-
42		oveq1	Could not format ( C = A -> ( C .no D ) = ( A .no D ) ) : No typesetting found for |- ( C = A -> ( C .no D ) = ( A .no D ) ) with typecode |-
43	42	oveq2d	Could not format ( C = A -> ( ( A .no B ) +no ( C .no D ) ) = ( ( A .no B ) +no ( A .no D ) ) ) : No typesetting found for |- ( C = A -> ( ( A .no B ) +no ( C .no D ) ) = ( ( A .no B ) +no ( A .no D ) ) ) with typecode |-
44	41 43	sseq12d	Could not format ( C = A -> ( ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) <-> ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) ) ) : No typesetting found for |- ( C = A -> ( ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) <-> ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) ) ) with typecode |-
45	44	imbi2d	Could not format ( C = A -> ( ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) <-> ( ( D e. B \/ D = B ) -> ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) ) ) ) : No typesetting found for |- ( C = A -> ( ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) <-> ( ( D e. B \/ D = B ) -> ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) ) ) ) with typecode |-
46	39 45	syl5ibrcom	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( C = A -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( C = A -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) ) with typecode |-
47	37 46	jaod	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( C e. A \/ C = A ) -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( C e. A \/ C = A ) -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) ) with typecode |-
48	47	impd	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( ( C e. A \/ C = A ) /\ ( D e. B \/ D = B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( ( C e. A \/ C = A ) /\ ( D e. B \/ D = B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) with typecode |-
49	6 48	sylbid	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( C C_ A /\ D C_ B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( C C_ A /\ D C_ B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) with typecode |-
50	49	3impia	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) /\ ( C C_ A /\ D C_ B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) /\ ( C C_ A /\ D C_ B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-