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	94	raleqdv	$⊢ (((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\} \leftrightarrow \forall z \in (a +_{𝑜} b) z \in \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\})$
96	93 95	mpbird	$⊢ (((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\}$
97	96	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\}))$
98	97	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\}))$
99	6 12 98	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\})$
100	99	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\}))$
101	1 5 100	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\})$
102	101	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\})$
103		eqeq1	$⊢ x = y \to (x = a +_{𝑜} b \leftrightarrow y = a +_{𝑜} b)$
104	103	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)$
105	104	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\})$
106	102 105	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\}$
107		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\}$
108	106 107	sylibr	$⊢ (A \in On \land B \in On) \to Tr \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
109		simpr	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land x = a +_{𝑜} b) \to x = a +_{𝑜} b$
110	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$
111	109 110	eqeltrd	$⊢ (((A \in On \land B \in On) \land (a \in A \land b \in B)) \land x = a +_{𝑜} b) \to x \in On$
112	111	exp31	$⊢ (A \in On \land B \in On) \to ((a \in A \land b \in B) \to (x = a +_{𝑜} b \to x \in On))$
113	112	rexlimdvv	$⊢ (A \in On \land B \in On) \to (\exists a \in A \exists b \in B x = a +_{𝑜} b \to x \in On)$
114	113	abssdv	$⊢ (A \in On \land B \in On) \to \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\} \subseteq On$
115		epweon	$⊢ E We On$
116		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\})$
117	114 115 116	mpisyl	$⊢ (A \in On \land B \in On) \to E We \{x \| \exists a \in A \exists b \in B x = a +_{𝑜} b\}$
118		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\})$
119	108 117 118	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