Metamath Proof Explorer

Theorem oen0

Description: Ordinal exponentiation with a nonzero mantissa is nonzero. Proposition 8.32 of TakeutiZaring p. 67. (Contributed by NM, 4-Jan-2005)

Ref Expression
Assertion oen0 ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ∅ ∈ ( 𝐴 ↑o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o ∅ ) )
2 1 eleq2d ⊢ ( 𝑥 = ∅ → ( ∅ ∈ ( 𝐴 ↑o 𝑥 ) ↔ ∅ ∈ ( 𝐴 ↑o ∅ ) ) )
3 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝑦 ) )
4 3 eleq2d ⊢ ( 𝑥 = 𝑦 → ( ∅ ∈ ( 𝐴 ↑o 𝑥 ) ↔ ∅ ∈ ( 𝐴 ↑o 𝑦 ) ) )
5 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o suc 𝑦 ) )
6 5 eleq2d ⊢ ( 𝑥 = suc 𝑦 → ( ∅ ∈ ( 𝐴 ↑o 𝑥 ) ↔ ∅ ∈ ( 𝐴 ↑o suc 𝑦 ) ) )
7 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝐵 ) )
8 7 eleq2d ⊢ ( 𝑥 = 𝐵 → ( ∅ ∈ ( 𝐴 ↑o 𝑥 ) ↔ ∅ ∈ ( 𝐴 ↑o 𝐵 ) ) )
9 0lt1o ⊢ ∅ ∈ 1o
10 oe0 ⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o ∅ ) = 1o )
11 9 10 eleqtrrid ⊢ ( 𝐴 ∈ On → ∅ ∈ ( 𝐴 ↑o ∅ ) )
12 11 adantr ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ∅ ∈ ( 𝐴 ↑o ∅ ) )
13 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
14 omordi ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐴 ↑o 𝑦 ) ∈ On ) ∧ ∅ ∈ ( 𝐴 ↑o 𝑦 ) ) → ( ∅ ∈ 𝐴 → ( ( 𝐴 ↑o 𝑦 ) ·o ∅ ) ∈ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
15 om0 ⊢ ( ( 𝐴 ↑o 𝑦 ) ∈ On → ( ( 𝐴 ↑o 𝑦 ) ·o ∅ ) = ∅ )
16 15 eleq1d ⊢ ( ( 𝐴 ↑o 𝑦 ) ∈ On → ( ( ( 𝐴 ↑o 𝑦 ) ·o ∅ ) ∈ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ↔ ∅ ∈ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
17 16 ad2antlr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐴 ↑o 𝑦 ) ∈ On ) ∧ ∅ ∈ ( 𝐴 ↑o 𝑦 ) ) → ( ( ( 𝐴 ↑o 𝑦 ) ·o ∅ ) ∈ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ↔ ∅ ∈ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
18 14 17 sylibd ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐴 ↑o 𝑦 ) ∈ On ) ∧ ∅ ∈ ( 𝐴 ↑o 𝑦 ) ) → ( ∅ ∈ 𝐴 → ∅ ∈ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
19 13 18 syldanl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) ∧ ∅ ∈ ( 𝐴 ↑o 𝑦 ) ) → ( ∅ ∈ 𝐴 → ∅ ∈ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
20 oesuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o suc 𝑦 ) = ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) )
21 20 eleq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ∅ ∈ ( 𝐴 ↑o suc 𝑦 ) ↔ ∅ ∈ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) ∧ ∅ ∈ ( 𝐴 ↑o 𝑦 ) ) → ( ∅ ∈ ( 𝐴 ↑o suc 𝑦 ) ↔ ∅ ∈ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ) )
23 19 22 sylibrd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) ∧ ∅ ∈ ( 𝐴 ↑o 𝑦 ) ) → ( ∅ ∈ 𝐴 → ∅ ∈ ( 𝐴 ↑o suc 𝑦 ) ) )
24 23 exp31 ⊢ ( 𝐴 ∈ On → ( 𝑦 ∈ On → ( ∅ ∈ ( 𝐴 ↑o 𝑦 ) → ( ∅ ∈ 𝐴 → ∅ ∈ ( 𝐴 ↑o suc 𝑦 ) ) ) ) )
25 24 com12 ⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( ∅ ∈ ( 𝐴 ↑o 𝑦 ) → ( ∅ ∈ 𝐴 → ∅ ∈ ( 𝐴 ↑o suc 𝑦 ) ) ) ) )
26 25 com34 ⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 → ( ∅ ∈ ( 𝐴 ↑o 𝑦 ) → ∅ ∈ ( 𝐴 ↑o suc 𝑦 ) ) ) ) )
27 26 impd ⊢ ( 𝑦 ∈ On → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ∅ ∈ ( 𝐴 ↑o 𝑦 ) → ∅ ∈ ( 𝐴 ↑o suc 𝑦 ) ) ) )
28 0ellim ⊢ ( Lim 𝑥 → ∅ ∈ 𝑥 )
29 eqimss2 ⊢ ( ( 𝐴 ↑o ∅ ) = 1o → 1o ⊆ ( 𝐴 ↑o ∅ ) )
30 10 29 syl ⊢ ( 𝐴 ∈ On → 1o ⊆ ( 𝐴 ↑o ∅ ) )
31 oveq2 ⊢ ( 𝑦 = ∅ → ( 𝐴 ↑o 𝑦 ) = ( 𝐴 ↑o ∅ ) )
32 31 sseq2d ⊢ ( 𝑦 = ∅ → ( 1o ⊆ ( 𝐴 ↑o 𝑦 ) ↔ 1o ⊆ ( 𝐴 ↑o ∅ ) ) )
33 32 rspcev ⊢ ( ( ∅ ∈ 𝑥 ∧ 1o ⊆ ( 𝐴 ↑o ∅ ) ) → ∃ 𝑦 ∈ 𝑥 1o ⊆ ( 𝐴 ↑o 𝑦 ) )
34 28 30 33 syl2an ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) → ∃ 𝑦 ∈ 𝑥 1o ⊆ ( 𝐴 ↑o 𝑦 ) )
35 ssiun ⊢ ( ∃ 𝑦 ∈ 𝑥 1o ⊆ ( 𝐴 ↑o 𝑦 ) → 1o ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
36 34 35 syl ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) → 1o ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
37 36 adantrr ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → 1o ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
38 vex ⊢ 𝑥 ∈ V
39 oelim ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
40 38 39 mpanlr1 ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
41 40 anasss ⊢ ( ( 𝐴 ∈ On ∧ ( Lim 𝑥 ∧ ∅ ∈ 𝐴 ) ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
42 41 an12s ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
43 37 42 sseqtrrd ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → 1o ⊆ ( 𝐴 ↑o 𝑥 ) )
44 limelon ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → 𝑥 ∈ On )
45 38 44 mpan ⊢ ( Lim 𝑥 → 𝑥 ∈ On )
46 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 ↑o 𝑥 ) ∈ On )
47 46 ancoms ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐴 ↑o 𝑥 ) ∈ On )
48 45 47 sylan ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) → ( 𝐴 ↑o 𝑥 ) ∈ On )
49 eloni ⊢ ( ( 𝐴 ↑o 𝑥 ) ∈ On → Ord ( 𝐴 ↑o 𝑥 ) )
50 ordgt0ge1 ⊢ ( Ord ( 𝐴 ↑o 𝑥 ) → ( ∅ ∈ ( 𝐴 ↑o 𝑥 ) ↔ 1o ⊆ ( 𝐴 ↑o 𝑥 ) ) )
51 48 49 50 3syl ⊢ ( ( Lim 𝑥 ∧ 𝐴 ∈ On ) → ( ∅ ∈ ( 𝐴 ↑o 𝑥 ) ↔ 1o ⊆ ( 𝐴 ↑o 𝑥 ) ) )
52 51 adantrr ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( ∅ ∈ ( 𝐴 ↑o 𝑥 ) ↔ 1o ⊆ ( 𝐴 ↑o 𝑥 ) ) )
53 43 52 mpbird ⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ∅ ∈ ( 𝐴 ↑o 𝑥 ) )
54 53 ex ⊢ ( Lim 𝑥 → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ∅ ∈ ( 𝐴 ↑o 𝑥 ) ) )
55 54 a1dd ⊢ ( Lim 𝑥 → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ∅ ∈ ( 𝐴 ↑o 𝑦 ) → ∅ ∈ ( 𝐴 ↑o 𝑥 ) ) ) )
56 2 4 6 8 12 27 55 tfinds3 ⊢ ( 𝐵 ∈ On → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ∅ ∈ ( 𝐴 ↑o 𝐵 ) ) )
57 56 expd ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 → ∅ ∈ ( 𝐴 ↑o 𝐵 ) ) ) )
58 57 com12 ⊢ ( 𝐴 ∈ On → ( 𝐵 ∈ On → ( ∅ ∈ 𝐴 → ∅ ∈ ( 𝐴 ↑o 𝐵 ) ) ) )
59 58 imp31 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ∅ ∈ ( 𝐴 ↑o 𝐵 ) )