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

Proof

Step	Hyp	Ref	Expression
1		elold	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑏 ) ) )
2		onelss	⊢ ( 𝐴 ∈ On → ( 𝑏 ∈ 𝐴 → 𝑏 ⊆ 𝐴 ) )
3	2	imp	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ⊆ 𝐴 )
4		madess	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ⊆ 𝐴 ) → ( M ‘ 𝑏 ) ⊆ ( M ‘ 𝐴 ) )
5	3 4	syldan	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → ( M ‘ 𝑏 ) ⊆ ( M ‘ 𝐴 ) )
6	5	sseld	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → ( 𝑥 ∈ ( M ‘ 𝑏 ) → 𝑥 ∈ ( M ‘ 𝐴 ) ) )
7	6	rexlimdva	⊢ ( 𝐴 ∈ On → ( ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑏 ) → 𝑥 ∈ ( M ‘ 𝐴 ) ) )
8	1 7	sylbid	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ ( O ‘ 𝐴 ) → 𝑥 ∈ ( M ‘ 𝐴 ) ) )
9	8	ssrdv	⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) )
10		oldf	⊢ O : On ⟶ 𝒫 No
11	10	fdmi	⊢ dom O = On
12	11	eleq2i	⊢ ( 𝐴 ∈ dom O ↔ 𝐴 ∈ On )
13		ndmfv	⊢ ( ¬ 𝐴 ∈ dom O → ( O ‘ 𝐴 ) = ∅ )
14	12 13	sylnbir	⊢ ( ¬ 𝐴 ∈ On → ( O ‘ 𝐴 ) = ∅ )
15		0ss	⊢ ∅ ⊆ ( M ‘ 𝐴 )
16	14 15	eqsstrdi	⊢ ( ¬ 𝐴 ∈ On → ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 ) )
17	9 16	pm2.61i	⊢ ( O ‘ 𝐴 ) ⊆ ( M ‘ 𝐴 )