Theorem naddel12

Description: Natural addition to both sides of ordinal less-than. (Contributed by Scott Fenton, 7-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		simprr	$$⊢\left(\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\wedge \left(A\in C\wedge B\in D\right)\right)\to B\in D$$
2		onelon	$$⊢\left(D\in \mathrm{On}\wedge B\in D\right)\to B\in \mathrm{On}$$
3	2	ad2ant2l	$$⊢\left(\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\wedge \left(A\in C\wedge B\in D\right)\right)\to B\in \mathrm{On}$$
4		simplr	$$⊢\left(\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\wedge \left(A\in C\wedge B\in D\right)\right)\to D\in \mathrm{On}$$
5		onelon	$$⊢\left(C\in \mathrm{On}\wedge A\in C\right)\to A\in \mathrm{On}$$
6	5	ad2ant2r	$$⊢\left(\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\wedge \left(A\in C\wedge B\in D\right)\right)\to A\in \mathrm{On}$$
7		naddel2	Could not format ( ( B e. On /\ D e. On /\ A e. On ) -> ( B e. D <-> ( A +no B ) e. ( A +no D ) ) ) : No typesetting found for |- ( ( B e. On /\ D e. On /\ A e. On ) -> ( B e. D <-> ( A +no B ) e. ( A +no D ) ) ) with typecode |-
8	3 4 6 7	syl3anc	Could not format ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( B e. D <-> ( A +no B ) e. ( A +no D ) ) ) : No typesetting found for |- ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( B e. D <-> ( A +no B ) e. ( A +no D ) ) ) with typecode |-
9	1 8	mpbid	Could not format ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A +no B ) e. ( A +no D ) ) : No typesetting found for |- ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A +no B ) e. ( A +no D ) ) with typecode |-
10		simprl	$$⊢\left(\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\wedge \left(A\in C\wedge B\in D\right)\right)\to A\in C$$
11		simpll	$$⊢\left(\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\wedge \left(A\in C\wedge B\in D\right)\right)\to C\in \mathrm{On}$$
12		naddel1	Could not format ( ( A e. On /\ C e. On /\ D e. On ) -> ( A e. C <-> ( A +no D ) e. ( C +no D ) ) ) : No typesetting found for |- ( ( A e. On /\ C e. On /\ D e. On ) -> ( A e. C <-> ( A +no D ) e. ( C +no D ) ) ) with typecode |-
13	6 11 4 12	syl3anc	Could not format ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A e. C <-> ( A +no D ) e. ( C +no D ) ) ) : No typesetting found for |- ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A e. C <-> ( A +no D ) e. ( C +no D ) ) ) with typecode |-
14	10 13	mpbid	Could not format ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A +no D ) e. ( C +no D ) ) : No typesetting found for |- ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A +no D ) e. ( C +no D ) ) with typecode |-
15		naddcl	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 |-
16	15	adantr	Could not format ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( C +no D ) e. On ) : No typesetting found for |- ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( C +no D ) e. On ) with typecode |-
17		ontr1	Could not format ( ( C +no D ) e. On -> ( ( ( A +no B ) e. ( A +no D ) /\ ( A +no D ) e. ( C +no D ) ) -> ( A +no B ) e. ( C +no D ) ) ) : No typesetting found for |- ( ( C +no D ) e. On -> ( ( ( A +no B ) e. ( A +no D ) /\ ( A +no D ) e. ( C +no D ) ) -> ( A +no B ) e. ( C +no D ) ) ) with typecode |-
18	16 17	syl	Could not format ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( ( ( A +no B ) e. ( A +no D ) /\ ( A +no D ) e. ( C +no D ) ) -> ( A +no B ) e. ( C +no D ) ) ) : No typesetting found for |- ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( ( ( A +no B ) e. ( A +no D ) /\ ( A +no D ) e. ( C +no D ) ) -> ( A +no B ) e. ( C +no D ) ) ) with typecode |-
19	9 14 18	mp2and	Could not format ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A +no B ) e. ( C +no D ) ) : No typesetting found for |- ( ( ( C e. On /\ D e. On ) /\ ( A e. C /\ B e. D ) ) -> ( A +no B ) e. ( C +no D ) ) with typecode |-
20	19	ex	Could not format ( ( C e. On /\ D e. On ) -> ( ( A e. C /\ B e. D ) -> ( A +no B ) e. ( C +no D ) ) ) : No typesetting found for |- ( ( C e. On /\ D e. On ) -> ( ( A e. C /\ B e. D ) -> ( A +no B ) e. ( C +no D ) ) ) with typecode |-