Theorem omabs

Description: Ordinal multiplication is also absorbed by powers of _om . (Contributed by Mario Carneiro, 30-May-2015)

	Ref	Expression
Assertion	omabs	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) ) → ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( ω ↑o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝑥 = ∅ → ( ∅ ∈ 𝑥 ↔ ∅ ∈ ∅ ) )
2		oveq2	⊢ ( 𝑥 = ∅ → ( ω ↑o 𝑥 ) = ( ω ↑o ∅ ) )
3	2	oveq2d	⊢ ( 𝑥 = ∅ → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( 𝐴 ·o ( ω ↑o ∅ ) ) )
4	3 2	eqeq12d	⊢ ( 𝑥 = ∅ → ( ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ↔ ( 𝐴 ·o ( ω ↑o ∅ ) ) = ( ω ↑o ∅ ) ) )
5	1 4	imbi12d	⊢ ( 𝑥 = ∅ → ( ( ∅ ∈ 𝑥 → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ) ↔ ( ∅ ∈ ∅ → ( 𝐴 ·o ( ω ↑o ∅ ) ) = ( ω ↑o ∅ ) ) ) )
6		eleq2	⊢ ( 𝑥 = 𝑦 → ( ∅ ∈ 𝑥 ↔ ∅ ∈ 𝑦 ) )
7		oveq2	⊢ ( 𝑥 = 𝑦 → ( ω ↑o 𝑥 ) = ( ω ↑o 𝑦 ) )
8	7	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( 𝐴 ·o ( ω ↑o 𝑦 ) ) )
9	8 7	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ↔ ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) )
10	6 9	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ∅ ∈ 𝑥 → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ) ↔ ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) )
11		eleq2	⊢ ( 𝑥 = suc 𝑦 → ( ∅ ∈ 𝑥 ↔ ∅ ∈ suc 𝑦 ) )
12		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( ω ↑o 𝑥 ) = ( ω ↑o suc 𝑦 ) )
13	12	oveq2d	⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) )
14	13 12	eqeq12d	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ↔ ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) )
15	11 14	imbi12d	⊢ ( 𝑥 = suc 𝑦 → ( ( ∅ ∈ 𝑥 → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ) ↔ ( ∅ ∈ suc 𝑦 → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) ) )
16		eleq2	⊢ ( 𝑥 = 𝐵 → ( ∅ ∈ 𝑥 ↔ ∅ ∈ 𝐵 ) )
17		oveq2	⊢ ( 𝑥 = 𝐵 → ( ω ↑o 𝑥 ) = ( ω ↑o 𝐵 ) )
18	17	oveq2d	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( 𝐴 ·o ( ω ↑o 𝐵 ) ) )
19	18 17	eqeq12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ↔ ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( ω ↑o 𝐵 ) ) )
20	16 19	imbi12d	⊢ ( 𝑥 = 𝐵 → ( ( ∅ ∈ 𝑥 → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ) ↔ ( ∅ ∈ 𝐵 → ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( ω ↑o 𝐵 ) ) ) )
21		noel	⊢ ¬ ∅ ∈ ∅
22	21	pm2.21i	⊢ ( ∅ ∈ ∅ → ( 𝐴 ·o ( ω ↑o ∅ ) ) = ( ω ↑o ∅ ) )
23	22	a1i	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ω ∈ On ) → ( ∅ ∈ ∅ → ( 𝐴 ·o ( ω ↑o ∅ ) ) = ( ω ↑o ∅ ) ) )
24		simprl	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ω ∈ On )
25		simpll	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → 𝐴 ∈ ω )
26		simplr	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ∅ ∈ 𝐴 )
27		omabslem	⊢ ( ( ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ·o ω ) = ω )
28	24 25 26 27	syl3anc	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( 𝐴 ·o ω ) = ω )
29	28	adantr	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) ∧ 𝑦 = ∅ ) → ( 𝐴 ·o ω ) = ω )
30		suceq	⊢ ( 𝑦 = ∅ → suc 𝑦 = suc ∅ )
31		df-1o	⊢ 1o = suc ∅
32	30 31	eqtr4di	⊢ ( 𝑦 = ∅ → suc 𝑦 = 1o )
33	32	oveq2d	⊢ ( 𝑦 = ∅ → ( ω ↑o suc 𝑦 ) = ( ω ↑o 1o ) )
34		oe1	⊢ ( ω ∈ On → ( ω ↑o 1o ) = ω )
35	34	ad2antrl	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( ω ↑o 1o ) = ω )
36	33 35	sylan9eqr	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) ∧ 𝑦 = ∅ ) → ( ω ↑o suc 𝑦 ) = ω )
37	36	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) ∧ 𝑦 = ∅ ) → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( 𝐴 ·o ω ) )
38	29 37 36	3eqtr4d	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) ∧ 𝑦 = ∅ ) → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) )
39	38	ex	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( 𝑦 = ∅ → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) )
40	39	a1dd	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( 𝑦 = ∅ → ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) ) )
41		oveq1	⊢ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) → ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) ·o ω ) = ( ( ω ↑o 𝑦 ) ·o ω ) )
42		oesuc	⊢ ( ( ω ∈ On ∧ 𝑦 ∈ On ) → ( ω ↑o suc 𝑦 ) = ( ( ω ↑o 𝑦 ) ·o ω ) )
43	42	adantl	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( ω ↑o suc 𝑦 ) = ( ( ω ↑o 𝑦 ) ·o ω ) )
44	43	oveq2d	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( 𝐴 ·o ( ( ω ↑o 𝑦 ) ·o ω ) ) )
45		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
46	45	ad2antrr	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → 𝐴 ∈ On )
47		oecl	⊢ ( ( ω ∈ On ∧ 𝑦 ∈ On ) → ( ω ↑o 𝑦 ) ∈ On )
48	47	adantl	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( ω ↑o 𝑦 ) ∈ On )
49		omass	⊢ ( ( 𝐴 ∈ On ∧ ( ω ↑o 𝑦 ) ∈ On ∧ ω ∈ On ) → ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) ·o ω ) = ( 𝐴 ·o ( ( ω ↑o 𝑦 ) ·o ω ) ) )
50	46 48 24 49	syl3anc	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) ·o ω ) = ( 𝐴 ·o ( ( ω ↑o 𝑦 ) ·o ω ) ) )
51	44 50	eqtr4d	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) ·o ω ) )
52	51 43	eqeq12d	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ↔ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) ·o ω ) = ( ( ω ↑o 𝑦 ) ·o ω ) ) )
53	41 52	imbitrrid	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) )
54	53	imim2d	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) ) )
55	54	com23	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( ∅ ∈ 𝑦 → ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) ) )
56		simprr	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → 𝑦 ∈ On )
57		on0eqel	⊢ ( 𝑦 ∈ On → ( 𝑦 = ∅ ∨ ∅ ∈ 𝑦 ) )
58	56 57	syl	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( 𝑦 = ∅ ∨ ∅ ∈ 𝑦 ) )
59	40 55 58	mpjaod	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) )
60	59	a1dd	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝑦 ∈ On ) ) → ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( ∅ ∈ suc 𝑦 → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) ) )
61	60	anassrs	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ω ∈ On ) ∧ 𝑦 ∈ On ) → ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( ∅ ∈ suc 𝑦 → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) ) )
62	61	expcom	⊢ ( 𝑦 ∈ On → ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ω ∈ On ) → ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( ∅ ∈ suc 𝑦 → ( 𝐴 ·o ( ω ↑o suc 𝑦 ) ) = ( ω ↑o suc 𝑦 ) ) ) ) )
63	45	ad3antrrr	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → 𝐴 ∈ On )
64		simprl	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → ω ∈ On )
65		simprr	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → Lim 𝑥 )
66		vex	⊢ 𝑥 ∈ V
67	65 66	jctil	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → ( 𝑥 ∈ V ∧ Lim 𝑥 ) )
68		limelon	⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → 𝑥 ∈ On )
69	67 68	syl	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → 𝑥 ∈ On )
70		oecl	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ↑o 𝑥 ) ∈ On )
71	64 69 70	syl2anc	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → ( ω ↑o 𝑥 ) ∈ On )
72	71	adantr	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( ω ↑o 𝑥 ) ∈ On )
73		1onn	⊢ 1o ∈ ω
74		ondif2	⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) )
75	64 73 74	sylanblrc	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → ω ∈ ( On ∖ 2o ) )
76	75	adantr	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ω ∈ ( On ∖ 2o ) )
77	67	adantr	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( 𝑥 ∈ V ∧ Lim 𝑥 ) )
78		oelimcl	⊢ ( ( ω ∈ ( On ∖ 2o ) ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → Lim ( ω ↑o 𝑥 ) )
79	76 77 78	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → Lim ( ω ↑o 𝑥 ) )
80		omlim	⊢ ( ( 𝐴 ∈ On ∧ ( ( ω ↑o 𝑥 ) ∈ On ∧ Lim ( ω ↑o 𝑥 ) ) ) → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ∪ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝐴 ·o 𝑧 ) )
81	63 72 79 80	syl12anc	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ∪ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝐴 ·o 𝑧 ) )
82		simplrl	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ω ∈ On )
83		oelim2	⊢ ( ( ω ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( ω ↑o 𝑥 ) = ∪ 𝑦 ∈ ( 𝑥 ∖ 1o ) ( ω ↑o 𝑦 ) )
84	82 77 83	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( ω ↑o 𝑥 ) = ∪ 𝑦 ∈ ( 𝑥 ∖ 1o ) ( ω ↑o 𝑦 ) )
85	84	eleq2d	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( 𝑧 ∈ ( ω ↑o 𝑥 ) ↔ 𝑧 ∈ ∪ 𝑦 ∈ ( 𝑥 ∖ 1o ) ( ω ↑o 𝑦 ) ) )
86		eliun	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ ( 𝑥 ∖ 1o ) ( ω ↑o 𝑦 ) ↔ ∃ 𝑦 ∈ ( 𝑥 ∖ 1o ) 𝑧 ∈ ( ω ↑o 𝑦 ) )
87	85 86	bitrdi	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( 𝑧 ∈ ( ω ↑o 𝑥 ) ↔ ∃ 𝑦 ∈ ( 𝑥 ∖ 1o ) 𝑧 ∈ ( ω ↑o 𝑦 ) ) )
88	69	adantr	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → 𝑥 ∈ On )
89		anass	⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ↔ ( 𝑦 ∈ 𝑥 ∧ ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) )
90		onelon	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
91		on0eln0	⊢ ( 𝑦 ∈ On → ( ∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅ ) )
92	90 91	syl	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅ ) )
93	92	pm5.32da	⊢ ( 𝑥 ∈ On → ( ( 𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦 ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅ ) ) )
94		dif1o	⊢ ( 𝑦 ∈ ( 𝑥 ∖ 1o ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅ ) )
95	93 94	bitr4di	⊢ ( 𝑥 ∈ On → ( ( 𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦 ) ↔ 𝑦 ∈ ( 𝑥 ∖ 1o ) ) )
96	95	anbi1d	⊢ ( 𝑥 ∈ On → ( ( ( 𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ↔ ( 𝑦 ∈ ( 𝑥 ∖ 1o ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) )
97	89 96	bitr3id	⊢ ( 𝑥 ∈ On → ( ( 𝑦 ∈ 𝑥 ∧ ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) ↔ ( 𝑦 ∈ ( 𝑥 ∖ 1o ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) )
98	97	rexbidv2	⊢ ( 𝑥 ∈ On → ( ∃ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ↔ ∃ 𝑦 ∈ ( 𝑥 ∖ 1o ) 𝑧 ∈ ( ω ↑o 𝑦 ) ) )
99	88 98	syl	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( ∃ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ↔ ∃ 𝑦 ∈ ( 𝑥 ∖ 1o ) 𝑧 ∈ ( ω ↑o 𝑦 ) ) )
100	87 99	bitr4d	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( 𝑧 ∈ ( ω ↑o 𝑥 ) ↔ ∃ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) )
101		r19.29	⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ∧ ∃ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ∃ 𝑦 ∈ 𝑥 ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ∧ ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) )
102		id	⊢ ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) )
103	102	imp	⊢ ( ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ∧ ∅ ∈ 𝑦 ) → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) )
104	103	anim1i	⊢ ( ( ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ∧ ∅ ∈ 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) → ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) )
105	104	anasss	⊢ ( ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ∧ ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) )
106	71	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( ω ↑o 𝑥 ) ∈ On )
107		eloni	⊢ ( ( ω ↑o 𝑥 ) ∈ On → Ord ( ω ↑o 𝑥 ) )
108	106 107	syl	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → Ord ( ω ↑o 𝑥 ) )
109		simprr	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → 𝑧 ∈ ( ω ↑o 𝑦 ) )
110	64	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ω ∈ On )
111	69	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → 𝑥 ∈ On )
112		simplr	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → 𝑦 ∈ 𝑥 )
113	111 112 90	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → 𝑦 ∈ On )
114	110 113 47	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( ω ↑o 𝑦 ) ∈ On )
115		onelon	⊢ ( ( ( ω ↑o 𝑦 ) ∈ On ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) → 𝑧 ∈ On )
116	114 109 115	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → 𝑧 ∈ On )
117	45	ad2antrr	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → 𝐴 ∈ On )
118	117	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → 𝐴 ∈ On )
119		simplr	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → ∅ ∈ 𝐴 )
120	119	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ∅ ∈ 𝐴 )
121		omord2	⊢ ( ( ( 𝑧 ∈ On ∧ ( ω ↑o 𝑦 ) ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑧 ∈ ( ω ↑o 𝑦 ) ↔ ( 𝐴 ·o 𝑧 ) ∈ ( 𝐴 ·o ( ω ↑o 𝑦 ) ) ) )
122	116 114 118 120 121	syl31anc	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( 𝑧 ∈ ( ω ↑o 𝑦 ) ↔ ( 𝐴 ·o 𝑧 ) ∈ ( 𝐴 ·o ( ω ↑o 𝑦 ) ) ) )
123	109 122	mpbid	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o 𝑧 ) ∈ ( 𝐴 ·o ( ω ↑o 𝑦 ) ) )
124		simprl	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) )
125	123 124	eleqtrd	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o 𝑧 ) ∈ ( ω ↑o 𝑦 ) )
126	75	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ω ∈ ( On ∖ 2o ) )
127		oeord	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( 𝑦 ∈ 𝑥 ↔ ( ω ↑o 𝑦 ) ∈ ( ω ↑o 𝑥 ) ) )
128	113 111 126 127	syl3anc	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( 𝑦 ∈ 𝑥 ↔ ( ω ↑o 𝑦 ) ∈ ( ω ↑o 𝑥 ) ) )
129	112 128	mpbid	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( ω ↑o 𝑦 ) ∈ ( ω ↑o 𝑥 ) )
130		ontr1	⊢ ( ( ω ↑o 𝑥 ) ∈ On → ( ( ( 𝐴 ·o 𝑧 ) ∈ ( ω ↑o 𝑦 ) ∧ ( ω ↑o 𝑦 ) ∈ ( ω ↑o 𝑥 ) ) → ( 𝐴 ·o 𝑧 ) ∈ ( ω ↑o 𝑥 ) ) )
131	106 130	syl	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( ( ( 𝐴 ·o 𝑧 ) ∈ ( ω ↑o 𝑦 ) ∧ ( ω ↑o 𝑦 ) ∈ ( ω ↑o 𝑥 ) ) → ( 𝐴 ·o 𝑧 ) ∈ ( ω ↑o 𝑥 ) ) )
132	125 129 131	mp2and	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o 𝑧 ) ∈ ( ω ↑o 𝑥 ) )
133		ordelss	⊢ ( ( Ord ( ω ↑o 𝑥 ) ∧ ( 𝐴 ·o 𝑧 ) ∈ ( ω ↑o 𝑥 ) ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) )
134	108 132 133	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) )
135	134	ex	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) ) )
136	105 135	syl5	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ∧ ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) ) )
137	136	rexlimdva	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → ( ∃ 𝑦 ∈ 𝑥 ( ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ∧ ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) ) )
138	101 137	syl5	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → ( ( ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ∧ ∃ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) ) )
139	138	expdimp	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( ∃ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 ∧ 𝑧 ∈ ( ω ↑o 𝑦 ) ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) ) )
140	100 139	sylbid	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( 𝑧 ∈ ( ω ↑o 𝑥 ) → ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) ) )
141	140	ralrimiv	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ∀ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) )
142		iunss	⊢ ( ∪ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) ↔ ∀ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) )
143	141 142	sylibr	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ∪ 𝑧 ∈ ( ω ↑o 𝑥 ) ( 𝐴 ·o 𝑧 ) ⊆ ( ω ↑o 𝑥 ) )
144	81 143	eqsstrd	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) ⊆ ( ω ↑o 𝑥 ) )
145		simpllr	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ∅ ∈ 𝐴 )
146		omword2	⊢ ( ( ( ( ω ↑o 𝑥 ) ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ω ↑o 𝑥 ) ⊆ ( 𝐴 ·o ( ω ↑o 𝑥 ) ) )
147	72 63 145 146	syl21anc	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( ω ↑o 𝑥 ) ⊆ ( 𝐴 ·o ( ω ↑o 𝑥 ) ) )
148	144 147	eqssd	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) ) → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) )
149	148	ex	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ Lim 𝑥 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ) )
150	149	anassrs	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ω ∈ On ) ∧ Lim 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ) )
151	150	a1dd	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ω ∈ On ) ∧ Lim 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( ∅ ∈ 𝑥 → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ) ) )
152	151	expcom	⊢ ( Lim 𝑥 → ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ω ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 ( ∅ ∈ 𝑦 → ( 𝐴 ·o ( ω ↑o 𝑦 ) ) = ( ω ↑o 𝑦 ) ) → ( ∅ ∈ 𝑥 → ( 𝐴 ·o ( ω ↑o 𝑥 ) ) = ( ω ↑o 𝑥 ) ) ) ) )
153	5 10 15 20 23 62 152	tfinds3	⊢ ( 𝐵 ∈ On → ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ω ∈ On ) → ( ∅ ∈ 𝐵 → ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( ω ↑o 𝐵 ) ) ) )
154	153	com12	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ω ∈ On ) → ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 → ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( ω ↑o 𝐵 ) ) ) )
155	154	adantrr	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 → ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( ω ↑o 𝐵 ) ) ) )
156	155	imp32	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( ω ∈ On ∧ 𝐵 ∈ On ) ) ∧ ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) ) → ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( ω ↑o 𝐵 ) )
157	156	an32s	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) ) ∧ ( ω ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( ω ↑o 𝐵 ) )
158		nnm0	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o ∅ ) = ∅ )
159	158	ad3antrrr	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) ) ∧ ¬ ( ω ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ·o ∅ ) = ∅ )
160		fnoe	⊢ ↑o Fn ( On × On )
161		fndm	⊢ ( ↑o Fn ( On × On ) → dom ↑o = ( On × On ) )
162	160 161	ax-mp	⊢ dom ↑o = ( On × On )
163	162	ndmov	⊢ ( ¬ ( ω ∈ On ∧ 𝐵 ∈ On ) → ( ω ↑o 𝐵 ) = ∅ )
164	163	adantl	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) ) ∧ ¬ ( ω ∈ On ∧ 𝐵 ∈ On ) ) → ( ω ↑o 𝐵 ) = ∅ )
165	164	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) ) ∧ ¬ ( ω ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( 𝐴 ·o ∅ ) )
166	159 165 164	3eqtr4d	⊢ ( ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) ) ∧ ¬ ( ω ∈ On ∧ 𝐵 ∈ On ) ) → ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( ω ↑o 𝐵 ) )
167	157 166	pm2.61dan	⊢ ( ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) ) → ( 𝐴 ·o ( ω ↑o 𝐵 ) ) = ( ω ↑o 𝐵 ) )