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

Proof

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