This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) )