Step | Hyp | Ref
| Expression |
1 | | ordom 7816 |
. . . . 5
β’ Ord
Ο |
2 | | ordwe 6334 |
. . . . 5
β’ (Ord
Ο β E We Ο) |
3 | 1, 2 | ax-mp 5 |
. . . 4
β’ E We
Ο |
4 | | rdgeq2 8362 |
. . . . . . . . 9
β’ (π΄ = if(π΄ β β€, π΄, 0) β rec((π₯ β V β¦ (π₯ + 1)), π΄) = rec((π₯ β V β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0))) |
5 | 4 | reseq1d 5940 |
. . . . . . . 8
β’ (π΄ = if(π΄ β β€, π΄, 0) β (rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) = (rec((π₯ β V β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ Ο)) |
6 | | isoeq1 7266 |
. . . . . . . 8
β’
((rec((π₯ β V
β¦ (π₯ + 1)), π΄) βΎ Ο) = (rec((π₯ β V β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ Ο) β ((rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) Isom E , < (Ο,
(β€β₯βπ΄)) β (rec((π₯ β V β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ Ο) Isom E , <
(Ο, (β€β₯βπ΄)))) |
7 | 5, 6 | syl 17 |
. . . . . . 7
β’ (π΄ = if(π΄ β β€, π΄, 0) β ((rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) Isom E , < (Ο,
(β€β₯βπ΄)) β (rec((π₯ β V β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ Ο) Isom E , <
(Ο, (β€β₯βπ΄)))) |
8 | | fveq2 6846 |
. . . . . . . 8
β’ (π΄ = if(π΄ β β€, π΄, 0) β
(β€β₯βπ΄) = (β€β₯βif(π΄ β β€, π΄, 0))) |
9 | | isoeq5 7270 |
. . . . . . . 8
β’
((β€β₯βπ΄) = (β€β₯βif(π΄ β β€, π΄, 0)) β ((rec((π₯ β V β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ Ο) Isom E , <
(Ο, (β€β₯βπ΄)) β (rec((π₯ β V β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ Ο) Isom E , <
(Ο, (β€β₯βif(π΄ β β€, π΄, 0))))) |
10 | 8, 9 | syl 17 |
. . . . . . 7
β’ (π΄ = if(π΄ β β€, π΄, 0) β ((rec((π₯ β V β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ Ο) Isom E , <
(Ο, (β€β₯βπ΄)) β (rec((π₯ β V β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ Ο) Isom E , <
(Ο, (β€β₯βif(π΄ β β€, π΄, 0))))) |
11 | | 0z 12518 |
. . . . . . . . 9
β’ 0 β
β€ |
12 | 11 | elimel 4559 |
. . . . . . . 8
β’ if(π΄ β β€, π΄, 0) β
β€ |
13 | | eqid 2733 |
. . . . . . . 8
β’
(rec((π₯ β V
β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ Ο) =
(rec((π₯ β V β¦
(π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ
Ο) |
14 | 12, 13 | om2uzisoi 13868 |
. . . . . . 7
β’
(rec((π₯ β V
β¦ (π₯ + 1)), if(π΄ β β€, π΄, 0)) βΎ Ο) Isom E ,
< (Ο, (β€β₯βif(π΄ β β€, π΄, 0))) |
15 | 7, 10, 14 | dedth2v 4552 |
. . . . . 6
β’ (π΄ β β€ β
(rec((π₯ β V β¦
(π₯ + 1)), π΄) βΎ Ο) Isom E , < (Ο,
(β€β₯βπ΄))) |
16 | | isocnv 7279 |
. . . . . 6
β’
((rec((π₯ β V
β¦ (π₯ + 1)), π΄) βΎ Ο) Isom E , <
(Ο, (β€β₯βπ΄)) β β‘(rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) Isom < , E
((β€β₯βπ΄), Ο)) |
17 | 15, 16 | syl 17 |
. . . . 5
β’ (π΄ β β€ β β‘(rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) Isom < , E
((β€β₯βπ΄), Ο)) |
18 | | dmres 5963 |
. . . . . . . 8
β’ dom
(rec((π₯ β V β¦
(π₯ + 1)), π΄) βΎ Ο) = (Ο β© dom
rec((π₯ β V β¦
(π₯ + 1)), π΄)) |
19 | | omex 9587 |
. . . . . . . . 9
β’ Ο
β V |
20 | 19 | inex1 5278 |
. . . . . . . 8
β’ (Ο
β© dom rec((π₯ β V
β¦ (π₯ + 1)), π΄)) β V |
21 | 18, 20 | eqeltri 2830 |
. . . . . . 7
β’ dom
(rec((π₯ β V β¦
(π₯ + 1)), π΄) βΎ Ο) β V |
22 | | cnvimass 6037 |
. . . . . . 7
β’ (β‘(rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) β π¦) β dom (rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) |
23 | 21, 22 | ssexi 5283 |
. . . . . 6
β’ (β‘(rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) β π¦) β V |
24 | 23 | ax-gen 1798 |
. . . . 5
β’
βπ¦(β‘(rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) β π¦) β V |
25 | | isowe2 7299 |
. . . . 5
β’ ((β‘(rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) Isom < , E
((β€β₯βπ΄), Ο) β§ βπ¦(β‘(rec((π₯ β V β¦ (π₯ + 1)), π΄) βΎ Ο) β π¦) β V) β ( E We
Ο β < We (β€β₯βπ΄))) |
26 | 17, 24, 25 | sylancl 587 |
. . . 4
β’ (π΄ β β€ β ( E We
Ο β < We (β€β₯βπ΄))) |
27 | 3, 26 | mpi 20 |
. . 3
β’ (π΄ β β€ β < We
(β€β₯βπ΄)) |
28 | | uzf 12774 |
. . . 4
β’
β€β₯:β€βΆπ« β€ |
29 | 28 | fdmi 6684 |
. . 3
β’ dom
β€β₯ = β€ |
30 | 27, 29 | eleq2s 2852 |
. 2
β’ (π΄ β dom
β€β₯ β < We (β€β₯βπ΄)) |
31 | | we0 5632 |
. . 3
β’ < We
β
|
32 | | ndmfv 6881 |
. . . 4
β’ (Β¬
π΄ β dom
β€β₯ β (β€β₯βπ΄) = β
) |
33 | | weeq2 5626 |
. . . 4
β’
((β€β₯βπ΄) = β
β ( < We
(β€β₯βπ΄) β < We β
)) |
34 | 32, 33 | syl 17 |
. . 3
β’ (Β¬
π΄ β dom
β€β₯ β ( < We (β€β₯βπ΄) β < We
β
)) |
35 | 31, 34 | mpbiri 258 |
. 2
β’ (Β¬
π΄ β dom
β€β₯ β < We (β€β₯βπ΄)) |
36 | 30, 35 | pm2.61i 182 |
1
β’ < We
(β€β₯βπ΄) |