oaabs2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > oaabs2		Structured version Visualization version GIF version

Theorem oaabs2 8687

Description: The absorption law oaabs 8686 is also a property of higher powers of ω. (Contributed by Mario Carneiro, 29-May-2015.)

**Assertion**
Ref	Expression
oaabs2	⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (𝐴 +_o 𝐵) = 𝐵)

Proof of Theorem oaabs2 Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		n0i 4340	. . . . . . 7 ⊢ (𝐴 ∈ (ω ↑_o 𝐶) → ¬ (ω ↑_o 𝐶) = ∅)
2		fnoe 8548	. . . . . . . . 9 ⊢ ↑_o Fn (On × On)
3		fndm 6671	. . . . . . . . 9 ⊢ ( ↑_o Fn (On × On) → dom ↑_o = (On × On))
4	2, 3	ax-mp 5	. . . . . . . 8 ⊢ dom ↑_o = (On × On)
5	4	ndmov 7617	. . . . . . 7 ⊢ (¬ (ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑_o 𝐶) = ∅)
6	1, 5	nsyl2 141	. . . . . 6 ⊢ (𝐴 ∈ (ω ↑_o 𝐶) → (ω ∈ On ∧ 𝐶 ∈ On))
7	6	ad2antrr 726	. . . . 5 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (ω ∈ On ∧ 𝐶 ∈ On))
8		oecl 8575	. . . . 5 ⊢ ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑_o 𝐶) ∈ On)
9	7, 8	syl 17	. . . 4 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (ω ↑_o 𝐶) ∈ On)
10		simplr 769	. . . 4 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → 𝐵 ∈ On)
11		simpr 484	. . . 4 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (ω ↑_o 𝐶) ⊆ 𝐵)
12		oawordeu 8593	. . . 4 ⊢ ((((ω ↑_o 𝐶) ∈ On ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑_o 𝐶) +_o 𝑥) = 𝐵)
13	9, 10, 11, 12	syl21anc 838	. . 3 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → ∃!𝑥 ∈ On ((ω ↑_o 𝐶) +_o 𝑥) = 𝐵)
14		reurex 3384	. . 3 ⊢ (∃!𝑥 ∈ On ((ω ↑_o 𝐶) +_o 𝑥) = 𝐵 → ∃𝑥 ∈ On ((ω ↑_o 𝐶) +_o 𝑥) = 𝐵)
15	13, 14	syl 17	. 2 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → ∃𝑥 ∈ On ((ω ↑_o 𝐶) +_o 𝑥) = 𝐵)
16		simpll 767	. . . . . . . 8 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → 𝐴 ∈ (ω ↑_o 𝐶))
17		onelon 6409	. . . . . . . 8 ⊢ (((ω ↑_o 𝐶) ∈ On ∧ 𝐴 ∈ (ω ↑_o 𝐶)) → 𝐴 ∈ On)
18	9, 16, 17	syl2anc 584	. . . . . . 7 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → 𝐴 ∈ On)
19	18	adantr 480	. . . . . 6 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝐴 ∈ On)
20	9	adantr 480	. . . . . 6 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (ω ↑_o 𝐶) ∈ On)
21		simpr 484	. . . . . 6 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
22		oaass 8599	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ (ω ↑_o 𝐶) ∈ On ∧ 𝑥 ∈ On) → ((𝐴 +_o (ω ↑_o 𝐶)) +_o 𝑥) = (𝐴 +_o ((ω ↑_o 𝐶) +_o 𝑥)))
23	19, 20, 21, 22	syl3anc 1373	. . . . 5 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +_o (ω ↑_o 𝐶)) +_o 𝑥) = (𝐴 +_o ((ω ↑_o 𝐶) +_o 𝑥)))
24	7	simprd 495	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → 𝐶 ∈ On)
25		eloni 6394	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → Ord 𝐶)
26	24, 25	syl 17	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → Ord 𝐶)
27		ordzsl 7866	. . . . . . . . 9 ⊢ (Ord 𝐶 ↔ (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
28	26, 27	sylib 218	. . . . . . . 8 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶))
29		simplll 775	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ (ω ↑_o 𝐶))
30		oveq2 7439	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = ∅ → (ω ↑_o 𝐶) = (ω ↑_o ∅))
31	7	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → ω ∈ On)
32		oe0 8560	. . . . . . . . . . . . . . . 16 ⊢ (ω ∈ On → (ω ↑_o ∅) = 1_o)
33	31, 32	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (ω ↑_o ∅) = 1_o)
34	30, 33	sylan9eqr 2799	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑_o 𝐶) = 1_o)
35	29, 34	eleqtrd 2843	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 ∈ 1_o)
36		el1o 8533	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 1_o ↔ 𝐴 = ∅)
37	35, 36	sylib 218	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → 𝐴 = ∅)
38	37	oveq1d 7446	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +_o (ω ↑_o 𝐶)) = (∅ +_o (ω ↑_o 𝐶)))
39	9	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (ω ↑_o 𝐶) ∈ On)
40		oa0r 8576	. . . . . . . . . . . 12 ⊢ ((ω ↑_o 𝐶) ∈ On → (∅ +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶))
41	39, 40	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (∅ +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶))
42	38, 41	eqtrd 2777	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝐶 = ∅) → (𝐴 +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶))
43	42	ex 412	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (𝐶 = ∅ → (𝐴 +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶)))
44	31	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ω ∈ On)
45		simprl 771	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝑥 ∈ On)
46		oecl 8575	. . . . . . . . . . . . . 14 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑_o 𝑥) ∈ On)
47	44, 45, 46	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑_o 𝑥) ∈ On)
48		limom 7903	. . . . . . . . . . . . . 14 ⊢ Lim ω
49	44, 48	jctir 520	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ∈ On ∧ Lim ω))
50		simplll 775	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ (ω ↑_o 𝐶))
51		simprr 773	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐶 = suc 𝑥)
52	51	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑_o 𝐶) = (ω ↑_o suc 𝑥))
53		oesuc 8565	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑_o suc 𝑥) = ((ω ↑_o 𝑥) ·_o ω))
54	44, 45, 53	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑_o suc 𝑥) = ((ω ↑_o 𝑥) ·_o ω))
55	52, 54	eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑_o 𝐶) = ((ω ↑_o 𝑥) ·_o ω))
56	50, 55	eleqtrd 2843	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → 𝐴 ∈ ((ω ↑_o 𝑥) ·_o ω))
57		omordlim 8615	. . . . . . . . . . . . 13 ⊢ ((((ω ↑_o 𝑥) ∈ On ∧ (ω ∈ On ∧ Lim ω)) ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o ω)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))
58	47, 49, 56, 57	syl21anc 838	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → ∃𝑦 ∈ ω 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))
59	47	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → (ω ↑_o 𝑥) ∈ On)
60		nnon 7893	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
61	60	ad2antrl 728	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → 𝑦 ∈ On)
62		omcl 8574	. . . . . . . . . . . . . . . . 17 ⊢ (((ω ↑_o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑_o 𝑥) ·_o 𝑦) ∈ On)
63	59, 61, 62	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → ((ω ↑_o 𝑥) ·_o 𝑦) ∈ On)
64		eloni 6394	. . . . . . . . . . . . . . . 16 ⊢ (((ω ↑_o 𝑥) ·_o 𝑦) ∈ On → Ord ((ω ↑_o 𝑥) ·_o 𝑦))
65	63, 64	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → Ord ((ω ↑_o 𝑥) ·_o 𝑦))
66		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))
67		ordelss 6400	. . . . . . . . . . . . . . 15 ⊢ ((Ord ((ω ↑_o 𝑥) ·_o 𝑦) ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦)) → 𝐴 ⊆ ((ω ↑_o 𝑥) ·_o 𝑦))
68	65, 66, 67	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → 𝐴 ⊆ ((ω ↑_o 𝑥) ·_o 𝑦))
69	18	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → 𝐴 ∈ On)
70	9	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → (ω ↑_o 𝐶) ∈ On)
71		oawordri 8588	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ On ∧ ((ω ↑_o 𝑥) ·_o 𝑦) ∈ On ∧ (ω ↑_o 𝐶) ∈ On) → (𝐴 ⊆ ((ω ↑_o 𝑥) ·_o 𝑦) → (𝐴 +_o (ω ↑_o 𝐶)) ⊆ (((ω ↑_o 𝑥) ·_o 𝑦) +_o (ω ↑_o 𝐶))))
72	69, 63, 70, 71	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → (𝐴 ⊆ ((ω ↑_o 𝑥) ·_o 𝑦) → (𝐴 +_o (ω ↑_o 𝐶)) ⊆ (((ω ↑_o 𝑥) ·_o 𝑦) +_o (ω ↑_o 𝐶))))
73	68, 72	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → (𝐴 +_o (ω ↑_o 𝐶)) ⊆ (((ω ↑_o 𝑥) ·_o 𝑦) +_o (ω ↑_o 𝐶)))
74	44	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → ω ∈ On)
75		odi 8617	. . . . . . . . . . . . . . . 16 ⊢ (((ω ↑_o 𝑥) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On) → ((ω ↑_o 𝑥) ·_o (𝑦 +_o ω)) = (((ω ↑_o 𝑥) ·_o 𝑦) +_o ((ω ↑_o 𝑥) ·_o ω)))
76	59, 61, 74, 75	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → ((ω ↑_o 𝑥) ·_o (𝑦 +_o ω)) = (((ω ↑_o 𝑥) ·_o 𝑦) +_o ((ω ↑_o 𝑥) ·_o ω)))
77		simprl 771	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → 𝑦 ∈ ω)
78		oaabslem 8685	. . . . . . . . . . . . . . . . 17 ⊢ ((ω ∈ On ∧ 𝑦 ∈ ω) → (𝑦 +_o ω) = ω)
79	74, 77, 78	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → (𝑦 +_o ω) = ω)
80	79	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → ((ω ↑_o 𝑥) ·_o (𝑦 +_o ω)) = ((ω ↑_o 𝑥) ·_o ω))
81	76, 80	eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → (((ω ↑_o 𝑥) ·_o 𝑦) +_o ((ω ↑_o 𝑥) ·_o ω)) = ((ω ↑_o 𝑥) ·_o ω))
82	55	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → (ω ↑_o 𝐶) = ((ω ↑_o 𝑥) ·_o ω))
83	82	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → (((ω ↑_o 𝑥) ·_o 𝑦) +_o (ω ↑_o 𝐶)) = (((ω ↑_o 𝑥) ·_o 𝑦) +_o ((ω ↑_o 𝑥) ·_o ω)))
84	81, 83, 82	3eqtr4d 2787	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → (((ω ↑_o 𝑥) ·_o 𝑦) +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶))
85	73, 84	sseqtrd 4020	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ((ω ↑_o 𝑥) ·_o 𝑦))) → (𝐴 +_o (ω ↑_o 𝐶)) ⊆ (ω ↑_o 𝐶))
86	58, 85	rexlimddv 3161	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +_o (ω ↑_o 𝐶)) ⊆ (ω ↑_o 𝐶))
87		oaword2 8591	. . . . . . . . . . . . 13 ⊢ (((ω ↑_o 𝐶) ∈ On ∧ 𝐴 ∈ On) → (ω ↑_o 𝐶) ⊆ (𝐴 +_o (ω ↑_o 𝐶)))
88	9, 18, 87	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (ω ↑_o 𝐶) ⊆ (𝐴 +_o (ω ↑_o 𝐶)))
89	88	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (ω ↑_o 𝐶) ⊆ (𝐴 +_o (ω ↑_o 𝐶)))
90	86, 89	eqssd 4001	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ (𝑥 ∈ On ∧ 𝐶 = suc 𝑥)) → (𝐴 +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶))
91	90	rexlimdvaa 3156	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On 𝐶 = suc 𝑥 → (𝐴 +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶)))
92		simplll 775	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ (ω ↑_o 𝐶))
93	31	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ω ∈ On)
94	24	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐶 ∈ On)
95		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → Lim 𝐶)
96		oelim2 8633	. . . . . . . . . . . . . . 15 ⊢ ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑_o 𝐶) = ∪ 𝑥 ∈ (𝐶 ∖ 1_o)(ω ↑_o 𝑥))
97	93, 94, 95, 96	syl12anc 837	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑_o 𝐶) = ∪ 𝑥 ∈ (𝐶 ∖ 1_o)(ω ↑_o 𝑥))
98	92, 97	eleqtrd 2843	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → 𝐴 ∈ ∪ 𝑥 ∈ (𝐶 ∖ 1_o)(ω ↑_o 𝑥))
99		eliun 4995	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ (𝐶 ∖ 1_o)(ω ↑_o 𝑥) ↔ ∃𝑥 ∈ (𝐶 ∖ 1_o)𝐴 ∈ (ω ↑_o 𝑥))
100	98, 99	sylib 218	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → ∃𝑥 ∈ (𝐶 ∖ 1_o)𝐴 ∈ (ω ↑_o 𝑥))
101		eldifi 4131	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐶 ∖ 1_o) → 𝑥 ∈ 𝐶)
102	18	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → 𝐴 ∈ On)
103	9	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → (ω ↑_o 𝐶) ∈ On)
104	93	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → ω ∈ On)
105		1onn 8678	. . . . . . . . . . . . . . . . . . 19 ⊢ 1_o ∈ ω
106		ondif2 8540	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ∈ (On ∖ 2_o) ↔ (ω ∈ On ∧ 1_o ∈ ω))
107	104, 105, 106	sylanblrc 590	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → ω ∈ (On ∖ 2_o))
108	94	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → 𝐶 ∈ On)
109		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → Lim 𝐶)
110		oelimcl 8638	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ (On ∖ 2_o) ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → Lim (ω ↑_o 𝐶))
111	107, 108, 109, 110	syl12anc 837	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → Lim (ω ↑_o 𝐶))
112		oalim 8570	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ On ∧ ((ω ↑_o 𝐶) ∈ On ∧ Lim (ω ↑_o 𝐶))) → (𝐴 +_o (ω ↑_o 𝐶)) = ∪ 𝑦 ∈ (ω ↑_o 𝐶)(𝐴 +_o 𝑦))
113	102, 103, 111, 112	syl12anc 837	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → (𝐴 +_o (ω ↑_o 𝐶)) = ∪ 𝑦 ∈ (ω ↑_o 𝐶)(𝐴 +_o 𝑦))
114		oelim2 8633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ (𝐶 ∈ On ∧ Lim 𝐶)) → (ω ↑_o 𝐶) = ∪ 𝑧 ∈ (𝐶 ∖ 1_o)(ω ↑_o 𝑧))
115	93, 94, 95, 114	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑_o 𝐶) = ∪ 𝑧 ∈ (𝐶 ∖ 1_o)(ω ↑_o 𝑧))
116	115	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑_o 𝐶) ↔ 𝑦 ∈ ∪ 𝑧 ∈ (𝐶 ∖ 1_o)(ω ↑_o 𝑧)))
117		eliun 4995	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ∪ 𝑧 ∈ (𝐶 ∖ 1_o)(ω ↑_o 𝑧) ↔ ∃𝑧 ∈ (𝐶 ∖ 1_o)𝑦 ∈ (ω ↑_o 𝑧))
118	116, 117	bitrdi 287	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝑦 ∈ (ω ↑_o 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1_o)𝑦 ∈ (ω ↑_o 𝑧)))
119	118	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → (𝑦 ∈ (ω ↑_o 𝐶) ↔ ∃𝑧 ∈ (𝐶 ∖ 1_o)𝑦 ∈ (ω ↑_o 𝑧)))
120		eldifi 4131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (𝐶 ∖ 1_o) → 𝑧 ∈ 𝐶)
121	104	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → ω ∈ On)
122	108	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝐶 ∈ On)
123		simplrl 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝑥 ∈ 𝐶)
124		onelon 6409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ On)
125	122, 123, 124	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝑥 ∈ On)
126	121, 125, 46	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (ω ↑_o 𝑥) ∈ On)
127		eloni 6394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ω ↑_o 𝑥) ∈ On → Ord (ω ↑_o 𝑥))
128	126, 127	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → Ord (ω ↑_o 𝑥))
129		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝐴 ∈ (ω ↑_o 𝑥))
130		ordelss 6400	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((Ord (ω ↑_o 𝑥) ∧ 𝐴 ∈ (ω ↑_o 𝑥)) → 𝐴 ⊆ (ω ↑_o 𝑥))
131	128, 129, 130	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝐴 ⊆ (ω ↑_o 𝑥))
132		ssun1 4178	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑥 ⊆ (𝑥 ∪ 𝑧)
133	26	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → Ord 𝐶)
134		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝑧 ∈ 𝐶)
135		ordunel 7847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((Ord 𝐶 ∧ 𝑥 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶) → (𝑥 ∪ 𝑧) ∈ 𝐶)
136	133, 123, 134, 135	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (𝑥 ∪ 𝑧) ∈ 𝐶)
137		onelon 6409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐶 ∈ On ∧ (𝑥 ∪ 𝑧) ∈ 𝐶) → (𝑥 ∪ 𝑧) ∈ On)
138	122, 136, 137	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (𝑥 ∪ 𝑧) ∈ On)
139		peano1 7910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∅ ∈ ω
140	139	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → ∅ ∈ ω)
141		oewordi 8629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑥 ∈ On ∧ (𝑥 ∪ 𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑥 ⊆ (𝑥 ∪ 𝑧) → (ω ↑_o 𝑥) ⊆ (ω ↑_o (𝑥 ∪ 𝑧))))
142	125, 138, 121, 140, 141	syl31anc 1375	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (𝑥 ⊆ (𝑥 ∪ 𝑧) → (ω ↑_o 𝑥) ⊆ (ω ↑_o (𝑥 ∪ 𝑧))))
143	132, 142	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (ω ↑_o 𝑥) ⊆ (ω ↑_o (𝑥 ∪ 𝑧)))
144	131, 143	sstrd 3994	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝐴 ⊆ (ω ↑_o (𝑥 ∪ 𝑧)))
145	102	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝐴 ∈ On)
146		oecl 8575	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ω ∈ On ∧ (𝑥 ∪ 𝑧) ∈ On) → (ω ↑_o (𝑥 ∪ 𝑧)) ∈ On)
147	121, 138, 146	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (ω ↑_o (𝑥 ∪ 𝑧)) ∈ On)
148		onelon 6409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐶 ∈ On ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ On)
149	122, 134, 148	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝑧 ∈ On)
150		oecl 8575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ω ∈ On ∧ 𝑧 ∈ On) → (ω ↑_o 𝑧) ∈ On)
151	121, 149, 150	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (ω ↑_o 𝑧) ∈ On)
152		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝑦 ∈ (ω ↑_o 𝑧))
153		onelon 6409	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ω ↑_o 𝑧) ∈ On ∧ 𝑦 ∈ (ω ↑_o 𝑧)) → 𝑦 ∈ On)
154	151, 152, 153	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝑦 ∈ On)
155		oawordri 8588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ On ∧ (ω ↑_o (𝑥 ∪ 𝑧)) ∈ On ∧ 𝑦 ∈ On) → (𝐴 ⊆ (ω ↑_o (𝑥 ∪ 𝑧)) → (𝐴 +_o 𝑦) ⊆ ((ω ↑_o (𝑥 ∪ 𝑧)) +_o 𝑦)))
156	145, 147, 154, 155	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (𝐴 ⊆ (ω ↑_o (𝑥 ∪ 𝑧)) → (𝐴 +_o 𝑦) ⊆ ((ω ↑_o (𝑥 ∪ 𝑧)) +_o 𝑦)))
157	144, 156	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (𝐴 +_o 𝑦) ⊆ ((ω ↑_o (𝑥 ∪ 𝑧)) +_o 𝑦))
158		eloni 6394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ω ↑_o 𝑧) ∈ On → Ord (ω ↑_o 𝑧))
159	151, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → Ord (ω ↑_o 𝑧))
160		ordelss 6400	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((Ord (ω ↑_o 𝑧) ∧ 𝑦 ∈ (ω ↑_o 𝑧)) → 𝑦 ⊆ (ω ↑_o 𝑧))
161	159, 152, 160	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝑦 ⊆ (ω ↑_o 𝑧))
162		ssun2 4179	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑧 ⊆ (𝑥 ∪ 𝑧)
163		oewordi 8629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑧 ∈ On ∧ (𝑥 ∪ 𝑧) ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (𝑧 ⊆ (𝑥 ∪ 𝑧) → (ω ↑_o 𝑧) ⊆ (ω ↑_o (𝑥 ∪ 𝑧))))
164	149, 138, 121, 140, 163	syl31anc 1375	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (𝑧 ⊆ (𝑥 ∪ 𝑧) → (ω ↑_o 𝑧) ⊆ (ω ↑_o (𝑥 ∪ 𝑧))))
165	162, 164	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (ω ↑_o 𝑧) ⊆ (ω ↑_o (𝑥 ∪ 𝑧)))
166	161, 165	sstrd 3994	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 𝑦 ⊆ (ω ↑_o (𝑥 ∪ 𝑧)))
167		oaword 8587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ On ∧ (ω ↑_o (𝑥 ∪ 𝑧)) ∈ On ∧ (ω ↑_o (𝑥 ∪ 𝑧)) ∈ On) → (𝑦 ⊆ (ω ↑_o (𝑥 ∪ 𝑧)) ↔ ((ω ↑_o (𝑥 ∪ 𝑧)) +_o 𝑦) ⊆ ((ω ↑_o (𝑥 ∪ 𝑧)) +_o (ω ↑_o (𝑥 ∪ 𝑧)))))
168	154, 147, 147, 167	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (𝑦 ⊆ (ω ↑_o (𝑥 ∪ 𝑧)) ↔ ((ω ↑_o (𝑥 ∪ 𝑧)) +_o 𝑦) ⊆ ((ω ↑_o (𝑥 ∪ 𝑧)) +_o (ω ↑_o (𝑥 ∪ 𝑧)))))
169	166, 168	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → ((ω ↑_o (𝑥 ∪ 𝑧)) +_o 𝑦) ⊆ ((ω ↑_o (𝑥 ∪ 𝑧)) +_o (ω ↑_o (𝑥 ∪ 𝑧))))
170	157, 169	sstrd 3994	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (𝐴 +_o 𝑦) ⊆ ((ω ↑_o (𝑥 ∪ 𝑧)) +_o (ω ↑_o (𝑥 ∪ 𝑧))))
171		ordom 7897	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ord ω
172		ordsucss 7838	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Ord ω → (1_o ∈ ω → suc 1_o ⊆ ω))
173	171, 105, 172	mp2 9	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ suc 1_o ⊆ ω
174		1on 8518	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1_o ∈ On
175		onsuc 7831	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (1_o ∈ On → suc 1_o ∈ On)
176	174, 175	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → suc 1_o ∈ On)
177		omwordi 8609	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((suc 1_o ∈ On ∧ ω ∈ On ∧ (ω ↑_o (𝑥 ∪ 𝑧)) ∈ On) → (suc 1_o ⊆ ω → ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o suc 1_o) ⊆ ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o ω)))
178	176, 121, 147, 177	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (suc 1_o ⊆ ω → ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o suc 1_o) ⊆ ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o ω)))
179	173, 178	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o suc 1_o) ⊆ ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o ω))
180	174	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → 1_o ∈ On)
181		omsuc 8564	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ω ↑_o (𝑥 ∪ 𝑧)) ∈ On ∧ 1_o ∈ On) → ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o suc 1_o) = (((ω ↑_o (𝑥 ∪ 𝑧)) ·_o 1_o) +_o (ω ↑_o (𝑥 ∪ 𝑧))))
182	147, 180, 181	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o suc 1_o) = (((ω ↑_o (𝑥 ∪ 𝑧)) ·_o 1_o) +_o (ω ↑_o (𝑥 ∪ 𝑧))))
183		om1 8580	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ω ↑_o (𝑥 ∪ 𝑧)) ∈ On → ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o 1_o) = (ω ↑_o (𝑥 ∪ 𝑧)))
184	147, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o 1_o) = (ω ↑_o (𝑥 ∪ 𝑧)))
185	184	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (((ω ↑_o (𝑥 ∪ 𝑧)) ·_o 1_o) +_o (ω ↑_o (𝑥 ∪ 𝑧))) = ((ω ↑_o (𝑥 ∪ 𝑧)) +_o (ω ↑_o (𝑥 ∪ 𝑧))))
186	182, 185	eqtr2d 2778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → ((ω ↑_o (𝑥 ∪ 𝑧)) +_o (ω ↑_o (𝑥 ∪ 𝑧))) = ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o suc 1_o))
187		oesuc 8565	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ω ∈ On ∧ (𝑥 ∪ 𝑧) ∈ On) → (ω ↑_o suc (𝑥 ∪ 𝑧)) = ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o ω))
188	121, 138, 187	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (ω ↑_o suc (𝑥 ∪ 𝑧)) = ((ω ↑_o (𝑥 ∪ 𝑧)) ·_o ω))
189	179, 186, 188	3sstr4d 4039	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → ((ω ↑_o (𝑥 ∪ 𝑧)) +_o (ω ↑_o (𝑥 ∪ 𝑧))) ⊆ (ω ↑_o suc (𝑥 ∪ 𝑧)))
190	170, 189	sstrd 3994	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (𝐴 +_o 𝑦) ⊆ (ω ↑_o suc (𝑥 ∪ 𝑧)))
191		ordsucss 7838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝐶 → ((𝑥 ∪ 𝑧) ∈ 𝐶 → suc (𝑥 ∪ 𝑧) ⊆ 𝐶))
192	133, 136, 191	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → suc (𝑥 ∪ 𝑧) ⊆ 𝐶)
193		onsuc 7831	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∪ 𝑧) ∈ On → suc (𝑥 ∪ 𝑧) ∈ On)
194	138, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → suc (𝑥 ∪ 𝑧) ∈ On)
195		oewordi 8629	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((suc (𝑥 ∪ 𝑧) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (suc (𝑥 ∪ 𝑧) ⊆ 𝐶 → (ω ↑_o suc (𝑥 ∪ 𝑧)) ⊆ (ω ↑_o 𝐶)))
196	194, 122, 121, 140, 195	syl31anc 1375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (suc (𝑥 ∪ 𝑧) ⊆ 𝐶 → (ω ↑_o suc (𝑥 ∪ 𝑧)) ⊆ (ω ↑_o 𝐶)))
197	192, 196	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (ω ↑_o suc (𝑥 ∪ 𝑧)) ⊆ (ω ↑_o 𝐶))
198	190, 197	sstrd 3994	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ (𝑧 ∈ 𝐶 ∧ 𝑦 ∈ (ω ↑_o 𝑧))) → (𝐴 +_o 𝑦) ⊆ (ω ↑_o 𝐶))
199	198	expr 456	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ 𝑧 ∈ 𝐶) → (𝑦 ∈ (ω ↑_o 𝑧) → (𝐴 +_o 𝑦) ⊆ (ω ↑_o 𝐶)))
200	120, 199	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) ∧ 𝑧 ∈ (𝐶 ∖ 1_o)) → (𝑦 ∈ (ω ↑_o 𝑧) → (𝐴 +_o 𝑦) ⊆ (ω ↑_o 𝐶)))
201	200	rexlimdva 3155	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → (∃𝑧 ∈ (𝐶 ∖ 1_o)𝑦 ∈ (ω ↑_o 𝑧) → (𝐴 +_o 𝑦) ⊆ (ω ↑_o 𝐶)))
202	119, 201	sylbid 240	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → (𝑦 ∈ (ω ↑_o 𝐶) → (𝐴 +_o 𝑦) ⊆ (ω ↑_o 𝐶)))
203	202	ralrimiv 3145	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → ∀𝑦 ∈ (ω ↑_o 𝐶)(𝐴 +_o 𝑦) ⊆ (ω ↑_o 𝐶))
204		iunss 5045	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑦 ∈ (ω ↑_o 𝐶)(𝐴 +_o 𝑦) ⊆ (ω ↑_o 𝐶) ↔ ∀𝑦 ∈ (ω ↑_o 𝐶)(𝐴 +_o 𝑦) ⊆ (ω ↑_o 𝐶))
205	203, 204	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → ∪ 𝑦 ∈ (ω ↑_o 𝐶)(𝐴 +_o 𝑦) ⊆ (ω ↑_o 𝐶))
206	113, 205	eqsstrd 4018	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝐴 ∈ (ω ↑_o 𝑥))) → (𝐴 +_o (ω ↑_o 𝐶)) ⊆ (ω ↑_o 𝐶))
207	206	expr 456	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ 𝐶) → (𝐴 ∈ (ω ↑_o 𝑥) → (𝐴 +_o (ω ↑_o 𝐶)) ⊆ (ω ↑_o 𝐶)))
208	101, 207	sylan2 593	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) ∧ 𝑥 ∈ (𝐶 ∖ 1_o)) → (𝐴 ∈ (ω ↑_o 𝑥) → (𝐴 +_o (ω ↑_o 𝐶)) ⊆ (ω ↑_o 𝐶)))
209	208	rexlimdva 3155	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (∃𝑥 ∈ (𝐶 ∖ 1_o)𝐴 ∈ (ω ↑_o 𝑥) → (𝐴 +_o (ω ↑_o 𝐶)) ⊆ (ω ↑_o 𝐶)))
210	100, 209	mpd 15	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +_o (ω ↑_o 𝐶)) ⊆ (ω ↑_o 𝐶))
211	88	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (ω ↑_o 𝐶) ⊆ (𝐴 +_o (ω ↑_o 𝐶)))
212	210, 211	eqssd 4001	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ Lim 𝐶) → (𝐴 +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶))
213	212	ex 412	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (Lim 𝐶 → (𝐴 +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶)))
214	43, 91, 213	3jaod 1431	. . . . . . . 8 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → ((𝐶 = ∅ ∨ ∃𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶) → (𝐴 +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶)))
215	28, 214	mpd 15	. . . . . . 7 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (𝐴 +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶))
216	215	adantr 480	. . . . . 6 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +_o (ω ↑_o 𝐶)) = (ω ↑_o 𝐶))
217	216	oveq1d 7446	. . . . 5 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → ((𝐴 +_o (ω ↑_o 𝐶)) +_o 𝑥) = ((ω ↑_o 𝐶) +_o 𝑥))
218	23, 217	eqtr3d 2779	. . . 4 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (𝐴 +_o ((ω ↑_o 𝐶) +_o 𝑥)) = ((ω ↑_o 𝐶) +_o 𝑥))
219		oveq2 7439	. . . . 5 ⊢ (((ω ↑_o 𝐶) +_o 𝑥) = 𝐵 → (𝐴 +_o ((ω ↑_o 𝐶) +_o 𝑥)) = (𝐴 +_o 𝐵))
220		id 22	. . . . 5 ⊢ (((ω ↑_o 𝐶) +_o 𝑥) = 𝐵 → ((ω ↑_o 𝐶) +_o 𝑥) = 𝐵)
221	219, 220	eqeq12d 2753	. . . 4 ⊢ (((ω ↑_o 𝐶) +_o 𝑥) = 𝐵 → ((𝐴 +_o ((ω ↑_o 𝐶) +_o 𝑥)) = ((ω ↑_o 𝐶) +_o 𝑥) ↔ (𝐴 +_o 𝐵) = 𝐵))
222	218, 221	syl5ibcom 245	. . 3 ⊢ ((((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) ∧ 𝑥 ∈ On) → (((ω ↑_o 𝐶) +_o 𝑥) = 𝐵 → (𝐴 +_o 𝐵) = 𝐵))
223	222	rexlimdva 3155	. 2 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (∃𝑥 ∈ On ((ω ↑_o 𝐶) +_o 𝑥) = 𝐵 → (𝐴 +_o 𝐵) = 𝐵))
224	15, 223	mpd 15	1 ⊢ (((𝐴 ∈ (ω ↑_o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑_o 𝐶) ⊆ 𝐵) → (𝐴 +_o 𝐵) = 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ w3o 1086 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 ∃!wreu 3378 ∖ cdif 3948 ∪ cun 3949 ⊆ wss 3951 ∅c0 4333 ∪ ciun 4991 × cxp 5683 dom cdm 5685 Ord word 6383 Oncon0 6384 Lim wlim 6385 suc csuc 6386 Fn wfn 6556 (class class class)co 7431 ωcom 7887 1_oc1o 8499 2_oc2o 8500 +_o coa 8503 ·_o comu 8504 ↑_o coe 8505

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-omul 8511 df-oexp 8512

This theorem is referenced by: cnfcomlem 9739 oacl2g 43343 omabs2 43345 ofoaf 43368

W3C validator