Step | Hyp | Ref
| Expression |
1 | | nosupbnd1.1 |
. . . . . . . 8
|
2 | 1 | nosupno 31849 |
. . . . . . 7
|
3 | 2 | 3ad2ant2 1083 |
. . . . . 6
|
4 | 3 | adantl 482 |
. . . . 5
|
5 | | nodmord 31806 |
. . . . 5
|
6 | | ordirr 5741 |
. . . . 5
|
7 | 4, 5, 6 | 3syl 18 |
. . . 4
|
8 | | simpr3l 1122 |
. . . . . . 7
|
9 | 8 | adantr 481 |
. . . . . 6
|
10 | | ndmfv 6218 |
. . . . . . . . 9
|
11 | | 1on 7567 |
. . . . . . . . . . . . . 14
|
12 | 11 | elexi 3213 |
. . . . . . . . . . . . 13
|
13 | 12 | prid1 4297 |
. . . . . . . . . . . 12
|
14 | 13 | nosgnn0i 31812 |
. . . . . . . . . . 11
|
15 | | neeq1 2856 |
. . . . . . . . . . 11
|
16 | 14, 15 | mpbiri 248 |
. . . . . . . . . 10
|
17 | 16 | neneqd 2799 |
. . . . . . . . 9
|
18 | 10, 17 | syl 17 |
. . . . . . . 8
|
19 | 18 | con4i 113 |
. . . . . . 7
|
20 | 19 | adantl 482 |
. . . . . 6
|
21 | | simp2l 1087 |
. . . . . . . . . . . . . . . . 17
|
22 | | simp3l 1089 |
. . . . . . . . . . . . . . . . 17
|
23 | 21, 22 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
|
24 | 23 | adantr 481 |
. . . . . . . . . . . . . . 15
|
25 | 24 | adantr 481 |
. . . . . . . . . . . . . 14
|
26 | | nofun 31802 |
. . . . . . . . . . . . . 14
|
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . 13
|
28 | | simpl2l 1114 |
. . . . . . . . . . . . . . 15
|
29 | | simpll 790 |
. . . . . . . . . . . . . . 15
|
30 | | ssel2 3598 |
. . . . . . . . . . . . . . 15
|
31 | 28, 29, 30 | syl2an 494 |
. . . . . . . . . . . . . 14
|
32 | | nofun 31802 |
. . . . . . . . . . . . . 14
|
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . 13
|
34 | | simpl3r 1117 |
. . . . . . . . . . . . . . 15
|
35 | 34 | adantr 481 |
. . . . . . . . . . . . . 14
|
36 | | simpll1 1100 |
. . . . . . . . . . . . . . 15
|
37 | | simpll2 1101 |
. . . . . . . . . . . . . . 15
|
38 | | simpll3 1102 |
. . . . . . . . . . . . . . 15
|
39 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
40 | 1 | nosupbnd1lem2 31855 |
. . . . . . . . . . . . . . 15
|
41 | 36, 37, 38, 39, 40 | syl112anc 1330 |
. . . . . . . . . . . . . 14
|
42 | 35, 41 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
43 | 19 | adantl 482 |
. . . . . . . . . . . . . 14
|
44 | 43 | adantr 481 |
. . . . . . . . . . . . 13
|
45 | | ndmfv 6218 |
. . . . . . . . . . . . . . . . 17
|
46 | | neeq1 2856 |
. . . . . . . . . . . . . . . . . . 19
|
47 | 14, 46 | mpbiri 248 |
. . . . . . . . . . . . . . . . . 18
|
48 | 47 | neneqd 2799 |
. . . . . . . . . . . . . . . . 17
|
49 | 45, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
|
50 | 49 | con4i 113 |
. . . . . . . . . . . . . . 15
|
51 | 50 | adantl 482 |
. . . . . . . . . . . . . 14
|
52 | 51 | adantl 482 |
. . . . . . . . . . . . 13
|
53 | | simplr 792 |
. . . . . . . . . . . . . 14
|
54 | | simprr 796 |
. . . . . . . . . . . . . 14
|
55 | 53, 54 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
56 | | eqfunressuc 31660 |
. . . . . . . . . . . . 13
|
57 | 27, 33, 42, 44, 52, 55, 56 | syl213anc 1345 |
. . . . . . . . . . . 12
|
58 | 57 | expr 643 |
. . . . . . . . . . 11
|
59 | 58 | expr 643 |
. . . . . . . . . 10
|
60 | 59 | a2d 29 |
. . . . . . . . 9
|
61 | 60 | ralimdva 2962 |
. . . . . . . 8
|
62 | 61 | impcom 446 |
. . . . . . 7
|
63 | 62 | anassrs 680 |
. . . . . 6
|
64 | | dmeq 5324 |
. . . . . . . . 9
|
65 | 64 | eleq2d 2687 |
. . . . . . . 8
|
66 | | breq2 4657 |
. . . . . . . . . . 11
|
67 | 66 | notbid 308 |
. . . . . . . . . 10
|
68 | | reseq1 5390 |
. . . . . . . . . . 11
|
69 | 68 | eqeq1d 2624 |
. . . . . . . . . 10
|
70 | 67, 69 | imbi12d 334 |
. . . . . . . . 9
|
71 | 70 | ralbidv 2986 |
. . . . . . . 8
|
72 | 65, 71 | anbi12d 747 |
. . . . . . 7
|
73 | 72 | rspcev 3309 |
. . . . . 6
|
74 | 9, 20, 63, 73 | syl12anc 1324 |
. . . . 5
|
75 | | simplr1 1103 |
. . . . . . 7
|
76 | 1 | nosupdm 31850 |
. . . . . . . 8
|
77 | 76 | eleq2d 2687 |
. . . . . . 7
|
78 | 75, 77 | syl 17 |
. . . . . 6
|
79 | 4 | adantr 481 |
. . . . . . 7
|
80 | | nodmon 31803 |
. . . . . . 7
|
81 | | eleq1 2689 |
. . . . . . . . . 10
|
82 | | suceq 5790 |
. . . . . . . . . . . . . 14
|
83 | 82 | reseq2d 5396 |
. . . . . . . . . . . . 13
|
84 | 82 | reseq2d 5396 |
. . . . . . . . . . . . 13
|
85 | 83, 84 | eqeq12d 2637 |
. . . . . . . . . . . 12
|
86 | 85 | imbi2d 330 |
. . . . . . . . . . 11
|
87 | 86 | ralbidv 2986 |
. . . . . . . . . 10
|
88 | 81, 87 | anbi12d 747 |
. . . . . . . . 9
|
89 | 88 | rexbidv 3052 |
. . . . . . . 8
|
90 | 89 | elabg 3351 |
. . . . . . 7
|
91 | 79, 80, 90 | 3syl 18 |
. . . . . 6
|
92 | 78, 91 | bitrd 268 |
. . . . 5
|
93 | 74, 92 | mpbird 247 |
. . . 4
|
94 | 7, 93 | mtand 691 |
. . 3
|
95 | 94 | neqned 2801 |
. 2
|
96 | | rexanali 2998 |
. . 3
|
97 | | simpl 473 |
. . . . . . . . . . 11
|
98 | 21, 97, 30 | syl2an 494 |
. . . . . . . . . 10
|
99 | | nofv 31810 |
. . . . . . . . . 10
|
100 | 98, 99 | syl 17 |
. . . . . . . . 9
|
101 | | 3orel2 31592 |
. . . . . . . . 9
|
102 | 100, 101 | syl5com 31 |
. . . . . . . 8
|
103 | 102 | imdistanda 729 |
. . . . . . 7
|
104 | | simpl1 1064 |
. . . . . . . . . . . 12
|
105 | | simpl2 1065 |
. . . . . . . . . . . 12
|
106 | | simprl 794 |
. . . . . . . . . . . 12
|
107 | | simpl3 1066 |
. . . . . . . . . . . . 13
|
108 | | simpr 477 |
. . . . . . . . . . . . 13
|
109 | 104, 105,
107, 108, 40 | syl112anc 1330 |
. . . . . . . . . . . 12
|
110 | 1 | nosupbnd1lem4 31857 |
. . . . . . . . . . . 12
|
111 | 104, 105,
106, 109, 110 | syl112anc 1330 |
. . . . . . . . . . 11
|
112 | 111 | neneqd 2799 |
. . . . . . . . . 10
|
113 | 112 | pm2.21d 118 |
. . . . . . . . 9
|
114 | 1 | nosupbnd1lem3 31856 |
. . . . . . . . . . . 12
|
115 | 104, 105,
106, 109, 114 | syl112anc 1330 |
. . . . . . . . . . 11
|
116 | 115 | neneqd 2799 |
. . . . . . . . . 10
|
117 | 116 | pm2.21d 118 |
. . . . . . . . 9
|
118 | 113, 117 | jaod 395 |
. . . . . . . 8
|
119 | 118 | expimpd 629 |
. . . . . . 7
|
120 | 103, 119 | syldc 48 |
. . . . . 6
|
121 | 120 | anasss 679 |
. . . . 5
|
122 | 121 | rexlimiva 3028 |
. . . 4
|
123 | 122 | imp 445 |
. . 3
|
124 | 96, 123 | sylanbr 490 |
. 2
|
125 | 95, 124 | pm2.61ian 831 |
1
|