Metamath Proof Explorer

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 ∈ On → Old ⁡ A ⊆ M ⁡ A

Proof

Step Hyp Ref Expression
1 elold ⊢ A ∈ On → x ∈ Old ⁡ A ↔ ∃ b ∈ A x ∈ M ⁡ b
2 onelon ⊢ A ∈ On ∧ b ∈ A → b ∈ On
3 simpl ⊢ A ∈ On ∧ b ∈ A → A ∈ On
4 onelss ⊢ A ∈ On → b ∈ A → b ⊆ A
5 4 imp ⊢ A ∈ On ∧ b ∈ A → b ⊆ A
6 madess ⊢ b ∈ On ∧ A ∈ On ∧ b ⊆ A → M ⁡ b ⊆ M ⁡ A
7 2 3 5 6 syl3anc ⊢ A ∈ On ∧ b ∈ A → M ⁡ b ⊆ M ⁡ A
8 7 sseld ⊢ A ∈ On ∧ b ∈ A → x ∈ M ⁡ b → x ∈ M ⁡ A
9 8 rexlimdva ⊢ A ∈ On → ∃ b ∈ A x ∈ M ⁡ b → x ∈ M ⁡ A
10 1 9 sylbid ⊢ A ∈ On → x ∈ Old ⁡ A → x ∈ M ⁡ A
11 10 ssrdv ⊢ A ∈ On → Old ⁡ A ⊆ M ⁡ A