Theorem om2uzoi

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

	Ref	Expression
Hypotheses	om2uz.1	⊢ 𝐶 ∈ ℤ
	om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
Assertion	om2uzoi	⊢ 𝐺 = OrdIso ( < , ( ℤ≥ ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	⊢ 𝐶 ∈ ℤ
2		om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3		ordom	⊢ Ord ω
4	1 2	om2uzisoi	⊢ 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 𝐶 ) )
5	3 4	pm3.2i	⊢ ( Ord ω ∧ 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 𝐶 ) ) )
6		ordwe	⊢ ( Ord ω → E We ω )
7	3 6	ax-mp	⊢ E We ω
8		isowe	⊢ ( 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 𝐶 ) ) → ( E We ω ↔ < We ( ℤ≥ ‘ 𝐶 ) ) )
9	4 8	ax-mp	⊢ ( E We ω ↔ < We ( ℤ≥ ‘ 𝐶 ) )
10	7 9	mpbi	⊢ < We ( ℤ≥ ‘ 𝐶 )
11		fvex	⊢ ( ℤ≥ ‘ 𝐶 ) ∈ V
12		exse	⊢ ( ( ℤ≥ ‘ 𝐶 ) ∈ V → < Se ( ℤ≥ ‘ 𝐶 ) )
13	11 12	ax-mp	⊢ < Se ( ℤ≥ ‘ 𝐶 )
14		eqid	⊢ OrdIso ( < , ( ℤ≥ ‘ 𝐶 ) ) = OrdIso ( < , ( ℤ≥ ‘ 𝐶 ) )
15	14	oieu	⊢ ( ( < We ( ℤ≥ ‘ 𝐶 ) ∧ < Se ( ℤ≥ ‘ 𝐶 ) ) → ( ( Ord ω ∧ 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 𝐶 ) ) ) ↔ ( ω = dom OrdIso ( < , ( ℤ≥ ‘ 𝐶 ) ) ∧ 𝐺 = OrdIso ( < , ( ℤ≥ ‘ 𝐶 ) ) ) ) )
16	10 13 15	mp2an	⊢ ( ( Ord ω ∧ 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 𝐶 ) ) ) ↔ ( ω = dom OrdIso ( < , ( ℤ≥ ‘ 𝐶 ) ) ∧ 𝐺 = OrdIso ( < , ( ℤ≥ ‘ 𝐶 ) ) ) )
17	5 16	mpbi	⊢ ( ω = dom OrdIso ( < , ( ℤ≥ ‘ 𝐶 ) ) ∧ 𝐺 = OrdIso ( < , ( ℤ≥ ‘ 𝐶 ) ) )
18	17	simpri	⊢ 𝐺 = OrdIso ( < , ( ℤ≥ ‘ 𝐶 ) )