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