This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oeworde

Description: Ordinal exponentiation compared to its exponent. Proposition 8.37 of TakeutiZaring p. 68. Lemma 3.20 of Schloeder p. 10. (Contributed by NM, 7-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

Ref Expression
Assertion oeworde ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → 𝐵 ⊆ ( 𝐴 ↑o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
2 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o ∅ ) )
3 1 2 sseq12d ⊢ ( 𝑥 = ∅ → ( 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ↔ ∅ ⊆ ( 𝐴 ↑o ∅ ) ) )
4 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
5 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝑦 ) )
6 4 5 sseq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ↔ 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) ) )
7 id ⊢ ( 𝑥 = suc 𝑦 → 𝑥 = suc 𝑦 )
8 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o suc 𝑦 ) )
9 7 8 sseq12d ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ↔ suc 𝑦 ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
10 id ⊢ ( 𝑥 = 𝐵 → 𝑥 = 𝐵 )
11 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝐵 ) )
12 10 11 sseq12d ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ↔ 𝐵 ⊆ ( 𝐴 ↑o 𝐵 ) ) )
13 0ss ⊢ ∅ ⊆ ( 𝐴 ↑o ∅ )
14 13 a1i ⊢ ( 𝐴 ∈ ( On ∖ 2o ) → ∅ ⊆ ( 𝐴 ↑o ∅ ) )
15 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
16 eldifi ⊢ ( 𝐴 ∈ ( On ∖ 2o ) → 𝐴 ∈ On )
17 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
18 16 17 sylan ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
19 eloni ⊢ ( ( 𝐴 ↑o 𝑦 ) ∈ On → Ord ( 𝐴 ↑o 𝑦 ) )
20 18 19 syl ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → Ord ( 𝐴 ↑o 𝑦 ) )
21 ordsucsssuc ⊢ ( ( Ord 𝑦 ∧ Ord ( 𝐴 ↑o 𝑦 ) ) → ( 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) ↔ suc 𝑦 ⊆ suc ( 𝐴 ↑o 𝑦 ) ) )
22 15 20 21 syl2an2 ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) ↔ suc 𝑦 ⊆ suc ( 𝐴 ↑o 𝑦 ) ) )
23 onsuc ⊢ ( 𝑦 ∈ On → suc 𝑦 ∈ On )
24 oecl ⊢ ( ( 𝐴 ∈ On ∧ suc 𝑦 ∈ On ) → ( 𝐴 ↑o suc 𝑦 ) ∈ On )
25 16 23 24 syl2an ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o suc 𝑦 ) ∈ On )
26 eloni ⊢ ( ( 𝐴 ↑o suc 𝑦 ) ∈ On → Ord ( 𝐴 ↑o suc 𝑦 ) )
27 25 26 syl ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → Ord ( 𝐴 ↑o suc 𝑦 ) )
28 id ⊢ ( 𝐴 ∈ ( On ∖ 2o ) → 𝐴 ∈ ( On ∖ 2o ) )
29 vex ⊢ 𝑦 ∈ V
30 29 sucid ⊢ 𝑦 ∈ suc 𝑦
31 oeordi ⊢ ( ( suc 𝑦 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝑦 ∈ suc 𝑦 → ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o suc 𝑦 ) ) )
32 30 31 mpi ⊢ ( ( suc 𝑦 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o suc 𝑦 ) )
33 23 28 32 syl2anr ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o suc 𝑦 ) )
34 ordsucss ⊢ ( Ord ( 𝐴 ↑o suc 𝑦 ) → ( ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o suc 𝑦 ) → suc ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
35 27 33 34 sylc ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → suc ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) )
36 sstr2 ⊢ ( suc 𝑦 ⊆ suc ( 𝐴 ↑o 𝑦 ) → ( suc ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) → suc 𝑦 ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
37 35 36 syl5com ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( suc 𝑦 ⊆ suc ( 𝐴 ↑o 𝑦 ) → suc 𝑦 ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
38 22 37 sylbid ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → suc 𝑦 ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
39 38 expcom ⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ ( On ∖ 2o ) → ( 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → suc 𝑦 ⊆ ( 𝐴 ↑o suc 𝑦 ) ) ) )
40 dif20el ⊢ ( 𝐴 ∈ ( On ∖ 2o ) → ∅ ∈ 𝐴 )
41 16 40 jca ⊢ ( 𝐴 ∈ ( On ∖ 2o ) → ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) )
42 ss2iun ⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → ∪ 𝑦 ∈ 𝑥 𝑦 ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
43 limuni ⊢ ( Lim 𝑥 → 𝑥 = ∪ 𝑥 )
44 uniiun ⊢ ∪ 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦
45 43 44 eqtrdi ⊢ ( Lim 𝑥 → 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦 )
46 45 adantr ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦 )
47 vex ⊢ 𝑥 ∈ V
48 oelim ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
49 47 48 mpanlr1 ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
50 49 anasss ⊢ ( ( 𝐴 ∈ On ∧ ( Lim 𝑥 ∧ ∅ ∈ 𝐴 ) ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
51 50 an12s ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
52 46 51 sseq12d ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ↔ ∪ 𝑦 ∈ 𝑥 𝑦 ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ) )
53 42 52 imbitrrid ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ) )
54 53 ex ⊢ ( Lim 𝑥 → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ) ) )
55 41 54 syl5 ⊢ ( Lim 𝑥 → ( 𝐴 ∈ ( On ∖ 2o ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ) ) )
56 3 6 9 12 14 39 55 tfinds3 ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ ( On ∖ 2o ) → 𝐵 ⊆ ( 𝐴 ↑o 𝐵 ) ) )
57 56 impcom ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → 𝐵 ⊆ ( 𝐴 ↑o 𝐵 ) )