madess

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

		Ref	Expression
	Assertion	madess	$⊢ (B \in On \land A \subseteq B) \to M (A) \subseteq M (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	sspwd	$⊢ A \subseteq B \to 𝒫 ⋃ M [A] \subseteq 𝒫 ⋃ M [B]$
4	3	adantl	$⊢ (B \in On \land A \subseteq B) \to 𝒫 ⋃ M [A] \subseteq 𝒫 ⋃ M [B]$
5	4	adantl	$⊢ (A \in On \land (B \in On \land A \subseteq B)) \to 𝒫 ⋃ M [A] \subseteq 𝒫 ⋃ M [B]$
6		ssrexv	$⊢ 𝒫 ⋃ M [A] \subseteq 𝒫 ⋃ M [B] \to (\exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to \exists a \in 𝒫 ⋃ M [B] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x))$
7	5 6	syl	$⊢ (A \in On \land (B \in On \land A \subseteq B)) \to (\exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to \exists a \in 𝒫 ⋃ M [B] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x))$
8		ssrexv	$⊢ 𝒫 ⋃ M [A] \subseteq 𝒫 ⋃ M [B] \to (\exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to \exists b \in 𝒫 ⋃ M [B] (a ≪_{s} b \land a \|_{s} b = x))$
9	5 8	syl	$⊢ (A \in On \land (B \in On \land A \subseteq B)) \to (\exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to \exists b \in 𝒫 ⋃ M [B] (a ≪_{s} b \land a \|_{s} b = x))$
10	9	reximdv	$⊢ (A \in On \land (B \in On \land A \subseteq B)) \to (\exists a \in 𝒫 ⋃ M [B] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to \exists a \in 𝒫 ⋃ M [B] \exists b \in 𝒫 ⋃ M [B] (a ≪_{s} b \land a \|_{s} b = x))$
11	7 10	syld	$⊢ (A \in On \land (B \in On \land A \subseteq B)) \to (\exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to \exists a \in 𝒫 ⋃ M [B] \exists b \in 𝒫 ⋃ M [B] (a ≪_{s} b \land a \|_{s} b = x))$
12	11	adantr	$⊢ ((A \in On \land (B \in On \land A \subseteq B)) \land x \in No) \to (\exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to \exists a \in 𝒫 ⋃ M [B] \exists b \in 𝒫 ⋃ M [B] (a ≪_{s} b \land a \|_{s} b = x))$
13	12	ss2rabdv	$⊢ (A \in On \land (B \in On \land A \subseteq B)) \to \{x \in No \| \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x)\} \subseteq \{x \in No \| \exists a \in 𝒫 ⋃ M [B] \exists b \in 𝒫 ⋃ M [B] (a ≪_{s} b \land a \|_{s} b = x)\}$
14		madeval2	$⊢ A \in On \to M (A) = \{x \in No \| \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x)\}$
15	14	adantr	$⊢ (A \in On \land (B \in On \land A \subseteq B)) \to M (A) = \{x \in No \| \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x)\}$
16		madeval2	$⊢ B \in On \to M (B) = \{x \in No \| \exists a \in 𝒫 ⋃ M [B] \exists b \in 𝒫 ⋃ M [B] (a ≪_{s} b \land a \|_{s} b = x)\}$
17	16	adantr	$⊢ (B \in On \land A \subseteq B) \to M (B) = \{x \in No \| \exists a \in 𝒫 ⋃ M [B] \exists b \in 𝒫 ⋃ M [B] (a ≪_{s} b \land a \|_{s} b = x)\}$
18	17	adantl	$⊢ (A \in On \land (B \in On \land A \subseteq B)) \to M (B) = \{x \in No \| \exists a \in 𝒫 ⋃ M [B] \exists b \in 𝒫 ⋃ M [B] (a ≪_{s} b \land a \|_{s} b = x)\}$
19	13 15 18	3sstr4d	$⊢ (A \in On \land (B \in On \land A \subseteq B)) \to M (A) \subseteq M (B)$
20		madef	$⊢ M : On ⟶ 𝒫 No$
21	20	fdmi	$⊢ dom M = On$
22	21	eleq2i	$⊢ A \in dom M \leftrightarrow A \in On$
23		ndmfv	$⊢ \neg A \in dom M \to M (A) = \emptyset$
24	22 23	sylnbir	$⊢ \neg A \in On \to M (A) = \emptyset$
25		0ss	$⊢ \emptyset \subseteq M (B)$
26	24 25	eqsstrdi	$⊢ \neg A \in On \to M (A) \subseteq M (B)$
27	26	adantr	$⊢ (\neg A \in On \land (B \in On \land A \subseteq B)) \to M (A) \subseteq M (B)$
28	19 27	pm2.61ian	$⊢ (B \in On \land A \subseteq B) \to M (A) \subseteq M (B)$

Metamath Proof Explorer

Theorem madess

Proof