Theorem oldss

Description: If A is less than or equal to ordinal B , then the old set of A is included in the made set of B . (Contributed by Scott Fenton, 9-Oct-2024)

	Ref	Expression
Assertion	oldss	|- ( ( B e. On /\ A C_ B ) -> ( _Old ` A ) C_ ( _Old ` B ) )

Proof

Step	Hyp	Ref	Expression
1		imass2	|- ( A C_ B -> ( _Made " A ) C_ ( _Made " B ) )
2	1	unissd	|- ( A C_ B -> U. ( _Made " A ) C_ U. ( _Made " B ) )
3	2	adantl	|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> U. ( _Made " A ) C_ U. ( _Made " B ) )
4		oldval	|- ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) )
5	4	adantr	|- ( ( A e. On /\ B e. On ) -> ( _Old ` A ) = U. ( _Made " A ) )
6	5	adantr	|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( _Old ` A ) = U. ( _Made " A ) )
7		oldval	|- ( B e. On -> ( _Old ` B ) = U. ( _Made " B ) )
8	7	adantl	|- ( ( A e. On /\ B e. On ) -> ( _Old ` B ) = U. ( _Made " B ) )
9	8	adantr	|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( _Old ` B ) = U. ( _Made " B ) )
10	3 6 9	3sstr4d	|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( _Old ` A ) C_ ( _Old ` B ) )
11	10	expl	|- ( A e. On -> ( ( B e. On /\ A C_ B ) -> ( _Old ` A ) C_ ( _Old ` B ) ) )
12		oldf	|- _Old : On --> ~P No
13	12	fdmi	|- dom _Old = On
14	13	eleq2i	|- ( A e. dom _Old <-> A e. On )
15		ndmfv	|- ( -. A e. dom _Old -> ( _Old ` A ) = (/) )
16	14 15	sylnbir	|- ( -. A e. On -> ( _Old ` A ) = (/) )
17		0ss	|- (/) C_ ( _Old ` B )
18	16 17	eqsstrdi	|- ( -. A e. On -> ( _Old ` A ) C_ ( _Old ` B ) )
19	18	a1d	|- ( -. A e. On -> ( ( B e. On /\ A C_ B ) -> ( _Old ` A ) C_ ( _Old ` B ) ) )
20	11 19	pm2.61i	|- ( ( B e. On /\ A C_ B ) -> ( _Old ` A ) C_ ( _Old ` B ) )