om2uzoi

Description: An alternative definition of G in terms of df-oi . (Contributed by Mario Carneiro, 2-Jun-2015)

Step	Hyp	Ref	Expression
1		om2uz.1	$⊢ C \in ℤ$
2		om2uz.2	$⊢ G = {rec ((x \in V ⟼ x + 1), C) ↾}_{ω}$
3		ordom	$⊢ Ord ω$
4	1 2	om2uzisoi	$⊢ G {Isom}_{E, <} (ω, ℤ_{\geq C})$
5	3 4	pm3.2i	$⊢ (Ord ω \land G {Isom}_{E, <} (ω, ℤ_{\geq C}))$
6		ordwe	$⊢ Ord ω \to E We ω$
7	3 6	ax-mp	$⊢ E We ω$
8		isowe	$⊢ G {Isom}_{E, <} (ω, ℤ_{\geq C}) \to (E We ω \leftrightarrow < We ℤ_{\geq C})$
9	4 8	ax-mp	$⊢ E We ω \leftrightarrow < We ℤ_{\geq C}$
10	7 9	mpbi	$⊢ < We ℤ_{\geq C}$
11		fvex	$⊢ ℤ_{\geq C} \in V$
12		exse	$⊢ ℤ_{\geq C} \in V \to < Se ℤ_{\geq C}$
13	11 12	ax-mp	$⊢ < Se ℤ_{\geq C}$
14		eqid	$⊢ OrdIso (< ℤ_{\geq C}) = OrdIso (< ℤ_{\geq C})$
15	14	oieu	$⊢ (< We ℤ_{\geq C} \land < Se ℤ_{\geq C}) \to ((Ord ω \land G {Isom}_{E, <} (ω, ℤ_{\geq C})) \leftrightarrow (ω = dom OrdIso (< ℤ_{\geq C}) \land G = OrdIso (< ℤ_{\geq C})))$
16	10 13 15	mp2an	$⊢ (Ord ω \land G {Isom}_{E, <} (ω, ℤ_{\geq C})) \leftrightarrow (ω = dom OrdIso (< ℤ_{\geq C}) \land G = OrdIso (< ℤ_{\geq C}))$
17	5 16	mpbi	$⊢ (ω = dom OrdIso (< ℤ_{\geq C}) \land G = OrdIso (< ℤ_{\geq C}))$
18	17	simpri	$⊢ G = OrdIso (< ℤ_{\geq C})$

Metamath Proof Explorer