Theorem hashnnlt

Description: The # function on _om preserves the ordering. (Contributed by Eric Schmidt, 7-Jul-2026)

	Ref	Expression
Assertion	hashnnlt	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to \left|B\right|<\left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		nnfi	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$
2		nnord	$$⊢A\in \mathrm{\omega }\to \mathrm{Ord}A$$
3		ordpss	$$⊢\mathrm{Ord}A\to \left(B\in A\to B\subset A\right)$$
4	2 3	syl	$$⊢A\in \mathrm{\omega }\to \left(B\in A\to B\subset A\right)$$
5	4	imp	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to B\subset A$$
6		hashpss	$$⊢\left(A\in \mathrm{Fin}\wedge B\subset A\right)\to \left|B\right|<\left|A\right|$$
7	1 5 6	syl2an2r	$$⊢\left(A\in \mathrm{\omega }\wedge B\in A\right)\to \left|B\right|<\left|A\right|$$