oldss

Description: If A is less than or equal to ordinal B , then the old set of A is included in the made set of B . (Contributed by Scott Fenton, 9-Oct-2024)

		Ref	Expression
	Assertion	oldss	$⊢ (B \in On \land A \subseteq B) \to Old (A) \subseteq Old (B)$

Proof

Step	Hyp	Ref	Expression
1		imass2	$⊢ A \subseteq B \to M [A] \subseteq M [B]$
2	1	unissd	$⊢ A \subseteq B \to ⋃ M [A] \subseteq ⋃ M [B]$
3	2	adantl	$⊢ ((A \in On \land B \in On) \land A \subseteq B) \to ⋃ M [A] \subseteq ⋃ M [B]$
4		oldval	$⊢ A \in On \to Old (A) = ⋃ M [A]$
5	4	adantr	$⊢ (A \in On \land B \in On) \to Old (A) = ⋃ M [A]$
6	5	adantr	$⊢ ((A \in On \land B \in On) \land A \subseteq B) \to Old (A) = ⋃ M [A]$
7		oldval	$⊢ B \in On \to Old (B) = ⋃ M [B]$
8	7	adantl	$⊢ (A \in On \land B \in On) \to Old (B) = ⋃ M [B]$
9	8	adantr	$⊢ ((A \in On \land B \in On) \land A \subseteq B) \to Old (B) = ⋃ M [B]$
10	3 6 9	3sstr4d	$⊢ ((A \in On \land B \in On) \land A \subseteq B) \to Old (A) \subseteq Old (B)$
11	10	expl	$⊢ A \in On \to ((B \in On \land A \subseteq B) \to Old (A) \subseteq Old (B))$
12		oldf	$⊢ Old : On ⟶ 𝒫 No$
13	12	fdmi	$⊢ dom Old = On$
14	13	eleq2i	$⊢ A \in dom Old \leftrightarrow A \in On$
15		ndmfv	$⊢ \neg A \in dom Old \to Old (A) = \emptyset$
16	14 15	sylnbir	$⊢ \neg A \in On \to Old (A) = \emptyset$
17		0ss	$⊢ \emptyset \subseteq Old (B)$
18	16 17	eqsstrdi	$⊢ \neg A \in On \to Old (A) \subseteq Old (B)$
19	18	a1d	$⊢ \neg A \in On \to ((B \in On \land A \subseteq B) \to Old (A) \subseteq Old (B))$
20	11 19	pm2.61i	$⊢ (B \in On \land A \subseteq B) \to Old (A) \subseteq Old (B)$

Metamath Proof Explorer

Theorem oldss

Proof