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 ⁡ X
oesuclem.2 ⊢ B ∈ X → rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ suc ⁡ B = x ∈ V ⟼ x ⋅ 𝑜 A ⁡ rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
Assertion oesuclem ⊢ A ∈ On ∧ B ∈ X → A ↑ 𝑜 suc ⁡ B = A ↑ 𝑜 B ⋅ 𝑜 A

Proof

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