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 ( < , ( ℤ≥ ‘ 𝐶 ) ) |