Theorem oldssmade

Description: The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024)

	Ref	Expression
Assertion	oldssmade	|- ( _Old ` A ) C_ ( _M ` A )

Proof

Step	Hyp	Ref	Expression
1		elold	|- ( A e. On -> ( x e. ( _Old ` A ) <-> E. b e. A x e. ( _M ` b ) ) )
2		onelss	|- ( A e. On -> ( b e. A -> b C_ A ) )
3	2	imp	|- ( ( A e. On /\ b e. A ) -> b C_ A )
4		madess	|- ( ( A e. On /\ b C_ A ) -> ( _M ` b ) C_ ( _M ` A ) )
5	3 4	syldan	|- ( ( A e. On /\ b e. A ) -> ( _M ` b ) C_ ( _M ` A ) )
6	5	sseld	|- ( ( A e. On /\ b e. A ) -> ( x e. ( _M ` b ) -> x e. ( _M ` A ) ) )
7	6	rexlimdva	|- ( A e. On -> ( E. b e. A x e. ( _M ` b ) -> x e. ( _M ` A ) ) )
8	1 7	sylbid	|- ( A e. On -> ( x e. ( _Old ` A ) -> x e. ( _M ` A ) ) )
9	8	ssrdv	|- ( A e. On -> ( _Old ` A ) C_ ( _M ` A ) )
10		oldf	|- _Old : On --> ~P No
11	10	fdmi	|- dom _Old = On
12	11	eleq2i	|- ( A e. dom _Old <-> A e. On )
13		ndmfv	|- ( -. A e. dom _Old -> ( _Old ` A ) = (/) )
14	12 13	sylnbir	|- ( -. A e. On -> ( _Old ` A ) = (/) )
15		0ss	|- (/) C_ ( _M ` A )
16	14 15	eqsstrdi	|- ( -. A e. On -> ( _Old ` A ) C_ ( _M ` A ) )
17	9 16	pm2.61i	|- ( _Old ` A ) C_ ( _M ` A )