Description: No filter base containing a finite element is free. (Contributed by Jeff Hankins, 5-Dec-2009) (Revised by Stefan O'Rear, 28-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fbfinnfr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 | |
|
2 | 1 | anbi2d | |
3 | 2 | imbi1d | |
4 | eleq1 | |
|
5 | 4 | anbi2d | |
6 | 5 | imbi1d | |
7 | bi2.04 | |
|
8 | ibar | |
|
9 | 8 | adantr | |
10 | 9 | imbi1d | |
11 | 7 10 | bitr4id | |
12 | 11 | albidv | |
13 | df-ral | |
|
14 | 12 13 | bitr4di | |
15 | 0nelfb | |
|
16 | eleq1 | |
|
17 | 16 | notbid | |
18 | 15 17 | syl5ibrcom | |
19 | 18 | necon2ad | |
20 | 19 | imp | |
21 | ssn0 | |
|
22 | 21 | ex | |
23 | 20 22 | syl5com | |
24 | 23 | a1dd | |
25 | ssint | |
|
26 | 25 | notbii | |
27 | rexnal | |
|
28 | 26 27 | bitr4i | |
29 | fbasssin | |
|
30 | nssinpss | |
|
31 | sspsstr | |
|
32 | 30 31 | sylan2b | |
33 | 32 | expcom | |
34 | 33 | reximdv | |
35 | 29 34 | syl5com | |
36 | 35 | 3expia | |
37 | 36 | rexlimdv | |
38 | 28 37 | biimtrid | |
39 | r19.29 | |
|
40 | id | |
|
41 | 40 | imp | |
42 | 41 | rexlimivw | |
43 | 39 42 | syl | |
44 | 43 | expcom | |
45 | 38 44 | syl6 | |
46 | 24 45 | pm2.61d | |
47 | 14 46 | sylbid | |
48 | 47 | com12 | |
49 | 48 | a1i | |
50 | 3 6 49 | findcard3 | |
51 | 50 | com12 | |
52 | 51 | 3impia | |