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 )