Metamath Proof Explorer

Theorem ltweuz

Description: < is a well-founded relation on any sequence of upper integers. (Contributed by Andrew Salmon, 13-Nov-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion ltweuz ⊢ < We ℤ ≥ A

Proof

Step Hyp Ref Expression
1 ordom ⊢ Ord ⁡ ω
2 ordwe ⊢ Ord ⁡ ω → E We ω
3 1 2 ax-mp ⊢ E We ω
4 rdgeq2 ⊢ A = if A ∈ ℤ A 0 → rec ⁡ x ∈ V ⟼ x + 1 A = rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0
5 4 reseq1d ⊢ A = if A ∈ ℤ A 0 → rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω
6 isoeq1 ⊢ rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω → rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω Isom E , < ω ℤ ≥ A ↔ rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω Isom E , < ω ℤ ≥ A
7 5 6 syl ⊢ A = if A ∈ ℤ A 0 → rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω Isom E , < ω ℤ ≥ A ↔ rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω Isom E , < ω ℤ ≥ A
8 fveq2 ⊢ A = if A ∈ ℤ A 0 → ℤ ≥ A = ℤ ≥ if A ∈ ℤ A 0
9 isoeq5 ⊢ ℤ ≥ A = ℤ ≥ if A ∈ ℤ A 0 → rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω Isom E , < ω ℤ ≥ A ↔ rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω Isom E , < ω ℤ ≥ if A ∈ ℤ A 0
10 8 9 syl ⊢ A = if A ∈ ℤ A 0 → rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω Isom E , < ω ℤ ≥ A ↔ rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω Isom E , < ω ℤ ≥ if A ∈ ℤ A 0
11 0z ⊢ 0 ∈ ℤ
12 11 elimel ⊢ if A ∈ ℤ A 0 ∈ ℤ
13 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω
14 12 13 om2uzisoi ⊢ rec ⁡ x ∈ V ⟼ x + 1 if A ∈ ℤ A 0 ↾ ω Isom E , < ω ℤ ≥ if A ∈ ℤ A 0
15 7 10 14 dedth2v ⊢ A ∈ ℤ → rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω Isom E , < ω ℤ ≥ A
16 isocnv ⊢ rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω Isom E , < ω ℤ ≥ A → rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω -1 Isom < , E ℤ ≥ A ω
17 15 16 syl ⊢ A ∈ ℤ → rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω -1 Isom < , E ℤ ≥ A ω
18 dmres ⊢ dom ⁡ rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω = ω ∩ dom ⁡ rec ⁡ x ∈ V ⟼ x + 1 A
19 omex ⊢ ω ∈ V
20 19 inex1 ⊢ ω ∩ dom ⁡ rec ⁡ x ∈ V ⟼ x + 1 A ∈ V
21 18 20 eqeltri ⊢ dom ⁡ rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω ∈ V
22 cnvimass ⊢ rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω -1 y ⊆ dom ⁡ rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω
23 21 22 ssexi ⊢ rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω -1 y ∈ V
24 23 ax-gen ⊢ ∀ y rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω -1 y ∈ V
25 isowe2 ⊢ rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω -1 Isom < , E ℤ ≥ A ω ∧ ∀ y rec ⁡ x ∈ V ⟼ x + 1 A ↾ ω -1 y ∈ V → E We ω → < We ℤ ≥ A
26 17 24 25 sylancl ⊢ A ∈ ℤ → E We ω → < We ℤ ≥ A
27 3 26 mpi ⊢ A ∈ ℤ → < We ℤ ≥ A
28 uzf ⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ
29 28 fdmi ⊢ dom ⁡ ℤ ≥ = ℤ
30 27 29 eleq2s ⊢ A ∈ dom ⁡ ℤ ≥ → < We ℤ ≥ A
31 we0 ⊢ < We ∅
32 ndmfv ⊢ ¬ A ∈ dom ⁡ ℤ ≥ → ℤ ≥ A = ∅
33 weeq2 ⊢ ℤ ≥ A = ∅ → < We ℤ ≥ A ↔ < We ∅
34 32 33 syl ⊢ ¬ A ∈ dom ⁡ ℤ ≥ → < We ℤ ≥ A ↔ < We ∅
35 31 34 mpbiri ⊢ ¬ A ∈ dom ⁡ ℤ ≥ → < We ℤ ≥ A
36 30 35 pm2.61i ⊢ < We ℤ ≥ A