Theorem naddel1

Description: Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		naddelim	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B -> ( A +no C ) e. ( B +no C ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B -> ( A +no C ) e. ( B +no C ) ) ) with typecode |-
2		naddssim	Could not format ( ( B e. On /\ A e. On /\ C e. On ) -> ( B C_ A -> ( B +no C ) C_ ( A +no C ) ) ) : No typesetting found for |- ( ( B e. On /\ A e. On /\ C e. On ) -> ( B C_ A -> ( B +no C ) C_ ( A +no C ) ) ) with typecode |-
3	2	3com12	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( B C_ A -> ( B +no C ) C_ ( A +no C ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( B C_ A -> ( B +no C ) C_ ( A +no C ) ) ) with typecode |-
4		ontri1	$$⊢\left(B\in \mathrm{On}\wedge A\in \mathrm{On}\right)\to \left(B\subseteq A\leftrightarrow \neg A\in B\right)$$
5	4	ancoms	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(B\subseteq A\leftrightarrow \neg A\in B\right)$$
6	5	3adant3	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to \left(B\subseteq A\leftrightarrow \neg A\in B\right)$$
7		naddcl	Could not format ( ( B e. On /\ C e. On ) -> ( B +no C ) e. On ) : No typesetting found for |- ( ( B e. On /\ C e. On ) -> ( B +no C ) e. On ) with typecode |-
8	7	3adant1	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) e. On ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) e. On ) with typecode |-
9		naddcl	Could not format ( ( A e. On /\ C e. On ) -> ( A +no C ) e. On ) : No typesetting found for |- ( ( A e. On /\ C e. On ) -> ( A +no C ) e. On ) with typecode |-
10		ontri1	Could not format ( ( ( B +no C ) e. On /\ ( A +no C ) e. On ) -> ( ( B +no C ) C_ ( A +no C ) <-> -. ( A +no C ) e. ( B +no C ) ) ) : No typesetting found for |- ( ( ( B +no C ) e. On /\ ( A +no C ) e. On ) -> ( ( B +no C ) C_ ( A +no C ) <-> -. ( A +no C ) e. ( B +no C ) ) ) with typecode |-
11	8 9 10	3imp3i2an	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( B +no C ) C_ ( A +no C ) <-> -. ( A +no C ) e. ( B +no C ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( B +no C ) C_ ( A +no C ) <-> -. ( A +no C ) e. ( B +no C ) ) ) with typecode |-
12	3 6 11	3imtr3d	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. A e. B -> -. ( A +no C ) e. ( B +no C ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( -. A e. B -> -. ( A +no C ) e. ( B +no C ) ) ) with typecode |-
13	1 12	impcon4bid	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( A +no C ) e. ( B +no C ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( A +no C ) e. ( B +no C ) ) ) with typecode |-