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	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
Assertion	oemapwe	$⊢ φ \to (T We S \land dom OrdIso (T, S) = A ↑_{𝑜} B)$

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	$⊢ S = dom (A CNF B)$
2		cantnfs.a	$⊢ φ \to A \in On$
3		cantnfs.b	$⊢ φ \to B \in On$
4		oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
5		oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$
6	2 3 5	syl2anc	$⊢ φ \to A ↑_{𝑜} B \in On$
7		eloni	$⊢ A ↑_{𝑜} B \in On \to Ord (A ↑_{𝑜} B)$
8		ordwe	$⊢ Ord (A ↑_{𝑜} B) \to E We (A ↑_{𝑜} B)$
9	6 7 8	3syl	$⊢ φ \to E We (A ↑_{𝑜} B)$
10	1 2 3 4	cantnf	$⊢ φ \to (A CNF B) {Isom}_{T, E} (S, A ↑_{𝑜} B)$
11		isowe	$⊢ (A CNF B) {Isom}_{T, E} (S, A ↑_{𝑜} B) \to (T We S \leftrightarrow E We (A ↑_{𝑜} B))$
12	10 11	syl	$⊢ φ \to (T We S \leftrightarrow E We (A ↑_{𝑜} B))$
13	9 12	mpbird	$⊢ φ \to T We S$
14	6 7	syl	$⊢ φ \to Ord (A ↑_{𝑜} B)$
15		isocnv	$⊢ (A CNF B) {Isom}_{T, E} (S, A ↑_{𝑜} B) \to {(A CNF B)}^{-1} {Isom}_{E, T} (A ↑_{𝑜} B, S)$
16	10 15	syl	$⊢ φ \to {(A CNF B)}^{-1} {Isom}_{E, T} (A ↑_{𝑜} B, S)$
17		ovex	$⊢ A CNF B \in V$
18	17	dmex	$⊢ dom (A CNF B) \in V$
19	1 18	eqeltri	$⊢ S \in V$
20		exse	$⊢ S \in V \to 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 \land T Se S) \to ((Ord (A ↑_{𝑜} B) \land {(A CNF B)}^{-1} {Isom}_{E, T} (A ↑_{𝑜} B, S)) \leftrightarrow (A ↑_{𝑜} B = dom OrdIso (T, S) \land {(A CNF B)}^{-1} = OrdIso (T, S)))$
24	13 21 23	sylancl	$⊢ φ \to ((Ord (A ↑_{𝑜} B) \land {(A CNF B)}^{-1} {Isom}_{E, T} (A ↑_{𝑜} B, S)) \leftrightarrow (A ↑_{𝑜} B = dom OrdIso (T, S) \land {(A CNF B)}^{-1} = OrdIso (T, S)))$
25	14 16 24	mpbi2and	$⊢ φ \to (A ↑_{𝑜} B = dom OrdIso (T, S) \land {(A CNF B)}^{-1} = OrdIso (T, S))$
26	25	simpld	$⊢ φ \to A ↑_{𝑜} B = dom OrdIso (T, S)$
27	26	eqcomd	$⊢ φ \to dom OrdIso (T, S) = A ↑_{𝑜} B$
28	13 27	jca	$⊢ φ \to (T We S \land dom OrdIso (T, S) = A ↑_{𝑜} B)$

Metamath Proof Explorer

Theorem oemapwe

Proof