Metamath Proof Explorer

Theorem oesuclem

Description: Lemma for oesuc . (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Hypotheses oesuclem.1 ⊢ Lim 𝑋
oesuclem.2 ⊢ ( 𝐵 ∈ 𝑋 → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 ·o 𝐴 ) ) , 1o ) ‘ 𝐵 ) ) )
Assertion oesuclem ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ↑o suc 𝐵 ) = ( ( 𝐴 ↑o 𝐵 ) ·o 𝐴 ) )

Proof

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 syl5eqr ⊢ ( ( ( 𝐴 ∈ 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 𝐴 ) )