Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . 5
|
2 | 1 | neeq1d 2853 |
. . . 4
|
3 | 2 | imbi2d 330 |
. . 3
|
4 | | fveq2 6191 |
. . . . 5
|
5 | 4 | neeq1d 2853 |
. . . 4
|
6 | 5 | imbi2d 330 |
. . 3
|
7 | | fveq2 6191 |
. . . . 5
|
8 | 7 | neeq1d 2853 |
. . . 4
|
9 | 8 | imbi2d 330 |
. . 3
|
10 | | fveq2 6191 |
. . . . 5
|
11 | 10 | neeq1d 2853 |
. . . 4
|
12 | 11 | imbi2d 330 |
. . 3
|
13 | | inf3lem.1 |
. . . . . . . 8
|
14 | | inf3lem.2 |
. . . . . . . 8
|
15 | | inf3lem.3 |
. . . . . . . 8
|
16 | | inf3lem.4 |
. . . . . . . 8
|
17 | 13, 14, 15, 16 | inf3lemb 8522 |
. . . . . . 7
|
18 | 17 | eqeq1i 2627 |
. . . . . 6
|
19 | | eqcom 2629 |
. . . . . 6
|
20 | 18, 19 | sylbb 209 |
. . . . 5
|
21 | 20 | necon3i 2826 |
. . . 4
|
22 | 21 | adantr 481 |
. . 3
|
23 | | vex 3203 |
. . . . . . . . 9
|
24 | 13, 14, 23, 16 | inf3lemd 8524 |
. . . . . . . 8
|
25 | | df-pss 3590 |
. . . . . . . . . 10
|
26 | | pssnel 4039 |
. . . . . . . . . 10
|
27 | 25, 26 | sylbir 225 |
. . . . . . . . 9
|
28 | | ssel 3597 |
. . . . . . . . . . . . . . 15
|
29 | | eluni 4439 |
. . . . . . . . . . . . . . 15
|
30 | 28, 29 | syl6ib 241 |
. . . . . . . . . . . . . 14
|
31 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 31 | biimparc 504 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | 13, 14, 23, 16 | inf3lemc 8523 |
. . . . . . . . . . . . . . . . . . . . . 22
|
34 | 33 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . 21
|
35 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . . 22
|
36 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
37 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
38 | 13, 14, 36, 37 | inf3lema 8521 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
39 | 38 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
40 | 39 | sseld 3602 |
. . . . . . . . . . . . . . . . . . . . . 22
|
41 | 35, 40 | syl5bir 233 |
. . . . . . . . . . . . . . . . . . . . 21
|
42 | 34, 41 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | 32, 42 | syl5 34 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 43 | com23 86 |
. . . . . . . . . . . . . . . . . 18
|
45 | 44 | exp5c 644 |
. . . . . . . . . . . . . . . . 17
|
46 | 45 | com34 91 |
. . . . . . . . . . . . . . . 16
|
47 | 46 | impd 447 |
. . . . . . . . . . . . . . 15
|
48 | 47 | exlimdv 1861 |
. . . . . . . . . . . . . 14
|
49 | 30, 48 | sylan9r 690 |
. . . . . . . . . . . . 13
|
50 | 49 | pm2.43d 53 |
. . . . . . . . . . . 12
|
51 | | id 22 |
. . . . . . . . . . . . 13
|
52 | 51 | necon3bd 2808 |
. . . . . . . . . . . 12
|
53 | 50, 52 | syl6 35 |
. . . . . . . . . . 11
|
54 | 53 | impd 447 |
. . . . . . . . . 10
|
55 | 54 | exlimdv 1861 |
. . . . . . . . 9
|
56 | 27, 55 | syl5 34 |
. . . . . . . 8
|
57 | 24, 56 | sylani 686 |
. . . . . . 7
|
58 | 57 | exp4b 632 |
. . . . . 6
|
59 | 58 | pm2.43a 54 |
. . . . 5
|
60 | 59 | adantld 483 |
. . . 4
|
61 | 60 | a2d 29 |
. . 3
|
62 | 3, 6, 9, 12, 22, 61 | finds 7092 |
. 2
|
63 | 62 | com12 32 |
1
|