Metamath Proof Explorer

Theorem oeordsuc

Description: Ordering property of ordinal exponentiation with a successor exponent. Corollary 8.36 of TakeutiZaring p. 68. (Contributed by NM, 7-Jan-2005)

Ref Expression
Assertion oeordsuc ⊢B∈On∧C∈On→A∈B→A↑𝑜suc⁡C∈B↑𝑜suc⁡C

Proof

Step Hyp Ref Expression
1 onelon ⊢B∈On∧A∈B→A∈On
2 1 ex ⊢B∈On→A∈B→A∈On
3 2 adantr ⊢B∈On∧C∈On→A∈B→A∈On
4 oewordri ⊢B∈On∧C∈On→A∈B→A↑𝑜C⊆B↑𝑜C
5 4 3adant1 ⊢A∈On∧B∈On∧C∈On→A∈B→A↑𝑜C⊆B↑𝑜C
6 oecl ⊢A∈On∧C∈On→A↑𝑜C∈On
7 6 3adant2 ⊢A∈On∧B∈On∧C∈On→A↑𝑜C∈On
8 oecl ⊢B∈On∧C∈On→B↑𝑜C∈On
9 8 3adant1 ⊢A∈On∧B∈On∧C∈On→B↑𝑜C∈On
10 simp1 ⊢A∈On∧B∈On∧C∈On→A∈On
11 omwordri ⊢A↑𝑜C∈On∧B↑𝑜C∈On∧A∈On→A↑𝑜C⊆B↑𝑜C→A↑𝑜C⋅𝑜A⊆B↑𝑜C⋅𝑜A
12 7 9 10 11 syl3anc ⊢A∈On∧B∈On∧C∈On→A↑𝑜C⊆B↑𝑜C→A↑𝑜C⋅𝑜A⊆B↑𝑜C⋅𝑜A
13 5 12 syld ⊢A∈On∧B∈On∧C∈On→A∈B→A↑𝑜C⋅𝑜A⊆B↑𝑜C⋅𝑜A
14 oesuc ⊢A∈On∧C∈On→A↑𝑜suc⁡C=A↑𝑜C⋅𝑜A
15 14 3adant2 ⊢A∈On∧B∈On∧C∈On→A↑𝑜suc⁡C=A↑𝑜C⋅𝑜A
16 15 sseq1d ⊢A∈On∧B∈On∧C∈On→A↑𝑜suc⁡C⊆B↑𝑜C⋅𝑜A↔A↑𝑜C⋅𝑜A⊆B↑𝑜C⋅𝑜A
17 13 16 sylibrd ⊢A∈On∧B∈On∧C∈On→A∈B→A↑𝑜suc⁡C⊆B↑𝑜C⋅𝑜A
18 ne0i ⊢A∈B→B≠∅
19 on0eln0 ⊢B∈On→∅∈B↔B≠∅
20 18 19 imbitrrid ⊢B∈On→A∈B→∅∈B
21 20 adantr ⊢B∈On∧C∈On→A∈B→∅∈B
22 oen0 ⊢B∈On∧C∈On∧∅∈B→∅∈B↑𝑜C
23 22 ex ⊢B∈On∧C∈On→∅∈B→∅∈B↑𝑜C
24 21 23 syld ⊢B∈On∧C∈On→A∈B→∅∈B↑𝑜C
25 omordi ⊢B∈On∧B↑𝑜C∈On∧∅∈B↑𝑜C→A∈B→B↑𝑜C⋅𝑜A∈B↑𝑜C⋅𝑜B
26 8 25 syldanl ⊢B∈On∧C∈On∧∅∈B↑𝑜C→A∈B→B↑𝑜C⋅𝑜A∈B↑𝑜C⋅𝑜B
27 26 ex ⊢B∈On∧C∈On→∅∈B↑𝑜C→A∈B→B↑𝑜C⋅𝑜A∈B↑𝑜C⋅𝑜B
28 27 com23 ⊢B∈On∧C∈On→A∈B→∅∈B↑𝑜C→B↑𝑜C⋅𝑜A∈B↑𝑜C⋅𝑜B
29 24 28 mpdd ⊢B∈On∧C∈On→A∈B→B↑𝑜C⋅𝑜A∈B↑𝑜C⋅𝑜B
30 29 3adant1 ⊢A∈On∧B∈On∧C∈On→A∈B→B↑𝑜C⋅𝑜A∈B↑𝑜C⋅𝑜B
31 oesuc ⊢B∈On∧C∈On→B↑𝑜suc⁡C=B↑𝑜C⋅𝑜B
32 31 3adant1 ⊢A∈On∧B∈On∧C∈On→B↑𝑜suc⁡C=B↑𝑜C⋅𝑜B
33 32 eleq2d ⊢A∈On∧B∈On∧C∈On→B↑𝑜C⋅𝑜A∈B↑𝑜suc⁡C↔B↑𝑜C⋅𝑜A∈B↑𝑜C⋅𝑜B
34 30 33 sylibrd ⊢A∈On∧B∈On∧C∈On→A∈B→B↑𝑜C⋅𝑜A∈B↑𝑜suc⁡C
35 17 34 jcad ⊢A∈On∧B∈On∧C∈On→A∈B→A↑𝑜suc⁡C⊆B↑𝑜C⋅𝑜A∧B↑𝑜C⋅𝑜A∈B↑𝑜suc⁡C
36 35 3expa ⊢A∈On∧B∈On∧C∈On→A∈B→A↑𝑜suc⁡C⊆B↑𝑜C⋅𝑜A∧B↑𝑜C⋅𝑜A∈B↑𝑜suc⁡C
37 onsucb ⊢C∈On↔suc⁡C∈On
38 oecl ⊢A∈On∧suc⁡C∈On→A↑𝑜suc⁡C∈On
39 oecl ⊢B∈On∧suc⁡C∈On→B↑𝑜suc⁡C∈On
40 ontr2 ⊢A↑𝑜suc⁡C∈On∧B↑𝑜suc⁡C∈On→A↑𝑜suc⁡C⊆B↑𝑜C⋅𝑜A∧B↑𝑜C⋅𝑜A∈B↑𝑜suc⁡C→A↑𝑜suc⁡C∈B↑𝑜suc⁡C
41 38 39 40 syl2an ⊢A∈On∧suc⁡C∈On∧B∈On∧suc⁡C∈On→A↑𝑜suc⁡C⊆B↑𝑜C⋅𝑜A∧B↑𝑜C⋅𝑜A∈B↑𝑜suc⁡C→A↑𝑜suc⁡C∈B↑𝑜suc⁡C
42 41 anandirs ⊢A∈On∧B∈On∧suc⁡C∈On→A↑𝑜suc⁡C⊆B↑𝑜C⋅𝑜A∧B↑𝑜C⋅𝑜A∈B↑𝑜suc⁡C→A↑𝑜suc⁡C∈B↑𝑜suc⁡C
43 37 42 sylan2b ⊢A∈On∧B∈On∧C∈On→A↑𝑜suc⁡C⊆B↑𝑜C⋅𝑜A∧B↑𝑜C⋅𝑜A∈B↑𝑜suc⁡C→A↑𝑜suc⁡C∈B↑𝑜suc⁡C
44 36 43 syld ⊢A∈On∧B∈On∧C∈On→A∈B→A↑𝑜suc⁡C∈B↑𝑜suc⁡C
45 44 exp31 ⊢A∈On→B∈On→C∈On→A∈B→A↑𝑜suc⁡C∈B↑𝑜suc⁡C
46 45 com4l ⊢B∈On→C∈On→A∈B→A∈On→A↑𝑜suc⁡C∈B↑𝑜suc⁡C
47 46 imp ⊢B∈On∧C∈On→A∈B→A∈On→A↑𝑜suc⁡C∈B↑𝑜suc⁡C
48 3 47 mpdd ⊢B∈On∧C∈On→A∈B→A↑𝑜suc⁡C∈B↑𝑜suc⁡C