Metamath Proof Explorer

Theorem oaun3lem4

Description: The class of all ordinal sums of elements from two ordinals is less than the successor to the sum. Lemma for oaun3 . (Contributed by RP, 12-Feb-2025)

		Ref	Expression
	Assertion	oaun3lem4	$⊢ (A \in On \land B \in On) \to \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \in suc (A +_{𝑜} B)$

Proof

Step	Hyp	Ref	Expression
1		oaun3lem2	$⊢ (A \in On \land B \in On) \to \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \subseteq A +_{𝑜} B$
2		oaun3lem3	$⊢ (A \in On \land B \in On) \to \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \in On$
3		oacl	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B \in On$
4		onsssuc	$⊢ (\{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \in On \land A +_{𝑜} B \in On) \to (\{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \subseteq A +_{𝑜} B \leftrightarrow \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \in suc (A +_{𝑜} B))$
5	2 3 4	syl2anc	$⊢ (A \in On \land B \in On) \to (\{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \subseteq A +_{𝑜} B \leftrightarrow \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \in suc (A +_{𝑜} B))$
6	1 5	mpbid	$⊢ (A \in On \land B \in On) \to \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \in suc (A +_{𝑜} B)$