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 𝐵 ) ) )