Step |
Hyp |
Ref |
Expression |
1 |
|
oesuclem.1 |
⊢ Lim 𝑋 |
2 |
|
oesuclem.2 |
⊢ ( 𝐵 ∈ 𝑋 → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) ) |
3 |
|
oveq1 |
⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o suc 𝐵 ) = ( ∅ ↑o suc 𝐵 ) ) |
4 |
|
limord |
⊢ ( Lim 𝑋 → Ord 𝑋 ) |
5 |
1 4
|
ax-mp |
⊢ Ord 𝑋 |
6 |
|
ordelord |
⊢ ( ( Ord 𝑋 ∧ 𝐵 ∈ 𝑋 ) → Ord 𝐵 ) |
7 |
5 6
|
mpan |
⊢ ( 𝐵 ∈ 𝑋 → Ord 𝐵 ) |
8 |
|
0elsuc |
⊢ ( Ord 𝐵 → ∅ ∈ suc 𝐵 ) |
9 |
7 8
|
syl |
⊢ ( 𝐵 ∈ 𝑋 → ∅ ∈ suc 𝐵 ) |
10 |
|
limsuc |
⊢ ( Lim 𝑋 → ( 𝐵 ∈ 𝑋 ↔ suc 𝐵 ∈ 𝑋 ) ) |
11 |
1 10
|
ax-mp |
⊢ ( 𝐵 ∈ 𝑋 ↔ suc 𝐵 ∈ 𝑋 ) |
12 |
|
ordelon |
⊢ ( ( Ord 𝑋 ∧ suc 𝐵 ∈ 𝑋 ) → suc 𝐵 ∈ On ) |
13 |
5 12
|
mpan |
⊢ ( suc 𝐵 ∈ 𝑋 → suc 𝐵 ∈ On ) |
14 |
|
oe0m1 |
⊢ ( suc 𝐵 ∈ On → ( ∅ ∈ suc 𝐵 ↔ ( ∅ ↑o suc 𝐵 ) = ∅ ) ) |
15 |
13 14
|
syl |
⊢ ( suc 𝐵 ∈ 𝑋 → ( ∅ ∈ suc 𝐵 ↔ ( ∅ ↑o suc 𝐵 ) = ∅ ) ) |
16 |
11 15
|
sylbi |
⊢ ( 𝐵 ∈ 𝑋 → ( ∅ ∈ suc 𝐵 ↔ ( ∅ ↑o suc 𝐵 ) = ∅ ) ) |
17 |
9 16
|
mpbid |
⊢ ( 𝐵 ∈ 𝑋 → ( ∅ ↑o suc 𝐵 ) = ∅ ) |
18 |
3 17
|
sylan9eqr |
⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o suc 𝐵 ) = ∅ ) |
19 |
|
oveq1 |
⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) = ( ∅ ↑o 𝐵 ) ) |
20 |
|
id |
⊢ ( 𝐴 = ∅ → 𝐴 = ∅ ) |
21 |
19 20
|
oveq12d |
⊢ ( 𝐴 = ∅ → ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) = ( ( ∅ ↑o 𝐵 ) ·o ∅ ) ) |
22 |
|
ordelon |
⊢ ( ( Ord 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ On ) |
23 |
5 22
|
mpan |
⊢ ( 𝐵 ∈ 𝑋 → 𝐵 ∈ On ) |
24 |
|
oveq2 |
⊢ ( 𝐵 = ∅ → ( ∅ ↑o 𝐵 ) = ( ∅ ↑o ∅ ) ) |
25 |
|
oe0m0 |
⊢ ( ∅ ↑o ∅ ) = 1o |
26 |
|
1on |
⊢ 1o ∈ On |
27 |
25 26
|
eqeltri |
⊢ ( ∅ ↑o ∅ ) ∈ On |
28 |
24 27
|
eqeltrdi |
⊢ ( 𝐵 = ∅ → ( ∅ ↑o 𝐵 ) ∈ On ) |
29 |
28
|
adantl |
⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐵 = ∅ ) → ( ∅ ↑o 𝐵 ) ∈ On ) |
30 |
|
oe0m1 |
⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ ( ∅ ↑o 𝐵 ) = ∅ ) ) |
31 |
23 30
|
syl |
⊢ ( 𝐵 ∈ 𝑋 → ( ∅ ∈ 𝐵 ↔ ( ∅ ↑o 𝐵 ) = ∅ ) ) |
32 |
31
|
biimpa |
⊢ ( ( 𝐵 ∈ 𝑋 ∧ ∅ ∈ 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∅ ) |
33 |
|
0elon |
⊢ ∅ ∈ On |
34 |
32 33
|
eqeltrdi |
⊢ ( ( 𝐵 ∈ 𝑋 ∧ ∅ ∈ 𝐵 ) → ( ∅ ↑o 𝐵 ) ∈ On ) |
35 |
34
|
adantll |
⊢ ( ( ( 𝐵 ∈ On ∧ 𝐵 ∈ 𝑋 ) ∧ ∅ ∈ 𝐵 ) → ( ∅ ↑o 𝐵 ) ∈ On ) |
36 |
29 35
|
oe0lem |
⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ∈ 𝑋 ) → ( ∅ ↑o 𝐵 ) ∈ On ) |
37 |
23 36
|
mpancom |
⊢ ( 𝐵 ∈ 𝑋 → ( ∅ ↑o 𝐵 ) ∈ On ) |
38 |
|
om0 |
⊢ ( ( ∅ ↑o 𝐵 ) ∈ On → ( ( ∅ ↑o 𝐵 ) ·o ∅ ) = ∅ ) |
39 |
37 38
|
syl |
⊢ ( 𝐵 ∈ 𝑋 → ( ( ∅ ↑o 𝐵 ) ·o ∅ ) = ∅ ) |
40 |
21 39
|
sylan9eqr |
⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 = ∅ ) → ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) = ∅ ) |
41 |
18 40
|
eqtr4d |
⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o suc 𝐵 ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) ) |
42 |
2
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝑋 ) ∧ ∅ ∈ 𝐴 ) → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) ) |
43 |
11 13
|
sylbi |
⊢ ( 𝐵 ∈ 𝑋 → suc 𝐵 ∈ On ) |
44 |
|
oevn0 |
⊢ ( ( ( 𝐴 ∈ On ∧ suc 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ suc 𝐵 ) ) |
45 |
43 44
|
sylanl2 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝑋 ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ suc 𝐵 ) ) |
46 |
|
ovex |
⊢ ( 𝐴 ↑o 𝐵 ) ∈ V |
47 |
|
oveq1 |
⊢ ( 𝑥 = ( 𝐴 ↑o 𝐵 ) → ( 𝑥 ·o 𝐴 ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) ) |
48 |
|
eqid |
⊢ ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) = ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) |
49 |
|
ovex |
⊢ ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) ∈ V |
50 |
47 48 49
|
fvmpt |
⊢ ( ( 𝐴 ↑o 𝐵 ) ∈ V → ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( 𝐴 ↑o 𝐵 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) ) |
51 |
46 50
|
ax-mp |
⊢ ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( 𝐴 ↑o 𝐵 ) ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) |
52 |
|
oevn0 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) |
53 |
23 52
|
sylanl2 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝑋 ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) |
54 |
53
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝑋 ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( 𝐴 ↑o 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) ) |
55 |
51 54
|
eqtr3id |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝑋 ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) ) |
56 |
42 45 55
|
3eqtr4d |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝑋 ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o suc 𝐵 ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) ) |
57 |
41 56
|
oe0lem |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ↑o suc 𝐵 ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) ) |