Metamath Proof Explorer


Theorem oeworde

Description: Ordinal exponentiation compared to its exponent. Proposition 8.37 of TakeutiZaring p. 68. (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 suceloni ( 𝑦 ∈ 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 syl5ibr ( ( 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 𝐵 ) )