Metamath Proof Explorer


Theorem fbfinnfr

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 FfBasBSFSFinF

Proof

Step Hyp Ref Expression
1 eleq1 x=yxFyF
2 1 anbi2d x=yFfBasBxFFfBasByF
3 2 imbi1d x=yFfBasBxFFFfBasByFF
4 eleq1 x=SxFSF
5 4 anbi2d x=SFfBasBxFFfBasBSF
6 5 imbi1d x=SFfBasBxFFFfBasBSFF
7 bi2.04 xyFfBasBxFFFfBasBxFxyF
8 ibar FfBasBxFFfBasBxF
9 8 adantr FfBasByFxFFfBasBxF
10 9 imbi1d FfBasByFxFxyFFfBasBxFxyF
11 7 10 bitr4id FfBasByFxyFfBasBxFFxFxyF
12 11 albidv FfBasByFxxyFfBasBxFFxxFxyF
13 df-ral xFxyFxxFxyF
14 12 13 bitr4di FfBasByFxxyFfBasBxFFxFxyF
15 0nelfb FfBasB¬F
16 eleq1 y=yFF
17 16 notbid y=¬yF¬F
18 15 17 syl5ibrcom FfBasBy=¬yF
19 18 necon2ad FfBasByFy
20 19 imp FfBasByFy
21 ssn0 yFyF
22 21 ex yFyF
23 20 22 syl5com FfBasByFyFF
24 23 a1dd FfBasByFyFxFxyFF
25 ssint yFzFyz
26 25 notbii ¬yF¬zFyz
27 rexnal zF¬yz¬zFyz
28 26 27 bitr4i ¬yFzF¬yz
29 fbasssin FfBasByFzFxFxyz
30 nssinpss ¬yzyzy
31 sspsstr xyzyzyxy
32 30 31 sylan2b xyz¬yzxy
33 32 expcom ¬yzxyzxy
34 33 reximdv ¬yzxFxyzxFxy
35 29 34 syl5com FfBasByFzF¬yzxFxy
36 35 3expia FfBasByFzF¬yzxFxy
37 36 rexlimdv FfBasByFzF¬yzxFxy
38 28 37 biimtrid FfBasByF¬yFxFxy
39 r19.29 xFxyFxFxyxFxyFxy
40 id xyFxyF
41 40 imp xyFxyF
42 41 rexlimivw xFxyFxyF
43 39 42 syl xFxyFxFxyF
44 43 expcom xFxyxFxyFF
45 38 44 syl6 FfBasByF¬yFxFxyFF
46 24 45 pm2.61d FfBasByFxFxyFF
47 14 46 sylbid FfBasByFxxyFfBasBxFFF
48 47 com12 xxyFfBasBxFFFfBasByFF
49 48 a1i yFinxxyFfBasBxFFFfBasByFF
50 3 6 49 findcard3 SFinFfBasBSFF
51 50 com12 FfBasBSFSFinF
52 51 3impia FfBasBSFSFinF