oaun3lem2

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

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land x = a +_{𝑜} b) \to x = a +_{𝑜} b$
2		onelon	$⊢ (A \in On \land a \in A) \to a \in On$
3	2	ad2ant2r	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a \in On$
4		onelon	$⊢ (B \in On \land b \in B) \to b \in On$
5	4	ad2ant2l	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to b \in On$
6		oacl	$⊢ (a \in On \land b \in On) \to a +_{𝑜} b \in On$
7	3 5 6	syl2anc	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a +_{𝑜} b \in On$
8		oacl	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B \in On$
9	8	adantr	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to A +_{𝑜} B \in On$
10	7 9	jca	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to (a +_{𝑜} b \in On \land A +_{𝑜} B \in On)$
11		simpl	$⊢ (A \in On \land B \in On) \to A \in On$
12	11	adantr	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to A \in On$
13	3 12 5	3jca	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to (a \in On \land A \in On \land b \in On)$
14		simpl	$⊢ (a \in A \land b \in B) \to a \in A$
15	14	adantl	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a \in A$
16		eloni	$⊢ a \in On \to Ord a$
17		eloni	$⊢ A \in On \to Ord A$
18	16 17	anim12i	$⊢ (a \in On \land A \in On) \to (Ord a \land Ord A)$
19	3 12 18	syl2anc	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to (Ord a \land Ord A)$
20		ordelpss	$⊢ (Ord a \land Ord A) \to (a \in A \leftrightarrow a \subset A)$
21	19 20	syl	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to (a \in A \leftrightarrow a \subset A)$
22	15 21	mpbid	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a \subset A$
23	22	pssssd	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a \subseteq A$
24		oawordri	$⊢ (a \in On \land A \in On \land b \in On) \to (a \subseteq A \to a +_{𝑜} b \subseteq A +_{𝑜} b)$
25	13 23 24	sylc	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a +_{𝑜} b \subseteq A +_{𝑜} b$
26		pm3.22	$⊢ (A \in On \land B \in On) \to (B \in On \land A \in On)$
27	26	adantr	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to (B \in On \land A \in On)$
28		simpr	$⊢ (a \in A \land b \in B) \to b \in B$
29	28	adantl	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to b \in B$
30		oaordi	$⊢ (B \in On \land A \in On) \to (b \in B \to A +_{𝑜} b \in (A +_{𝑜} B))$
31	27 29 30	sylc	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to A +_{𝑜} b \in (A +_{𝑜} B)$
32	25 31	jca	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to (a +_{𝑜} b \subseteq A +_{𝑜} b \land A +_{𝑜} b \in (A +_{𝑜} B))$
33		ontr2	$⊢ (a +_{𝑜} b \in On \land A +_{𝑜} B \in On) \to ((a +_{𝑜} b \subseteq A +_{𝑜} b \land A +_{𝑜} b \in (A +_{𝑜} B)) \to a +_{𝑜} b \in (A +_{𝑜} B))$
34	10 32 33	sylc	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a +_{𝑜} b \in (A +_{𝑜} B)$
35	34	adantr	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land x = a +_{𝑜} b) \to a +_{𝑜} b \in (A +_{𝑜} B)$
36	1 35	eqeltrd	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land x = a +_{𝑜} b) \to x \in (A +_{𝑜} B)$
37	36	exp31	$⊢ (A \in On \land B \in On) \to ((a \in A \land b \in B) \to (x = a +_{𝑜} b \to x \in (A +_{𝑜} B)))$
38	37	rexlimdvv	$⊢ (A \in On \land B \in On) \to (\exists a \in A \exists b \in B x = a +_{𝑜} b \to x \in (A +_{𝑜} B))$
39	38	abssdv	$⊢ (A \in On \land B \in On) \to \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \subseteq A +_{𝑜} B$

Metamath Proof Explorer

Theorem oaun3lem2

Proof