Theorem oaabs2

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

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

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝐴 ∈ ( ω ↑o 𝐶 ) → ¬ ( ω ↑o 𝐶 ) = ∅ )
2		fnoe	⊢ ↑o Fn ( On × On )
3		fndm	⊢ ( ↑o Fn ( On × On ) → dom ↑o = ( On × On ) )
4	2 3	ax-mp	⊢ dom ↑o = ( On × On )
5	4	ndmov	⊢ ( ¬ ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ↑o 𝐶 ) = ∅ )
6	1 5	nsyl2	⊢ ( 𝐴 ∈ ( ω ↑o 𝐶 ) → ( ω ∈ On ∧ 𝐶 ∈ On ) )
7	6	ad2antrr	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ∈ On ∧ 𝐶 ∈ On ) )
8		oecl	⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ↑o 𝐶 ) ∈ On )
9	7 8	syl	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o 𝐶 ) ∈ On )
10		simplr	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐵 ∈ On )
11		simpr	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o 𝐶 ) ⊆ 𝐵 )
12		oawordeu	⊢ ( ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 )
13	9 10 11 12	syl21anc	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 )
14		reurex	⊢ ( ∃! 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ∃ 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 )
15	13 14	syl	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ∃ 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 )
16		simpll	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐴 ∈ ( ω ↑o 𝐶 ) )
17		onelon	⊢ ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝐴 ∈ ( ω ↑o 𝐶 ) ) → 𝐴 ∈ On )
18	9 16 17	syl2anc	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐴 ∈ On )
19	18	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → 𝐴 ∈ On )
20	9	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ω ↑o 𝐶 ) ∈ On )
21		simpr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → 𝑥 ∈ On )
22		oaass	⊢ ( ( 𝐴 ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ( ω ↑o 𝐶 ) ) +o 𝑥 ) = ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) )
23	19 20 21 22	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ( ω ↑o 𝐶 ) ) +o 𝑥 ) = ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) )
24	7	simprd	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → 𝐶 ∈ On )
25		eloni	⊢ ( 𝐶 ∈ On → Ord 𝐶 )
26	24 25	syl	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → Ord 𝐶 )
27		ordzsl	⊢ ( Ord 𝐶 ↔ ( 𝐶 = ∅ ∨ ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶 ) )
28	26 27	sylib	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐶 = ∅ ∨ ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶 ) )
29		simplll	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → 𝐴 ∈ ( ω ↑o 𝐶 ) )
30		oveq2	⊢ ( 𝐶 = ∅ → ( ω ↑o 𝐶 ) = ( ω ↑o ∅ ) )
31	7	simpld	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ω ∈ On )
32		oe0	⊢ ( ω ∈ On → ( ω ↑o ∅ ) = 1o )
33	31 32	syl	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o ∅ ) = 1o )
34	30 33	sylan9eqr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( ω ↑o 𝐶 ) = 1o )
35	29 34	eleqtrd	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → 𝐴 ∈ 1o )
36		el1o	⊢ ( 𝐴 ∈ 1o ↔ 𝐴 = ∅ )
37	35 36	sylib	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → 𝐴 = ∅ )
38	37	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ∅ +o ( ω ↑o 𝐶 ) ) )
39	9	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( ω ↑o 𝐶 ) ∈ On )
40		oa0r	⊢ ( ( ω ↑o 𝐶 ) ∈ On → ( ∅ +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
41	39 40	syl	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( ∅ +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
42	38 41	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝐶 = ∅ ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
43	42	ex	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐶 = ∅ → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) )
44	31	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ω ∈ On )
45		simprl	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝑥 ∈ On )
46		oecl	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ↑o 𝑥 ) ∈ On )
47	44 45 46	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝑥 ) ∈ On )
48		limom	⊢ Lim ω
49	44 48	jctir	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ∈ On ∧ Lim ω ) )
50		simplll	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝐴 ∈ ( ω ↑o 𝐶 ) )
51		simprr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝐶 = suc 𝑥 )
52	51	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝐶 ) = ( ω ↑o suc 𝑥 ) )
53		oesuc	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ↑o suc 𝑥 ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
54	44 45 53	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o suc 𝑥 ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
55	52 54	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝐶 ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
56	50 55	eleqtrd	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o ω ) )
57		omordlim	⊢ ( ( ( ( ω ↑o 𝑥 ) ∈ On ∧ ( ω ∈ On ∧ Lim ω ) ) ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o ω ) ) → ∃ 𝑦 ∈ ω 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
58	47 49 56 57	syl21anc	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ∃ 𝑦 ∈ ω 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
59	47	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ω ↑o 𝑥 ) ∈ On )
60		nnon	⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On )
61	60	ad2antrl	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝑦 ∈ On )
62		omcl	⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 𝑦 ∈ On ) → ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On )
63	59 61 62	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On )
64		eloni	⊢ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On → Ord ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
65	63 64	syl	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → Ord ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
66		simprr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
67		ordelss	⊢ ( ( Ord ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) → 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
68	65 66 67	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) )
69	18	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝐴 ∈ On )
70	9	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ω ↑o 𝐶 ) ∈ On )
71		oawordri	⊢ ( ( 𝐴 ∈ On ∧ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ∈ On ∧ ( ω ↑o 𝐶 ) ∈ On ) → ( 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) ) )
72	69 63 70 71	syl3anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝐴 ⊆ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) ) )
73	68 72	mpd	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) )
74	44	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ω ∈ On )
75		odi	⊢ ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 𝑦 ∈ On ∧ ω ∈ On ) → ( ( ω ↑o 𝑥 ) ·o ( 𝑦 +o ω ) ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) )
76	59 61 74 75	syl3anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ω ↑o 𝑥 ) ·o ( 𝑦 +o ω ) ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) )
77		simprl	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → 𝑦 ∈ ω )
78		oaabslem	⊢ ( ( ω ∈ On ∧ 𝑦 ∈ ω ) → ( 𝑦 +o ω ) = ω )
79	74 77 78	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝑦 +o ω ) = ω )
80	79	oveq2d	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ω ↑o 𝑥 ) ·o ( 𝑦 +o ω ) ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
81	76 80	eqtr3d	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
82	55	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ω ↑o 𝐶 ) = ( ( ω ↑o 𝑥 ) ·o ω ) )
83	82	oveq2d	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) = ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ( ω ↑o 𝑥 ) ·o ω ) ) )
84	81 83 82	3eqtr4d	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( ( ( ω ↑o 𝑥 ) ·o 𝑦 ) +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
85	73 84	sseqtrd	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) ∧ ( 𝑦 ∈ ω ∧ 𝐴 ∈ ( ( ω ↑o 𝑥 ) ·o 𝑦 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) )
86	58 85	rexlimddv	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) )
87		oaword2	⊢ ( ( ( ω ↑o 𝐶 ) ∈ On ∧ 𝐴 ∈ On ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) )
88	9 18 87	syl2anc	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) )
89	88	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) )
90	86 89	eqssd	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ ( 𝑥 ∈ On ∧ 𝐶 = suc 𝑥 ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
91	90	rexlimdvaa	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) )
92		simplll	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → 𝐴 ∈ ( ω ↑o 𝐶 ) )
93	31	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ω ∈ On )
94	24	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → 𝐶 ∈ On )
95		simpr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → Lim 𝐶 )
96		oelim2	⊢ ( ( ω ∈ On ∧ ( 𝐶 ∈ On ∧ Lim 𝐶 ) ) → ( ω ↑o 𝐶 ) = ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) )
97	93 94 95 96	syl12anc	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ω ↑o 𝐶 ) = ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) )
98	92 97	eleqtrd	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → 𝐴 ∈ ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) )
99		eliun	⊢ ( 𝐴 ∈ ∪ 𝑥 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑥 ) ↔ ∃ 𝑥 ∈ ( 𝐶 ∖ 1o ) 𝐴 ∈ ( ω ↑o 𝑥 ) )
100	98 99	sylib	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ∃ 𝑥 ∈ ( 𝐶 ∖ 1o ) 𝐴 ∈ ( ω ↑o 𝑥 ) )
101		eldifi	⊢ ( 𝑥 ∈ ( 𝐶 ∖ 1o ) → 𝑥 ∈ 𝐶 )
102	18	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → 𝐴 ∈ On )
103	9	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( ω ↑o 𝐶 ) ∈ On )
104	93	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ω ∈ On )
105		1onn	⊢ 1o ∈ ω
106		ondif2	⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) )
107	104 105 106	sylanblrc	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ω ∈ ( On ∖ 2o ) )
108	94	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → 𝐶 ∈ On )
109		simplr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → Lim 𝐶 )
110		oelimcl	⊢ ( ( ω ∈ ( On ∖ 2o ) ∧ ( 𝐶 ∈ On ∧ Lim 𝐶 ) ) → Lim ( ω ↑o 𝐶 ) )
111	107 108 109 110	syl12anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → Lim ( ω ↑o 𝐶 ) )
112		oalim	⊢ ( ( 𝐴 ∈ On ∧ ( ( ω ↑o 𝐶 ) ∈ On ∧ Lim ( ω ↑o 𝐶 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) )
113	102 103 111 112	syl12anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) )
114		oelim2	⊢ ( ( ω ∈ On ∧ ( 𝐶 ∈ On ∧ Lim 𝐶 ) ) → ( ω ↑o 𝐶 ) = ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) )
115	93 94 95 114	syl12anc	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ω ↑o 𝐶 ) = ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) )
116	115	eleq2d	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) ↔ 𝑦 ∈ ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) ) )
117		eliun	⊢ ( 𝑦 ∈ ∪ 𝑧 ∈ ( 𝐶 ∖ 1o ) ( ω ↑o 𝑧 ) ↔ ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) )
118	116 117	bitrdi	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) ↔ ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) ) )
119	118	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) ↔ ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) ) )
120		eldifi	⊢ ( 𝑧 ∈ ( 𝐶 ∖ 1o ) → 𝑧 ∈ 𝐶 )
121	104	adantr	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ω ∈ On )
122	108	adantr	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐶 ∈ On )
123		simplrl	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑥 ∈ 𝐶 )
124		onelon	⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ On )
125	122 123 124	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑥 ∈ On )
126	121 125 46	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑥 ) ∈ On )
127		eloni	⊢ ( ( ω ↑o 𝑥 ) ∈ On → Ord ( ω ↑o 𝑥 ) )
128	126 127	syl	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → Ord ( ω ↑o 𝑥 ) )
129		simplrr	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ∈ ( ω ↑o 𝑥 ) )
130		ordelss	⊢ ( ( Ord ( ω ↑o 𝑥 ) ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) → 𝐴 ⊆ ( ω ↑o 𝑥 ) )
131	128 129 130	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ⊆ ( ω ↑o 𝑥 ) )
132		ssun1	⊢ 𝑥 ⊆ ( 𝑥 ∪ 𝑧 )
133	26	ad3antrrr	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → Ord 𝐶 )
134		simprl	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑧 ∈ 𝐶 )
135		ordunel	⊢ ( ( Ord 𝐶 ∧ 𝑥 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 )
136	133 123 134 135	syl3anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 )
137		onelon	⊢ ( ( 𝐶 ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 ) → ( 𝑥 ∪ 𝑧 ) ∈ On )
138	122 136 137	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑥 ∪ 𝑧 ) ∈ On )
139		peano1	⊢ ∅ ∈ ω
140	139	a1i	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ∅ ∈ ω )
141		oewordi	⊢ ( ( ( 𝑥 ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( 𝑥 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑥 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
142	125 138 121 140 141	syl31anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑥 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑥 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
143	132 142	mpi	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑥 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
144	131 143	sstrd	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
145	102	adantr	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝐴 ∈ On )
146		oecl	⊢ ( ( ω ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ) → ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On )
147	121 138 146	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On )
148		onelon	⊢ ( ( 𝐶 ∈ On ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ On )
149	122 134 148	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑧 ∈ On )
150		oecl	⊢ ( ( ω ∈ On ∧ 𝑧 ∈ On ) → ( ω ↑o 𝑧 ) ∈ On )
151	121 149 150	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑧 ) ∈ On )
152		simprr	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ∈ ( ω ↑o 𝑧 ) )
153		onelon	⊢ ( ( ( ω ↑o 𝑧 ) ∈ On ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) → 𝑦 ∈ On )
154	151 152 153	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ∈ On )
155		oawordri	⊢ ( ( 𝐴 ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ) )
156	145 147 154 155	syl3anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ) )
157	144 156	mpd	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) )
158		eloni	⊢ ( ( ω ↑o 𝑧 ) ∈ On → Ord ( ω ↑o 𝑧 ) )
159	151 158	syl	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → Ord ( ω ↑o 𝑧 ) )
160		ordelss	⊢ ( ( Ord ( ω ↑o 𝑧 ) ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) → 𝑦 ⊆ ( ω ↑o 𝑧 ) )
161	159 152 160	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ⊆ ( ω ↑o 𝑧 ) )
162		ssun2	⊢ 𝑧 ⊆ ( 𝑥 ∪ 𝑧 )
163		oewordi	⊢ ( ( ( 𝑧 ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( 𝑧 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑧 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
164	149 138 121 140 163	syl31anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑧 ⊆ ( 𝑥 ∪ 𝑧 ) → ( ω ↑o 𝑧 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
165	162 164	mpi	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o 𝑧 ) ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
166	161 165	sstrd	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 𝑦 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
167		oaword	⊢ ( ( 𝑦 ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ) → ( 𝑦 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ↔ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) )
168	154 147 147 167	syl3anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝑦 ⊆ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ↔ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ) )
169	166 168	mpbid	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
170	157 169	sstrd	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
171		ordom	⊢ Ord ω
172		ordsucss	⊢ ( Ord ω → ( 1o ∈ ω → suc 1o ⊆ ω ) )
173	171 105 172	mp2	⊢ suc 1o ⊆ ω
174		1on	⊢ 1o ∈ On
175		onsuc	⊢ ( 1o ∈ On → suc 1o ∈ On )
176	174 175	mp1i	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → suc 1o ∈ On )
177		omwordi	⊢ ( ( suc 1o ∈ On ∧ ω ∈ On ∧ ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ) → ( suc 1o ⊆ ω → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) ) )
178	176 121 147 177	syl3anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( suc 1o ⊆ ω → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) ) )
179	173 178	mpi	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) ⊆ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) )
180	174	a1i	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → 1o ∈ On )
181		omsuc	⊢ ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On ∧ 1o ∈ On ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) = ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
182	147 180 181	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) = ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
183		om1	⊢ ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ∈ On → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) = ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
184	147 183	syl	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) = ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) )
185	184	oveq1d	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o 1o ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) )
186	182 185	eqtr2d	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o suc 1o ) )
187		oesuc	⊢ ( ( ω ∈ On ∧ ( 𝑥 ∪ 𝑧 ) ∈ On ) → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) )
188	121 138 187	syl2anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) = ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ·o ω ) )
189	179 186 188	3sstr4d	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) +o ( ω ↑o ( 𝑥 ∪ 𝑧 ) ) ) ⊆ ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) )
190	170 189	sstrd	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) )
191		ordsucss	⊢ ( Ord 𝐶 → ( ( 𝑥 ∪ 𝑧 ) ∈ 𝐶 → suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 ) )
192	133 136 191	sylc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 )
193		onsuc	⊢ ( ( 𝑥 ∪ 𝑧 ) ∈ On → suc ( 𝑥 ∪ 𝑧 ) ∈ On )
194	138 193	syl	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → suc ( 𝑥 ∪ 𝑧 ) ∈ On )
195		oewordi	⊢ ( ( ( suc ( 𝑥 ∪ 𝑧 ) ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ On ) ∧ ∅ ∈ ω ) → ( suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ⊆ ( ω ↑o 𝐶 ) ) )
196	194 122 121 140 195	syl31anc	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( suc ( 𝑥 ∪ 𝑧 ) ⊆ 𝐶 → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ⊆ ( ω ↑o 𝐶 ) ) )
197	192 196	mpd	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( ω ↑o suc ( 𝑥 ∪ 𝑧 ) ) ⊆ ( ω ↑o 𝐶 ) )
198	190 197	sstrd	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑦 ∈ ( ω ↑o 𝑧 ) ) ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) )
199	198	expr	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ∈ ( ω ↑o 𝑧 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) )
200	120 199	sylan2	⊢ ( ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ∧ 𝑧 ∈ ( 𝐶 ∖ 1o ) ) → ( 𝑦 ∈ ( ω ↑o 𝑧 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) )
201	200	rexlimdva	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( ∃ 𝑧 ∈ ( 𝐶 ∖ 1o ) 𝑦 ∈ ( ω ↑o 𝑧 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) )
202	119 201	sylbid	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝑦 ∈ ( ω ↑o 𝐶 ) → ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ) )
203	202	ralrimiv	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ∀ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) )
204		iunss	⊢ ( ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) ↔ ∀ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) )
205	203 204	sylibr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ∪ 𝑦 ∈ ( ω ↑o 𝐶 ) ( 𝐴 +o 𝑦 ) ⊆ ( ω ↑o 𝐶 ) )
206	113 205	eqsstrd	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) )
207	206	expr	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐴 ∈ ( ω ↑o 𝑥 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) )
208	101 207	sylan2	⊢ ( ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) ∧ 𝑥 ∈ ( 𝐶 ∖ 1o ) ) → ( 𝐴 ∈ ( ω ↑o 𝑥 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) )
209	208	rexlimdva	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ∃ 𝑥 ∈ ( 𝐶 ∖ 1o ) 𝐴 ∈ ( ω ↑o 𝑥 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) ) )
210	100 209	mpd	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) ⊆ ( ω ↑o 𝐶 ) )
211	88	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( ω ↑o 𝐶 ) ⊆ ( 𝐴 +o ( ω ↑o 𝐶 ) ) )
212	210 211	eqssd	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ Lim 𝐶 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
213	212	ex	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( Lim 𝐶 → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) )
214	43 91 213	3jaod	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ( 𝐶 = ∅ ∨ ∃ 𝑥 ∈ On 𝐶 = suc 𝑥 ∨ Lim 𝐶 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) ) )
215	28 214	mpd	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
216	215	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( 𝐴 +o ( ω ↑o 𝐶 ) ) = ( ω ↑o 𝐶 ) )
217	216	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ( ω ↑o 𝐶 ) ) +o 𝑥 ) = ( ( ω ↑o 𝐶 ) +o 𝑥 ) )
218	23 217	eqtr3d	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) = ( ( ω ↑o 𝐶 ) +o 𝑥 ) )
219		oveq2	⊢ ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) = ( 𝐴 +o 𝐵 ) )
220		id	⊢ ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 )
221	219 220	eqeq12d	⊢ ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( ( 𝐴 +o ( ( ω ↑o 𝐶 ) +o 𝑥 ) ) = ( ( ω ↑o 𝐶 ) +o 𝑥 ) ↔ ( 𝐴 +o 𝐵 ) = 𝐵 ) )
222	218 221	syl5ibcom	⊢ ( ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( 𝐴 +o 𝐵 ) = 𝐵 ) )
223	222	rexlimdva	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( ∃ 𝑥 ∈ On ( ( ω ↑o 𝐶 ) +o 𝑥 ) = 𝐵 → ( 𝐴 +o 𝐵 ) = 𝐵 ) )
224	15 223	mpd	⊢ ( ( ( 𝐴 ∈ ( ω ↑o 𝐶 ) ∧ 𝐵 ∈ On ) ∧ ( ω ↑o 𝐶 ) ⊆ 𝐵 ) → ( 𝐴 +o 𝐵 ) = 𝐵 )