Step | Hyp | Ref
| Expression |
1 | | simp2l 1087 |
. . . 4
|
2 | | simp3 1063 |
. . . 4
|
3 | 1, 2 | sseldd 3604 |
. . 3
|
4 | | nosupbnd1.1 |
. . . . . 6
|
5 | 4 | nosupno 31849 |
. . . . 5
|
6 | 5 | 3ad2ant2 1083 |
. . . 4
|
7 | | nodmon 31803 |
. . . 4
|
8 | 6, 7 | syl 17 |
. . 3
|
9 | | noreson 31813 |
. . 3
|
10 | 3, 8, 9 | syl2anc 693 |
. 2
|
11 | | dmres 5419 |
. . . 4
|
12 | | inss1 3833 |
. . . 4
|
13 | 11, 12 | eqsstri 3635 |
. . 3
|
14 | 13 | a1i 11 |
. 2
|
15 | | ssid 3624 |
. . 3
|
16 | 15 | a1i 11 |
. 2
|
17 | | iffalse 4095 |
. . . . . . . . . . . 12
|
18 | 4, 17 | syl5eq 2668 |
. . . . . . . . . . 11
|
19 | 18 | dmeqd 5326 |
. . . . . . . . . 10
|
20 | | iotaex 5868 |
. . . . . . . . . . 11
|
21 | | eqid 2622 |
. . . . . . . . . . 11
|
22 | 20, 21 | dmmpti 6023 |
. . . . . . . . . 10
|
23 | 19, 22 | syl6eq 2672 |
. . . . . . . . 9
|
24 | 23 | eleq2d 2687 |
. . . . . . . 8
|
25 | | vex 3203 |
. . . . . . . . 9
|
26 | | eleq1 2689 |
. . . . . . . . . . . 12
|
27 | | suceq 5790 |
. . . . . . . . . . . . . . . 16
|
28 | 27 | reseq2d 5396 |
. . . . . . . . . . . . . . 15
|
29 | 27 | reseq2d 5396 |
. . . . . . . . . . . . . . 15
|
30 | 28, 29 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
|
31 | 30 | imbi2d 330 |
. . . . . . . . . . . . 13
|
32 | 31 | ralbidv 2986 |
. . . . . . . . . . . 12
|
33 | 26, 32 | anbi12d 747 |
. . . . . . . . . . 11
|
34 | 33 | rexbidv 3052 |
. . . . . . . . . 10
|
35 | | dmeq 5324 |
. . . . . . . . . . . . 13
|
36 | 35 | eleq2d 2687 |
. . . . . . . . . . . 12
|
37 | | breq2 4657 |
. . . . . . . . . . . . . . 15
|
38 | 37 | notbid 308 |
. . . . . . . . . . . . . 14
|
39 | | reseq1 5390 |
. . . . . . . . . . . . . . 15
|
40 | 39 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
41 | 38, 40 | imbi12d 334 |
. . . . . . . . . . . . 13
|
42 | 41 | ralbidv 2986 |
. . . . . . . . . . . 12
|
43 | 36, 42 | anbi12d 747 |
. . . . . . . . . . 11
|
44 | 43 | cbvrexv 3172 |
. . . . . . . . . 10
|
45 | 34, 44 | syl6bb 276 |
. . . . . . . . 9
|
46 | 25, 45 | elab 3350 |
. . . . . . . 8
|
47 | 24, 46 | syl6bb 276 |
. . . . . . 7
|
48 | 47 | 3ad2ant1 1082 |
. . . . . 6
|
49 | | simpl1 1064 |
. . . . . . . . 9
|
50 | | simpl2 1065 |
. . . . . . . . 9
|
51 | | simprl 794 |
. . . . . . . . 9
|
52 | | simprrl 804 |
. . . . . . . . 9
|
53 | | simprrr 805 |
. . . . . . . . 9
|
54 | 4 | nosupres 31853 |
. . . . . . . . 9
|
55 | 49, 50, 51, 52, 53, 54 | syl113anc 1338 |
. . . . . . . 8
|
56 | | simpl2l 1114 |
. . . . . . . . . . . . . . 15
|
57 | 56, 51 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
58 | 3 | adantr 481 |
. . . . . . . . . . . . . 14
|
59 | | sltso 31827 |
. . . . . . . . . . . . . . 15
|
60 | | soasym 31657 |
. . . . . . . . . . . . . . 15
|
61 | 59, 60 | mpan 706 |
. . . . . . . . . . . . . 14
|
62 | 57, 58, 61 | syl2anc 693 |
. . . . . . . . . . . . 13
|
63 | | simpl3 1066 |
. . . . . . . . . . . . . 14
|
64 | | breq1 4656 |
. . . . . . . . . . . . . . . . 17
|
65 | 64 | notbid 308 |
. . . . . . . . . . . . . . . 16
|
66 | | reseq1 5390 |
. . . . . . . . . . . . . . . . 17
|
67 | 66 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
68 | 65, 67 | imbi12d 334 |
. . . . . . . . . . . . . . 15
|
69 | 68 | rspcv 3305 |
. . . . . . . . . . . . . 14
|
70 | 63, 53, 69 | sylc 65 |
. . . . . . . . . . . . 13
|
71 | 62, 70 | syld 47 |
. . . . . . . . . . . 12
|
72 | 71 | imp 445 |
. . . . . . . . . . 11
|
73 | | nodmon 31803 |
. . . . . . . . . . . . . . . . 17
|
74 | 57, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
|
75 | | onelon 5748 |
. . . . . . . . . . . . . . . 16
|
76 | 74, 52, 75 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
77 | | sucelon 7017 |
. . . . . . . . . . . . . . 15
|
78 | 76, 77 | sylib 208 |
. . . . . . . . . . . . . 14
|
79 | | noreson 31813 |
. . . . . . . . . . . . . 14
|
80 | 58, 78, 79 | syl2anc 693 |
. . . . . . . . . . . . 13
|
81 | | sonr 5056 |
. . . . . . . . . . . . . 14
|
82 | 59, 81 | mpan 706 |
. . . . . . . . . . . . 13
|
83 | 80, 82 | syl 17 |
. . . . . . . . . . . 12
|
84 | 83 | adantr 481 |
. . . . . . . . . . 11
|
85 | 72, 84 | eqnbrtrd 4671 |
. . . . . . . . . 10
|
86 | 85 | ex 450 |
. . . . . . . . 9
|
87 | | sltres 31815 |
. . . . . . . . . . 11
|
88 | 57, 58, 78, 87 | syl3anc 1326 |
. . . . . . . . . 10
|
89 | 88 | con3d 148 |
. . . . . . . . 9
|
90 | 86, 89 | pm2.61d 170 |
. . . . . . . 8
|
91 | 55, 90 | eqnbrtrd 4671 |
. . . . . . 7
|
92 | 91 | rexlimdvaa 3032 |
. . . . . 6
|
93 | 48, 92 | sylbid 230 |
. . . . 5
|
94 | 93 | imp 445 |
. . . 4
|
95 | | nodmord 31806 |
. . . . . . . 8
|
96 | | ordsucss 7018 |
. . . . . . . 8
|
97 | 6, 95, 96 | 3syl 18 |
. . . . . . 7
|
98 | 97 | imp 445 |
. . . . . 6
|
99 | 98 | resabs1d 5428 |
. . . . 5
|
100 | 99 | breq2d 4665 |
. . . 4
|
101 | 94, 100 | mtbird 315 |
. . 3
|
102 | 101 | ralrimiva 2966 |
. 2
|
103 | | noresle 31846 |
. 2
|
104 | 10, 6, 14, 16, 102, 103 | syl23anc 1333 |
1
|