Metamath Proof Explorer

Theorem madess

Description: If ordinal 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, 7-Aug-2024)

		Ref	Expression
	Assertion	madess	$⊢ (A \in On \land 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	3ad2ant3	$⊢ (A \in On \land B \in On \land A \subseteq B) \to M [A] \subseteq M [B]$
3	2	adantr	$⊢ ((A \in On \land B \in On \land A \subseteq B) \land x \in No) \to M [A] \subseteq M [B]$
4	3	unissd	$⊢ ((A \in On \land B \in On \land A \subseteq B) \land x \in No) \to ⋃ M [A] \subseteq ⋃ M [B]$
5	4	sspwd	$⊢ ((A \in On \land B \in On \land A \subseteq B) \land x \in No) \to 𝒫 ⋃ M [A] \subseteq 𝒫 ⋃ M [B]$
6		ssrexv	$⊢ 𝒫 ⋃ M [A] \subseteq 𝒫 ⋃ M [B] \to (\exists l \in 𝒫 ⋃ M [A] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x) \to \exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x))$
7	5 6	syl	$⊢ ((A \in On \land B \in On \land A \subseteq B) \land x \in No) \to (\exists l \in 𝒫 ⋃ M [A] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x) \to \exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x))$
8		ssrexv	$⊢ 𝒫 ⋃ M [A] \subseteq 𝒫 ⋃ M [B] \to (\exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x) \to \exists r \in 𝒫 ⋃ M [B] (l ≪_{s} r \land l \|_{s} r = x))$
9	5 8	syl	$⊢ ((A \in On \land B \in On \land A \subseteq B) \land x \in No) \to (\exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x) \to \exists r \in 𝒫 ⋃ M [B] (l ≪_{s} r \land l \|_{s} r = x))$
10	9	reximdv	$⊢ ((A \in On \land B \in On \land A \subseteq B) \land x \in No) \to (\exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x) \to \exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [B] (l ≪_{s} r \land l \|_{s} r = x))$
11	7 10	syld	$⊢ ((A \in On \land B \in On \land A \subseteq B) \land x \in No) \to (\exists l \in 𝒫 ⋃ M [A] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x) \to \exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [B] (l ≪_{s} r \land l \|_{s} r = x))$
12	11	ralrimiva	$⊢ (A \in On \land B \in On \land A \subseteq B) \to \forall x \in No (\exists l \in 𝒫 ⋃ M [A] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x) \to \exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [B] (l ≪_{s} r \land l \|_{s} r = x))$
13		ss2rab	$⊢ \{x \in No \| \exists l \in 𝒫 ⋃ M [A] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x)\} \subseteq \{x \in No \| \exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [B] (l ≪_{s} r \land l \|_{s} r = x)\} \leftrightarrow \forall x \in No (\exists l \in 𝒫 ⋃ M [A] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x) \to \exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [B] (l ≪_{s} r \land l \|_{s} r = x))$
14	12 13	sylibr	$⊢ (A \in On \land B \in On \land A \subseteq B) \to \{x \in No \| \exists l \in 𝒫 ⋃ M [A] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x)\} \subseteq \{x \in No \| \exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [B] (l ≪_{s} r \land l \|_{s} r = x)\}$
15		madeval2	$⊢ A \in On \to M (A) = \{x \in No \| \exists l \in 𝒫 ⋃ M [A] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x)\}$
16	15	3ad2ant1	$⊢ (A \in On \land B \in On \land A \subseteq B) \to M (A) = \{x \in No \| \exists l \in 𝒫 ⋃ M [A] \exists r \in 𝒫 ⋃ M [A] (l ≪_{s} r \land l \|_{s} r = x)\}$
17		madeval2	$⊢ B \in On \to M (B) = \{x \in No \| \exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [B] (l ≪_{s} r \land l \|_{s} r = x)\}$
18	17	3ad2ant2	$⊢ (A \in On \land B \in On \land A \subseteq B) \to M (B) = \{x \in No \| \exists l \in 𝒫 ⋃ M [B] \exists r \in 𝒫 ⋃ M [B] (l ≪_{s} r \land l \|_{s} r = x)\}$
19	14 16 18	3sstr4d	$⊢ (A \in On \land B \in On \land A \subseteq B) \to M (A) \subseteq M (B)$