Metamath Proof Explorer

Theorem oemapwe

Description: The lexicographic order on a function space of ordinals gives a well-ordering with order type equal to the ordinal exponential. This provides an alternate definition of the ordinal exponential. (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s ⊢ S = dom ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
Assertion oemapwe ⊢ φ → T We S ∧ dom ⁡ OrdIso T S = A ↑ 𝑜 B

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
5 oecl ⊢ A ∈ On ∧ B ∈ On → A ↑ 𝑜 B ∈ On
6 2 3 5 syl2anc ⊢ φ → A ↑ 𝑜 B ∈ On
7 eloni ⊢ A ↑ 𝑜 B ∈ On → Ord ⁡ A ↑ 𝑜 B
8 ordwe ⊢ Ord ⁡ A ↑ 𝑜 B → E We A ↑ 𝑜 B
9 6 7 8 3syl ⊢ φ → E We A ↑ 𝑜 B
10 1 2 3 4 cantnf ⊢ φ → A CNF B Isom T , E S A ↑ 𝑜 B
11 isowe ⊢ A CNF B Isom T , E S A ↑ 𝑜 B → T We S ↔ E We A ↑ 𝑜 B
12 10 11 syl ⊢ φ → T We S ↔ E We A ↑ 𝑜 B
13 9 12 mpbird ⊢ φ → T We S
14 6 7 syl ⊢ φ → Ord ⁡ A ↑ 𝑜 B
15 isocnv ⊢ A CNF B Isom T , E S A ↑ 𝑜 B → A CNF B -1 Isom E , T A ↑ 𝑜 B S
16 10 15 syl ⊢ φ → A CNF B -1 Isom E , T A ↑ 𝑜 B S
17 ovex ⊢ A CNF B ∈ V
18 17 dmex ⊢ dom ⁡ A CNF B ∈ V
19 1 18 eqeltri ⊢ S ∈ V
20 exse ⊢ S ∈ V → T Se S
21 19 20 ax-mp ⊢ T Se S
22 eqid ⊢ OrdIso T S = OrdIso T S
23 22 oieu ⊢ T We S ∧ T Se S → Ord ⁡ A ↑ 𝑜 B ∧ A CNF B -1 Isom E , T A ↑ 𝑜 B S ↔ A ↑ 𝑜 B = dom ⁡ OrdIso T S ∧ A CNF B -1 = OrdIso T S
24 13 21 23 sylancl ⊢ φ → Ord ⁡ A ↑ 𝑜 B ∧ A CNF B -1 Isom E , T A ↑ 𝑜 B S ↔ A ↑ 𝑜 B = dom ⁡ OrdIso T S ∧ A CNF B -1 = OrdIso T S
25 14 16 24 mpbi2and ⊢ φ → A ↑ 𝑜 B = dom ⁡ OrdIso T S ∧ A CNF B -1 = OrdIso T S
26 25 simpld ⊢ φ → A ↑ 𝑜 B = dom ⁡ OrdIso T S
27 26 eqcomd ⊢ φ → dom ⁡ OrdIso T S = A ↑ 𝑜 B
28 13 27 jca ⊢ φ → T We S ∧ dom ⁡ OrdIso T S = A ↑ 𝑜 B