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

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 ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
Assertion oemapwe ( 𝜑 → ( 𝑇 We 𝑆 ∧ dom OrdIso ( 𝑇 , 𝑆 ) = ( 𝐴 ↑o 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
5 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
6 2 3 5 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↑o 𝐵 ) ∈ On )
7 eloni ⊢ ( ( 𝐴 ↑o 𝐵 ) ∈ On → Ord ( 𝐴 ↑o 𝐵 ) )
8 ordwe ⊢ ( Ord ( 𝐴 ↑o 𝐵 ) → E We ( 𝐴 ↑o 𝐵 ) )
9 6 7 8 3syl ⊢ ( 𝜑 → E We ( 𝐴 ↑o 𝐵 ) )
10 1 2 3 4 cantnf ⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) )
11 isowe ⊢ ( ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) → ( 𝑇 We 𝑆 ↔ E We ( 𝐴 ↑o 𝐵 ) ) )
12 10 11 syl ⊢ ( 𝜑 → ( 𝑇 We 𝑆 ↔ E We ( 𝐴 ↑o 𝐵 ) ) )
13 9 12 mpbird ⊢ ( 𝜑 → 𝑇 We 𝑆 )
14 6 7 syl ⊢ ( 𝜑 → Ord ( 𝐴 ↑o 𝐵 ) )
15 isocnv ⊢ ( ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) → ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) )
16 10 15 syl ⊢ ( 𝜑 → ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) )
17 ovex ⊢ ( 𝐴 CNF 𝐵 ) ∈ V
18 17 dmex ⊢ dom ( 𝐴 CNF 𝐵 ) ∈ V
19 1 18 eqeltri ⊢ 𝑆 ∈ V
20 exse ⊢ ( 𝑆 ∈ V → 𝑇 Se 𝑆 )
21 19 20 ax-mp ⊢ 𝑇 Se 𝑆
22 eqid ⊢ OrdIso ( 𝑇 , 𝑆 ) = OrdIso ( 𝑇 , 𝑆 )
23 22 oieu ⊢ ( ( 𝑇 We 𝑆 ∧ 𝑇 Se 𝑆 ) → ( ( Ord ( 𝐴 ↑o 𝐵 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) ) ↔ ( ( 𝐴 ↑o 𝐵 ) = dom OrdIso ( 𝑇 , 𝑆 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) ) ) )
24 13 21 23 sylancl ⊢ ( 𝜑 → ( ( Ord ( 𝐴 ↑o 𝐵 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) ) ↔ ( ( 𝐴 ↑o 𝐵 ) = dom OrdIso ( 𝑇 , 𝑆 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) ) ) )
25 14 16 24 mpbi2and ⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝐵 ) = dom OrdIso ( 𝑇 , 𝑆 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) ) )
26 25 simpld ⊢ ( 𝜑 → ( 𝐴 ↑o 𝐵 ) = dom OrdIso ( 𝑇 , 𝑆 ) )
27 26 eqcomd ⊢ ( 𝜑 → dom OrdIso ( 𝑇 , 𝑆 ) = ( 𝐴 ↑o 𝐵 ) )
28 13 27 jca ⊢ ( 𝜑 → ( 𝑇 We 𝑆 ∧ dom OrdIso ( 𝑇 , 𝑆 ) = ( 𝐴 ↑o 𝐵 ) ) )