Metamath Proof Explorer

Theorem oeoelem

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

Ref Expression
Hypotheses oeoelem.1 ⊢ 𝐴 ∈ On
oeoelem.2 ⊢ ∅ ∈ 𝐴
Assertion oeoelem ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) ↑o 𝐶 ) = ( 𝐴 ↑o ( 𝐵 ·o 𝐶 ) ) )

Proof

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