oaun3lem1

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

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

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ a (A \in On \land B \in On)$
2		nfcv	$⊢ \underline{Ⅎ} a y$
3		nfre1	$⊢ Ⅎ a \exists a \in A \exists b \in B x = a +_{𝑜} b$
4	3	nfsab	$⊢ Ⅎ a z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
5	2 4	nfralw	$⊢ Ⅎ a \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
6		nfv	$⊢ Ⅎ b ((A \in On \land B \in On) \land a \in A)$
7		nfcv	$⊢ \underline{Ⅎ} b y$
8		nfcv	$⊢ \underline{Ⅎ} b A$
9		nfre1	$⊢ Ⅎ b \exists b \in B x = a +_{𝑜} b$
10	8 9	nfrexw	$⊢ Ⅎ b \exists a \in A \exists b \in B x = a +_{𝑜} b$
11	10	nfsab	$⊢ Ⅎ b z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
12	7 11	nfralw	$⊢ Ⅎ b \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
13		simp-4l	$⊢ ((((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \land z \in a) \to A \in On$
14		simplrl	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to a \in A$
15	14	anim1ci	$⊢ ((((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \land z \in a) \to (z \in a \land a \in A)$
16		ontr1	$⊢ A \in On \to ((z \in a \land a \in A) \to z \in A)$
17	13 15 16	sylc	$⊢ ((((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \land z \in a) \to z \in A$
18		simpr	$⊢ (A \in On \land B \in On) \to B \in On$
19		ne0i	$⊢ b \in B \to B \neq \emptyset$
20	19	adantl	$⊢ (a \in A \land b \in B) \to B \neq \emptyset$
21		on0eln0	$⊢ B \in On \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
22	21	biimpar	$⊢ (B \in On \land B \neq \emptyset) \to \emptyset \in B$
23	18 20 22	syl2an	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to \emptyset \in B$
24		onelon	$⊢ (A \in On \land a \in A) \to a \in On$
25	24	ad2ant2r	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a \in On$
26		simpr	$⊢ (a \in A \land b \in B) \to b \in B$
27		onelon	$⊢ (B \in On \land b \in B) \to b \in On$
28	18 26 27	syl2an	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to b \in On$
29		oacl	$⊢ (a \in On \land b \in On) \to a +_{𝑜} b \in On$
30	25 28 29	syl2anc	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a +_{𝑜} b \in On$
31		onelon	$⊢ (a +_{𝑜} b \in On \land z \in (a +_{𝑜} b)) \to z \in On$
32	30 31	sylan	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to z \in On$
33		oa0	$⊢ z \in On \to z +_{𝑜} \emptyset = z$
34	32 33	syl	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to z +_{𝑜} \emptyset = z$
35	34	eqcomd	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to z = z +_{𝑜} \emptyset$
36		oveq2	$⊢ y = \emptyset \to z +_{𝑜} y = z +_{𝑜} \emptyset$
37	36	rspceeqv	$⊢ (\emptyset \in B \land z = z +_{𝑜} \emptyset) \to \exists y \in B z = z +_{𝑜} y$
38	23 35 37	syl2an2r	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to \exists y \in B z = z +_{𝑜} y$
39	38	adantr	$⊢ ((((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \land z \in a) \to \exists y \in B z = z +_{𝑜} y$
40		oveq1	$⊢ w = z \to w +_{𝑜} y = z +_{𝑜} y$
41	40	eqeq2d	$⊢ w = z \to (z = w +_{𝑜} y \leftrightarrow z = z +_{𝑜} y)$
42	41	rexbidv	$⊢ w = z \to (\exists y \in B z = w +_{𝑜} y \leftrightarrow \exists y \in B z = z +_{𝑜} y)$
43	42	rspcev	$⊢ (z \in A \land \exists y \in B z = z +_{𝑜} y) \to \exists w \in A \exists y \in B z = w +_{𝑜} y$
44	17 39 43	syl2anc	$⊢ ((((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \land z \in a) \to \exists w \in A \exists y \in B z = w +_{𝑜} y$
45	18	adantr	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to B \in On$
46	25 45	jca	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to (a \in On \land B \in On)$
47	46	adantr	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to (a \in On \land B \in On)$
48		oacl	$⊢ (a \in On \land B \in On) \to a +_{𝑜} B \in On$
49	25 45 48	syl2anc	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a +_{𝑜} B \in On$
50		eloni	$⊢ a +_{𝑜} b \in On \to Ord (a +_{𝑜} b)$
51		eloni	$⊢ a +_{𝑜} B \in On \to Ord (a +_{𝑜} B)$
52	50 51	anim12i	$⊢ (a +_{𝑜} b \in On \land a +_{𝑜} B \in On) \to (Ord (a +_{𝑜} b) \land Ord (a +_{𝑜} B))$
53	30 49 52	syl2anc	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to (Ord (a +_{𝑜} b) \land Ord (a +_{𝑜} B))$
54	45 25	jca	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to (B \in On \land a \in On)$
55	26	adantl	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to b \in B$
56		oaordi	$⊢ (B \in On \land a \in On) \to (b \in B \to a +_{𝑜} b \in (a +_{𝑜} B))$
57	54 55 56	sylc	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a +_{𝑜} b \in (a +_{𝑜} B)$
58		ordelpss	$⊢ (Ord (a +_{𝑜} b) \land Ord (a +_{𝑜} B)) \to (a +_{𝑜} b \in (a +_{𝑜} B) \leftrightarrow a +_{𝑜} b \subset a +_{𝑜} B)$
59	58	biimpd	$⊢ (Ord (a +_{𝑜} b) \land Ord (a +_{𝑜} B)) \to (a +_{𝑜} b \in (a +_{𝑜} B) \to a +_{𝑜} b \subset a +_{𝑜} B)$
60	53 57 59	sylc	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a +_{𝑜} b \subset a +_{𝑜} B$
61	60	pssssd	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to a +_{𝑜} b \subseteq a +_{𝑜} B$
62	61	sselda	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to z \in (a +_{𝑜} B)$
63	62	anim1ci	$⊢ ((((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \land a \subseteq z) \to (a \subseteq z \land z \in (a +_{𝑜} B))$
64		oawordex2	$⊢ ((a \in On \land B \in On) \land (a \subseteq z \land z \in (a +_{𝑜} B))) \to \exists y \in B a +_{𝑜} y = z$
65	47 63 64	syl2an2r	$⊢ ((((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \land a \subseteq z) \to \exists y \in B a +_{𝑜} y = z$
66		oveq1	$⊢ w = a \to w +_{𝑜} y = a +_{𝑜} y$
67	66	eqeq2d	$⊢ w = a \to (z = w +_{𝑜} y \leftrightarrow z = a +_{𝑜} y)$
68		eqcom	$⊢ z = a +_{𝑜} y \leftrightarrow a +_{𝑜} y = z$
69	67 68	bitrdi	$⊢ w = a \to (z = w +_{𝑜} y \leftrightarrow a +_{𝑜} y = z)$
70	69	rexbidv	$⊢ w = a \to (\exists y \in B z = w +_{𝑜} y \leftrightarrow \exists y \in B a +_{𝑜} y = z)$
71	70	rspcev	$⊢ (a \in A \land \exists y \in B a +_{𝑜} y = z) \to \exists w \in A \exists y \in B z = w +_{𝑜} y$
72	14 65 71	syl2an2r	$⊢ ((((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \land a \subseteq z) \to \exists w \in A \exists y \in B z = w +_{𝑜} y$
73		eloni	$⊢ z \in On \to Ord z$
74	32 73	syl	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to Ord z$
75		eloni	$⊢ a \in On \to Ord a$
76	25 75	syl	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to Ord a$
77	76	adantr	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to Ord a$
78		ordtri2or	$⊢ (Ord z \land Ord a) \to (z \in a \lor a \subseteq z)$
79	74 77 78	syl2anc	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to (z \in a \lor a \subseteq z)$
80	44 72 79	mpjaodan	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to \exists w \in A \exists y \in B z = w +_{𝑜} y$
81		vex	$⊢ z \in V$
82		eqeq1	$⊢ x = z \to (x = a +_{𝑜} b \leftrightarrow z = a +_{𝑜} b)$
83	82	2rexbidv	$⊢ x = z \to (\exists a \in A \exists b \in B x = a +_{𝑜} b \leftrightarrow \exists a \in A \exists b \in B z = a +_{𝑜} b)$
84		oveq1	$⊢ a = w \to a +_{𝑜} b = w +_{𝑜} b$
85	84	eqeq2d	$⊢ a = w \to (z = a +_{𝑜} b \leftrightarrow z = w +_{𝑜} b)$
86		oveq2	$⊢ b = y \to w +_{𝑜} b = w +_{𝑜} y$
87	86	eqeq2d	$⊢ b = y \to (z = w +_{𝑜} b \leftrightarrow z = w +_{𝑜} y)$
88	85 87	cbvrex2vw	$⊢ \exists a \in A \exists b \in B z = a +_{𝑜} b \leftrightarrow \exists w \in A \exists y \in B z = w +_{𝑜} y$
89	83 88	bitrdi	$⊢ x = z \to (\exists a \in A \exists b \in B x = a +_{𝑜} b \leftrightarrow \exists w \in A \exists y \in B z = w +_{𝑜} y)$
90	81 89	elab	$⊢ z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \leftrightarrow \exists w \in A \exists y \in B z = w +_{𝑜} y$
91	80 90	sylibr	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land z \in (a +_{𝑜} b)) \to z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
92	91	ralrimiva	$⊢ ((A \in On \land B \in On) \land (a \in A \land b \in B)) \to \forall z \in (a +_{𝑜} b) z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
93	92	adantr	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land y = a +_{𝑜} b) \to \forall z \in (a +_{𝑜} b) z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
94		simpr	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land y = a +_{𝑜} b) \to y = a +_{𝑜} b$
95	93 94	raleqtrrdv	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land y = a +_{𝑜} b) \to \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
96	95	exp31	$⊢ (A \in On \land B \in On) \to ((a \in A \land b \in B) \to (y = a +_{𝑜} b \to \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}))$
97	96	expdimp	$⊢ ((A \in On \land B \in On) \land a \in A) \to (b \in B \to (y = a +_{𝑜} b \to \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}))$
98	6 12 97	rexlimd	$⊢ ((A \in On \land B \in On) \land a \in A) \to (\exists b \in B y = a +_{𝑜} b \to \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\})$
99	98	ex	$⊢ (A \in On \land B \in On) \to (a \in A \to (\exists b \in B y = a +_{𝑜} b \to \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}))$
100	1 5 99	rexlimd	$⊢ (A \in On \land B \in On) \to (\exists a \in A \exists b \in B y = a +_{𝑜} b \to \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\})$
101	100	alrimiv	$⊢ (A \in On \land B \in On) \to \forall y (\exists a \in A \exists b \in B y = a +_{𝑜} b \to \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\})$
102		eqeq1	$⊢ x = y \to (x = a +_{𝑜} b \leftrightarrow y = a +_{𝑜} b)$
103	102	2rexbidv	$⊢ x = y \to (\exists a \in A \exists b \in B x = a +_{𝑜} b \leftrightarrow \exists a \in A \exists b \in B y = a +_{𝑜} b)$
104	103	ralab	$⊢ \forall y \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \leftrightarrow \forall y (\exists a \in A \exists b \in B y = a +_{𝑜} b \to \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\})$
105	101 104	sylibr	$⊢ (A \in On \land B \in On) \to \forall y \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
106		dftr5	$⊢ Tr \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \leftrightarrow \forall y \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \forall z \in y z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
107	105 106	sylibr	$⊢ (A \in On \land B \in On) \to Tr \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
108		simpr	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land x = a +_{𝑜} b) \to x = a +_{𝑜} b$
109	30	adantr	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land x = a +_{𝑜} b) \to a +_{𝑜} b \in On$
110	108 109	eqeltrd	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land x = a +_{𝑜} b) \to x \in On$
111	110	exp31	$⊢ (A \in On \land B \in On) \to ((a \in A \land b \in B) \to (x = a +_{𝑜} b \to x \in On))$
112	111	rexlimdvv	$⊢ (A \in On \land B \in On) \to (\exists a \in A \exists b \in B x = a +_{𝑜} b \to x \in On)$
113	112	abssdv	$⊢ (A \in On \land B \in On) \to \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \subseteq On$
114		epweon	$⊢ E We On$
115		wess	$⊢ \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \subseteq On \to (E We On \to E We \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\})$
116	113 114 115	mpisyl	$⊢ (A \in On \land B \in On) \to E We \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
117		df-ord	$⊢ Ord \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \leftrightarrow (Tr \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \land E We \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\})$
118	107 116 117	sylanbrc	$⊢ (A \in On \land B \in On) \to Ord \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$

Metamath Proof Explorer

Theorem oaun3lem1

Proof