Theorem oldssmade

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

	Ref	Expression
Assertion	oldssmade	|- ( A e. On -> ( _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		onelon	|- ( ( A e. On /\ b e. A ) -> b e. On )
3		simpl	|- ( ( A e. On /\ b e. A ) -> A e. On )
4		onelss	|- ( A e. On -> ( b e. A -> b C_ A ) )
5	4	imp	|- ( ( A e. On /\ b e. A ) -> b C_ A )
6		madess	|- ( ( b e. On /\ A e. On /\ b C_ A ) -> ( _M ` b ) C_ ( _M ` A ) )
7	2 3 5 6	syl3anc	|- ( ( A e. On /\ b e. A ) -> ( _M ` b ) C_ ( _M ` A ) )
8	7	sseld	|- ( ( A e. On /\ b e. A ) -> ( x e. ( _M ` b ) -> x e. ( _M ` A ) ) )
9	8	rexlimdva	|- ( A e. On -> ( E. b e. A x e. ( _M ` b ) -> x e. ( _M ` A ) ) )
10	1 9	sylbid	|- ( A e. On -> ( x e. ( _Old ` A ) -> x e. ( _M ` A ) ) )
11	10	ssrdv	|- ( A e. On -> ( _Old ` A ) C_ ( _M ` A ) )