Step | Hyp | Ref
| Expression |
1 | | wofi 8209 |
. . 3
|
2 | | cnvso 5674 |
. . . 4
|
3 | | wofi 8209 |
. . . 4
|
4 | 2, 3 | sylanb 489 |
. . 3
|
5 | 1, 4 | jca 554 |
. 2
|
6 | | weso 5105 |
. . . 4
|
7 | 6 | adantr 481 |
. . 3
|
8 | | peano2 7086 |
. . . . . . . . 9
|
9 | | sucidg 5803 |
. . . . . . . . 9
|
10 | | vex 3203 |
. . . . . . . . . . . . 13
|
11 | | vex 3203 |
. . . . . . . . . . . . 13
|
12 | 10, 11 | brcnv 5305 |
. . . . . . . . . . . 12
|
13 | | epel 5032 |
. . . . . . . . . . . 12
|
14 | 12, 13 | bitri 264 |
. . . . . . . . . . 11
|
15 | | eleq2 2690 |
. . . . . . . . . . 11
|
16 | 14, 15 | syl5bb 272 |
. . . . . . . . . 10
|
17 | 16 | rspcev 3309 |
. . . . . . . . 9
|
18 | 8, 9, 17 | syl2anc 693 |
. . . . . . . 8
|
19 | | dfrex2 2996 |
. . . . . . . 8
|
20 | 18, 19 | sylib 208 |
. . . . . . 7
|
21 | 20 | nrex 3000 |
. . . . . 6
|
22 | | ordom 7074 |
. . . . . . . 8
|
23 | | eqid 2622 |
. . . . . . . . 9
OrdIso OrdIso |
24 | 23 | oicl 8434 |
. . . . . . . 8
OrdIso |
25 | | ordtri1 5756 |
. . . . . . . 8
OrdIso
OrdIso
OrdIso |
26 | 22, 24, 25 | mp2an 708 |
. . . . . . 7
OrdIso
OrdIso |
27 | | wofib.1 |
. . . . . . . . . . 11
|
28 | 23 | oion 8441 |
. . . . . . . . . . 11
OrdIso |
29 | 27, 28 | mp1i 13 |
. . . . . . . . . 10
OrdIso
OrdIso |
30 | | simpr 477 |
. . . . . . . . . 10
OrdIso
OrdIso |
31 | 29, 30 | ssexd 4805 |
. . . . . . . . 9
OrdIso
|
32 | 23 | oiiso 8442 |
. . . . . . . . . . . . 13
OrdIso
OrdIso |
33 | 27, 32 | mpan 706 |
. . . . . . . . . . . 12
OrdIso OrdIso |
34 | | isocnv2 6581 |
. . . . . . . . . . . 12
OrdIso
OrdIso OrdIso
OrdIso |
35 | 33, 34 | sylib 208 |
. . . . . . . . . . 11
OrdIso
OrdIso |
36 | | wefr 5104 |
. . . . . . . . . . 11
|
37 | | isofr 6592 |
. . . . . . . . . . . 12
OrdIso
OrdIso
OrdIso
|
38 | 37 | biimpar 502 |
. . . . . . . . . . 11
OrdIso
OrdIso
OrdIso |
39 | 35, 36, 38 | syl2an 494 |
. . . . . . . . . 10
OrdIso |
40 | 39 | adantr 481 |
. . . . . . . . 9
OrdIso
OrdIso |
41 | | 1onn 7719 |
. . . . . . . . . 10
|
42 | | ne0i 3921 |
. . . . . . . . . 10
|
43 | 41, 42 | mp1i 13 |
. . . . . . . . 9
OrdIso
|
44 | | fri 5076 |
. . . . . . . . 9
OrdIso OrdIso
|
45 | 31, 40, 30, 43, 44 | syl22anc 1327 |
. . . . . . . 8
OrdIso
|
46 | 45 | ex 450 |
. . . . . . 7
OrdIso
|
47 | 26, 46 | syl5bir 233 |
. . . . . 6
OrdIso
|
48 | 21, 47 | mt3i 141 |
. . . . 5
OrdIso |
49 | | ssid 3624 |
. . . . 5
OrdIso OrdIso |
50 | | ssnnfi 8179 |
. . . . 5
OrdIso OrdIso
OrdIso
OrdIso |
51 | 48, 49, 50 | sylancl 694 |
. . . 4
OrdIso |
52 | | simpl 473 |
. . . . . 6
|
53 | 23 | oien 8443 |
. . . . . 6
OrdIso |
54 | 27, 52, 53 | sylancr 695 |
. . . . 5
OrdIso |
55 | | enfi 8176 |
. . . . 5
OrdIso OrdIso
|
56 | 54, 55 | syl 17 |
. . . 4
OrdIso
|
57 | 51, 56 | mpbid 222 |
. . 3
|
58 | 7, 57 | jca 554 |
. 2
|
59 | 5, 58 | impbii 199 |
1
|