Metamath Proof Explorer

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 ⊆ M ⁡ A

Proof

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