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	⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elold	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑏 ) ) )
2		onelon	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ On )
3		simpl	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → 𝐴 ∈ On )
4		onelss	⊢ ( 𝐴 ∈ On → ( 𝑏 ∈ 𝐴 → 𝑏 ⊆ 𝐴 ) )
5	4	imp	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ⊆ 𝐴 )
6		madess	⊢ ( ( 𝑏 ∈ On ∧ 𝐴 ∈ On ∧ 𝑏 ⊆ 𝐴 ) → ( M ‘ 𝑏 ) ⊆ ( M ‘ 𝐴 ) )
7	2 3 5 6	syl3anc	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → ( M ‘ 𝑏 ) ⊆ ( M ‘ 𝐴 ) )
8	7	sseld	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → ( 𝑥 ∈ ( M ‘ 𝑏 ) → 𝑥 ∈ ( M ‘ 𝐴 ) ) )
9	8	rexlimdva	⊢ ( 𝐴 ∈ On → ( ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑏 ) → 𝑥 ∈ ( M ‘ 𝐴 ) ) )
10	1 9	sylbid	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ ( O ‘ 𝐴 ) → 𝑥 ∈ ( M ‘ 𝐴 ) ) )
11	10	ssrdv	⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) )