This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ZZ>= ` A )

Proof

Step Hyp Ref Expression
1 ordom 
 |-  Ord _om
2 ordwe 
 |-  ( Ord _om -> _E We _om )
3 1 2 ax-mp 
 |-  _E We _om
4 rdgeq2 
 |-  ( A = if ( A e. ZZ , A , 0 ) -> rec ( ( x e. _V |-> ( x + 1 ) ) , A ) = rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) )
5 4 reseq1d 
 |-  ( A = if ( A e. ZZ , A , 0 ) -> ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om ) )
6 isoeq1 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` A ) ) <-> ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` A ) ) ) )
7 5 6 syl 
 |-  ( A = if ( A e. ZZ , A , 0 ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` A ) ) <-> ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` A ) ) ) )
8 fveq2 
 |-  ( A = if ( A e. ZZ , A , 0 ) -> ( ZZ>= ` A ) = ( ZZ>= ` if ( A e. ZZ , A , 0 ) ) )
9 isoeq5 
 |-  ( ( ZZ>= ` A ) = ( ZZ>= ` if ( A e. ZZ , A , 0 ) ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` A ) ) <-> ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` if ( A e. ZZ , A , 0 ) ) ) ) )
10 8 9 syl 
 |-  ( A = if ( A e. ZZ , A , 0 ) -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` A ) ) <-> ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` if ( A e. ZZ , A , 0 ) ) ) ) )
11 0z 
 |-  0 e. ZZ
12 11 elimel 
 |-  if ( A e. ZZ , A , 0 ) e. ZZ
13 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om )
14 12 13 om2uzisoi 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , if ( A e. ZZ , A , 0 ) ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` if ( A e. ZZ , A , 0 ) ) )
15 7 10 14 dedth2v 
 |-  ( A e. ZZ -> ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` A ) ) )
16 isocnv 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) Isom _E , < ( _om , ( ZZ>= ` A ) ) -> `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) Isom < , _E ( ( ZZ>= ` A ) , _om ) )
17 15 16 syl 
 |-  ( A e. ZZ -> `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) Isom < , _E ( ( ZZ>= ` A ) , _om ) )
18 dmres 
 |-  dom ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) = ( _om i^i dom rec ( ( x e. _V |-> ( x + 1 ) ) , A ) )
19 omex 
 |-  _om e. _V
20 19 inex1 
 |-  ( _om i^i dom rec ( ( x e. _V |-> ( x + 1 ) ) , A ) ) e. _V
21 18 20 eqeltri 
 |-  dom ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) e. _V
22 cnvimass 
 |-  ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) " y ) C_ dom ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om )
23 21 22 ssexi 
 |-  ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) " y ) e. _V
24 23 ax-gen 
 |-  A. y ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) " y ) e. _V
25 isowe2 
 |-  ( ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) Isom < , _E ( ( ZZ>= ` A ) , _om ) /\ A. y ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , A ) |` _om ) " y ) e. _V ) -> ( _E We _om -> < We ( ZZ>= ` A ) ) )
26 17 24 25 sylancl 
 |-  ( A e. ZZ -> ( _E We _om -> < We ( ZZ>= ` A ) ) )
27 3 26 mpi 
 |-  ( A e. ZZ -> < We ( ZZ>= ` A ) )
28 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
29 28 fdmi 
 |-  dom ZZ>= = ZZ
30 27 29 eleq2s 
 |-  ( A e. dom ZZ>= -> < We ( ZZ>= ` A ) )
31 we0 
 |-  < We (/)
32 ndmfv 
 |-  ( -. A e. dom ZZ>= -> ( ZZ>= ` A ) = (/) )
33 weeq2 
 |-  ( ( ZZ>= ` A ) = (/) -> ( < We ( ZZ>= ` A ) <-> < We (/) ) )
34 32 33 syl 
 |-  ( -. A e. dom ZZ>= -> ( < We ( ZZ>= ` A ) <-> < We (/) ) )
35 31 34 mpbiri 
 |-  ( -. A e. dom ZZ>= -> < We ( ZZ>= ` A ) )
36 30 35 pm2.61i 
 |-  < We ( ZZ>= ` A )