Metamath Proof Explorer

Theorem oeoelem

Description: Lemma for oeoe . (Contributed by Eric Schmidt, 26-May-2009)

Ref Expression
Hypotheses oeoelem.1 ⊢ A ∈ On
oeoelem.2 ⊢ ∅ ∈ A
Assertion oeoelem ⊢ B ∈ On ∧ C ∈ On → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C

Proof

Step Hyp Ref Expression
1 oeoelem.1 ⊢ A ∈ On
2 oeoelem.2 ⊢ ∅ ∈ A
3 oveq2 ⊢ x = ∅ → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ↑ 𝑜 ∅
4 oveq2 ⊢ x = ∅ → B ⋅ 𝑜 x = B ⋅ 𝑜 ∅
5 4 oveq2d ⊢ x = ∅ → A ↑ 𝑜 B ⋅ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 ∅
6 3 5 eqeq12d ⊢ x = ∅ → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 x ↔ A ↑ 𝑜 B ↑ 𝑜 ∅ = A ↑ 𝑜 B ⋅ 𝑜 ∅
7 oveq2 ⊢ x = y → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ↑ 𝑜 y
8 oveq2 ⊢ x = y → B ⋅ 𝑜 x = B ⋅ 𝑜 y
9 8 oveq2d ⊢ x = y → A ↑ 𝑜 B ⋅ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 y
10 7 9 eqeq12d ⊢ x = y → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 x ↔ A ↑ 𝑜 B ↑ 𝑜 y = A ↑ 𝑜 B ⋅ 𝑜 y
11 oveq2 ⊢ x = suc ⁡ y → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ↑ 𝑜 suc ⁡ y
12 oveq2 ⊢ x = suc ⁡ y → B ⋅ 𝑜 x = B ⋅ 𝑜 suc ⁡ y
13 12 oveq2d ⊢ x = suc ⁡ y → A ↑ 𝑜 B ⋅ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 suc ⁡ y
14 11 13 eqeq12d ⊢ x = suc ⁡ y → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 x ↔ A ↑ 𝑜 B ↑ 𝑜 suc ⁡ y = A ↑ 𝑜 B ⋅ 𝑜 suc ⁡ y
15 oveq2 ⊢ x = C → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ↑ 𝑜 C
16 oveq2 ⊢ x = C → B ⋅ 𝑜 x = B ⋅ 𝑜 C
17 16 oveq2d ⊢ x = C → A ↑ 𝑜 B ⋅ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 C
18 15 17 eqeq12d ⊢ x = C → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 x ↔ A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C
19 oecl ⊢ A ∈ On ∧ B ∈ On → A ↑ 𝑜 B ∈ On
20 1 19 mpan ⊢ B ∈ On → A ↑ 𝑜 B ∈ On
21 oe0 ⊢ A ↑ 𝑜 B ∈ On → A ↑ 𝑜 B ↑ 𝑜 ∅ = 1 𝑜
22 20 21 syl ⊢ B ∈ On → A ↑ 𝑜 B ↑ 𝑜 ∅ = 1 𝑜
23 om0 ⊢ B ∈ On → B ⋅ 𝑜 ∅ = ∅
24 23 oveq2d ⊢ B ∈ On → A ↑ 𝑜 B ⋅ 𝑜 ∅ = A ↑ 𝑜 ∅
25 oe0 ⊢ A ∈ On → A ↑ 𝑜 ∅ = 1 𝑜
26 1 25 ax-mp ⊢ A ↑ 𝑜 ∅ = 1 𝑜
27 24 26 eqtrdi ⊢ B ∈ On → A ↑ 𝑜 B ⋅ 𝑜 ∅ = 1 𝑜
28 22 27 eqtr4d ⊢ B ∈ On → A ↑ 𝑜 B ↑ 𝑜 ∅ = A ↑ 𝑜 B ⋅ 𝑜 ∅
29 oveq1 ⊢ A ↑ 𝑜 B ↑ 𝑜 y = A ↑ 𝑜 B ⋅ 𝑜 y → A ↑ 𝑜 B ↑ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B = A ↑ 𝑜 B ⋅ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B
30 oesuc ⊢ A ↑ 𝑜 B ∈ On ∧ y ∈ On → A ↑ 𝑜 B ↑ 𝑜 suc ⁡ y = A ↑ 𝑜 B ↑ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B
31 20 30 sylan ⊢ B ∈ On ∧ y ∈ On → A ↑ 𝑜 B ↑ 𝑜 suc ⁡ y = A ↑ 𝑜 B ↑ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B
32 omsuc ⊢ B ∈ On ∧ y ∈ On → B ⋅ 𝑜 suc ⁡ y = B ⋅ 𝑜 y + 𝑜 B
33 32 oveq2d ⊢ B ∈ On ∧ y ∈ On → A ↑ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ↑ 𝑜 B ⋅ 𝑜 y + 𝑜 B
34 omcl ⊢ B ∈ On ∧ y ∈ On → B ⋅ 𝑜 y ∈ On
35 oeoa ⊢ A ∈ On ∧ B ⋅ 𝑜 y ∈ On ∧ B ∈ On → A ↑ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ↑ 𝑜 B ⋅ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B
36 1 35 mp3an1 ⊢ B ⋅ 𝑜 y ∈ On ∧ B ∈ On → A ↑ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ↑ 𝑜 B ⋅ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B
37 34 36 sylan ⊢ B ∈ On ∧ y ∈ On ∧ B ∈ On → A ↑ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ↑ 𝑜 B ⋅ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B
38 37 anabss1 ⊢ B ∈ On ∧ y ∈ On → A ↑ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ↑ 𝑜 B ⋅ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B
39 33 38 eqtrd ⊢ B ∈ On ∧ y ∈ On → A ↑ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ↑ 𝑜 B ⋅ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B
40 31 39 eqeq12d ⊢ B ∈ On ∧ y ∈ On → A ↑ 𝑜 B ↑ 𝑜 suc ⁡ y = A ↑ 𝑜 B ⋅ 𝑜 suc ⁡ y ↔ A ↑ 𝑜 B ↑ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B = A ↑ 𝑜 B ⋅ 𝑜 y ⋅ 𝑜 A ↑ 𝑜 B
41 29 40 imbitrrid ⊢ B ∈ On ∧ y ∈ On → A ↑ 𝑜 B ↑ 𝑜 y = A ↑ 𝑜 B ⋅ 𝑜 y → A ↑ 𝑜 B ↑ 𝑜 suc ⁡ y = A ↑ 𝑜 B ⋅ 𝑜 suc ⁡ y
42 41 expcom ⊢ y ∈ On → B ∈ On → A ↑ 𝑜 B ↑ 𝑜 y = A ↑ 𝑜 B ⋅ 𝑜 y → A ↑ 𝑜 B ↑ 𝑜 suc ⁡ y = A ↑ 𝑜 B ⋅ 𝑜 suc ⁡ y
43 iuneq2 ⊢ ∀ y ∈ x A ↑ 𝑜 B ↑ 𝑜 y = A ↑ 𝑜 B ⋅ 𝑜 y → ⋃ y ∈ x A ↑ 𝑜 B ↑ 𝑜 y = ⋃ y ∈ x A ↑ 𝑜 B ⋅ 𝑜 y
44 vex ⊢ x ∈ V
45 oen0 ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ A → ∅ ∈ A ↑ 𝑜 B
46 2 45 mpan2 ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ A ↑ 𝑜 B
47 oelim ⊢ A ↑ 𝑜 B ∈ On ∧ x ∈ V ∧ Lim ⁡ x ∧ ∅ ∈ A ↑ 𝑜 B → A ↑ 𝑜 B ↑ 𝑜 x = ⋃ y ∈ x A ↑ 𝑜 B ↑ 𝑜 y
48 19 47 sylanl1 ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x ∧ ∅ ∈ A ↑ 𝑜 B → A ↑ 𝑜 B ↑ 𝑜 x = ⋃ y ∈ x A ↑ 𝑜 B ↑ 𝑜 y
49 46 48 mpidan ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → A ↑ 𝑜 B ↑ 𝑜 x = ⋃ y ∈ x A ↑ 𝑜 B ↑ 𝑜 y
50 1 49 mpanl1 ⊢ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → A ↑ 𝑜 B ↑ 𝑜 x = ⋃ y ∈ x A ↑ 𝑜 B ↑ 𝑜 y
51 44 50 mpanr1 ⊢ B ∈ On ∧ Lim ⁡ x → A ↑ 𝑜 B ↑ 𝑜 x = ⋃ y ∈ x A ↑ 𝑜 B ↑ 𝑜 y
52 omlim ⊢ B ∈ On ∧ x ∈ V ∧ Lim ⁡ x → B ⋅ 𝑜 x = ⋃ y ∈ x B ⋅ 𝑜 y
53 44 52 mpanr1 ⊢ B ∈ On ∧ Lim ⁡ x → B ⋅ 𝑜 x = ⋃ y ∈ x B ⋅ 𝑜 y
54 53 oveq2d ⊢ B ∈ On ∧ Lim ⁡ x → A ↑ 𝑜 B ⋅ 𝑜 x = A ↑ 𝑜 ⋃ y ∈ x B ⋅ 𝑜 y
55 limord ⊢ Lim ⁡ x → Ord ⁡ x
56 ordelon ⊢ Ord ⁡ x ∧ y ∈ x → y ∈ On
57 55 56 sylan ⊢ Lim ⁡ x ∧ y ∈ x → y ∈ On
58 57 34 sylan2 ⊢ B ∈ On ∧ Lim ⁡ x ∧ y ∈ x → B ⋅ 𝑜 y ∈ On
59 58 anassrs ⊢ B ∈ On ∧ Lim ⁡ x ∧ y ∈ x → B ⋅ 𝑜 y ∈ On
60 59 ralrimiva ⊢ B ∈ On ∧ Lim ⁡ x → ∀ y ∈ x B ⋅ 𝑜 y ∈ On
61 0ellim ⊢ Lim ⁡ x → ∅ ∈ x
62 61 ne0d ⊢ Lim ⁡ x → x ≠ ∅
63 62 adantl ⊢ B ∈ On ∧ Lim ⁡ x → x ≠ ∅
64 vex ⊢ w ∈ V
65 oelim ⊢ A ∈ On ∧ w ∈ V ∧ Lim ⁡ w ∧ ∅ ∈ A → A ↑ 𝑜 w = ⋃ z ∈ w A ↑ 𝑜 z
66 2 65 mpan2 ⊢ A ∈ On ∧ w ∈ V ∧ Lim ⁡ w → A ↑ 𝑜 w = ⋃ z ∈ w A ↑ 𝑜 z
67 1 66 mpan ⊢ w ∈ V ∧ Lim ⁡ w → A ↑ 𝑜 w = ⋃ z ∈ w A ↑ 𝑜 z
68 64 67 mpan ⊢ Lim ⁡ w → A ↑ 𝑜 w = ⋃ z ∈ w A ↑ 𝑜 z
69 oewordi ⊢ z ∈ On ∧ w ∈ On ∧ A ∈ On ∧ ∅ ∈ A → z ⊆ w → A ↑ 𝑜 z ⊆ A ↑ 𝑜 w
70 2 69 mpan2 ⊢ z ∈ On ∧ w ∈ On ∧ A ∈ On → z ⊆ w → A ↑ 𝑜 z ⊆ A ↑ 𝑜 w
71 1 70 mp3an3 ⊢ z ∈ On ∧ w ∈ On → z ⊆ w → A ↑ 𝑜 z ⊆ A ↑ 𝑜 w
72 71 3impia ⊢ z ∈ On ∧ w ∈ On ∧ z ⊆ w → A ↑ 𝑜 z ⊆ A ↑ 𝑜 w
73 68 72 onoviun ⊢ x ∈ V ∧ ∀ y ∈ x B ⋅ 𝑜 y ∈ On ∧ x ≠ ∅ → A ↑ 𝑜 ⋃ y ∈ x B ⋅ 𝑜 y = ⋃ y ∈ x A ↑ 𝑜 B ⋅ 𝑜 y
74 44 60 63 73 mp3an2i ⊢ B ∈ On ∧ Lim ⁡ x → A ↑ 𝑜 ⋃ y ∈ x B ⋅ 𝑜 y = ⋃ y ∈ x A ↑ 𝑜 B ⋅ 𝑜 y
75 54 74 eqtrd ⊢ B ∈ On ∧ Lim ⁡ x → A ↑ 𝑜 B ⋅ 𝑜 x = ⋃ y ∈ x A ↑ 𝑜 B ⋅ 𝑜 y
76 51 75 eqeq12d ⊢ B ∈ On ∧ Lim ⁡ x → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 x ↔ ⋃ y ∈ x A ↑ 𝑜 B ↑ 𝑜 y = ⋃ y ∈ x A ↑ 𝑜 B ⋅ 𝑜 y
77 43 76 imbitrrid ⊢ B ∈ On ∧ Lim ⁡ x → ∀ y ∈ x A ↑ 𝑜 B ↑ 𝑜 y = A ↑ 𝑜 B ⋅ 𝑜 y → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 x
78 77 expcom ⊢ Lim ⁡ x → B ∈ On → ∀ y ∈ x A ↑ 𝑜 B ↑ 𝑜 y = A ↑ 𝑜 B ⋅ 𝑜 y → A ↑ 𝑜 B ↑ 𝑜 x = A ↑ 𝑜 B ⋅ 𝑜 x
79 6 10 14 18 28 42 78 tfinds3 ⊢ C ∈ On → B ∈ On → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C
80 79 impcom ⊢ B ∈ On ∧ C ∈ On → A ↑ 𝑜 B ↑ 𝑜 C = A ↑ 𝑜 B ⋅ 𝑜 C