Metamath Proof Explorer

Theorem fbunfip

Description: A helpful lemma for showing that certain sets generate filters. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fbunfip ⊢F∈fBas⁡X∧G∈fBas⁡Y→¬∅∈fi⁡F∪G↔∀x∈F∀y∈Gx∩y≠∅

Proof

Step Hyp Ref Expression
1 elfiun ⊢F∈fBas⁡X∧G∈fBas⁡Y→∅∈fi⁡F∪G↔∅∈fi⁡F∨∅∈fi⁡G∨∃x∈fi⁡F∃y∈fi⁡G∅=x∩y
2 1 notbid ⊢F∈fBas⁡X∧G∈fBas⁡Y→¬∅∈fi⁡F∪G↔¬∅∈fi⁡F∨∅∈fi⁡G∨∃x∈fi⁡F∃y∈fi⁡G∅=x∩y
3 3ioran ⊢¬∅∈fi⁡F∨∅∈fi⁡G∨∃x∈fi⁡F∃y∈fi⁡G∅=x∩y↔¬∅∈fi⁡F∧¬∅∈fi⁡G∧¬∃x∈fi⁡F∃y∈fi⁡G∅=x∩y
4 df-3an ⊢¬∅∈fi⁡F∧¬∅∈fi⁡G∧¬∃x∈fi⁡F∃y∈fi⁡G∅=x∩y↔¬∅∈fi⁡F∧¬∅∈fi⁡G∧¬∃x∈fi⁡F∃y∈fi⁡G∅=x∩y
5 3 4 bitr2i ⊢¬∅∈fi⁡F∧¬∅∈fi⁡G∧¬∃x∈fi⁡F∃y∈fi⁡G∅=x∩y↔¬∅∈fi⁡F∨∅∈fi⁡G∨∃x∈fi⁡F∃y∈fi⁡G∅=x∩y
6 2 5 bitr4di ⊢F∈fBas⁡X∧G∈fBas⁡Y→¬∅∈fi⁡F∪G↔¬∅∈fi⁡F∧¬∅∈fi⁡G∧¬∃x∈fi⁡F∃y∈fi⁡G∅=x∩y
7 nesym ⊢x∩y≠∅↔¬∅=x∩y
8 7 ralbii ⊢∀y∈fi⁡Gx∩y≠∅↔∀y∈fi⁡G¬∅=x∩y
9 ralnex ⊢∀y∈fi⁡G¬∅=x∩y↔¬∃y∈fi⁡G∅=x∩y
10 8 9 bitri ⊢∀y∈fi⁡Gx∩y≠∅↔¬∃y∈fi⁡G∅=x∩y
11 10 ralbii ⊢∀x∈fi⁡F∀y∈fi⁡Gx∩y≠∅↔∀x∈fi⁡F¬∃y∈fi⁡G∅=x∩y
12 ralnex ⊢∀x∈fi⁡F¬∃y∈fi⁡G∅=x∩y↔¬∃x∈fi⁡F∃y∈fi⁡G∅=x∩y
13 11 12 bitri ⊢∀x∈fi⁡F∀y∈fi⁡Gx∩y≠∅↔¬∃x∈fi⁡F∃y∈fi⁡G∅=x∩y
14 fbasfip ⊢F∈fBas⁡X→¬∅∈fi⁡F
15 fbasfip ⊢G∈fBas⁡Y→¬∅∈fi⁡G
16 14 15 anim12i ⊢F∈fBas⁡X∧G∈fBas⁡Y→¬∅∈fi⁡F∧¬∅∈fi⁡G
17 16 biantrurd ⊢F∈fBas⁡X∧G∈fBas⁡Y→¬∃x∈fi⁡F∃y∈fi⁡G∅=x∩y↔¬∅∈fi⁡F∧¬∅∈fi⁡G∧¬∃x∈fi⁡F∃y∈fi⁡G∅=x∩y
18 13 17 bitr2id ⊢F∈fBas⁡X∧G∈fBas⁡Y→¬∅∈fi⁡F∧¬∅∈fi⁡G∧¬∃x∈fi⁡F∃y∈fi⁡G∅=x∩y↔∀x∈fi⁡F∀y∈fi⁡Gx∩y≠∅
19 ssfii ⊢F∈fBas⁡X→F⊆fi⁡F
20 ssralv ⊢F⊆fi⁡F→∀x∈fi⁡F∀y∈fi⁡Gx∩y≠∅→∀x∈F∀y∈fi⁡Gx∩y≠∅
21 19 20 syl ⊢F∈fBas⁡X→∀x∈fi⁡F∀y∈fi⁡Gx∩y≠∅→∀x∈F∀y∈fi⁡Gx∩y≠∅
22 ssfii ⊢G∈fBas⁡Y→G⊆fi⁡G
23 ssralv ⊢G⊆fi⁡G→∀y∈fi⁡Gx∩y≠∅→∀y∈Gx∩y≠∅
24 22 23 syl ⊢G∈fBas⁡Y→∀y∈fi⁡Gx∩y≠∅→∀y∈Gx∩y≠∅
25 24 ralimdv ⊢G∈fBas⁡Y→∀x∈F∀y∈fi⁡Gx∩y≠∅→∀x∈F∀y∈Gx∩y≠∅
26 21 25 sylan9 ⊢F∈fBas⁡X∧G∈fBas⁡Y→∀x∈fi⁡F∀y∈fi⁡Gx∩y≠∅→∀x∈F∀y∈Gx∩y≠∅
27 ineq1 ⊢x=z→x∩y=z∩y
28 27 neeq1d ⊢x=z→x∩y≠∅↔z∩y≠∅
29 ineq2 ⊢y=w→z∩y=z∩w
30 29 neeq1d ⊢y=w→z∩y≠∅↔z∩w≠∅
31 28 30 cbvral2vw ⊢∀x∈F∀y∈Gx∩y≠∅↔∀z∈F∀w∈Gz∩w≠∅
32 fbssfi ⊢F∈fBas⁡X∧x∈fi⁡F→∃z∈Fz⊆x
33 fbssfi ⊢G∈fBas⁡Y∧y∈fi⁡G→∃w∈Gw⊆y
34 r19.29 ⊢∀z∈F∀w∈Gz∩w≠∅∧∃z∈Fz⊆x→∃z∈F∀w∈Gz∩w≠∅∧z⊆x
35 r19.29 ⊢∀w∈Gz∩w≠∅∧∃w∈Gw⊆y→∃w∈Gz∩w≠∅∧w⊆y
36 ss2in ⊢z⊆x∧w⊆y→z∩w⊆x∩y
37 sseq2 ⊢x∩y=∅→z∩w⊆x∩y↔z∩w⊆∅
38 ss0 ⊢z∩w⊆∅→z∩w=∅
39 37 38 syl6bi ⊢x∩y=∅→z∩w⊆x∩y→z∩w=∅
40 36 39 syl5com ⊢z⊆x∧w⊆y→x∩y=∅→z∩w=∅
41 40 necon3d ⊢z⊆x∧w⊆y→z∩w≠∅→x∩y≠∅
42 41 ex ⊢z⊆x→w⊆y→z∩w≠∅→x∩y≠∅
43 42 com13 ⊢z∩w≠∅→w⊆y→z⊆x→x∩y≠∅
44 43 imp ⊢z∩w≠∅∧w⊆y→z⊆x→x∩y≠∅
45 44 rexlimivw ⊢∃w∈Gz∩w≠∅∧w⊆y→z⊆x→x∩y≠∅
46 35 45 syl ⊢∀w∈Gz∩w≠∅∧∃w∈Gw⊆y→z⊆x→x∩y≠∅
47 46 impancom ⊢∀w∈Gz∩w≠∅∧z⊆x→∃w∈Gw⊆y→x∩y≠∅
48 47 rexlimivw ⊢∃z∈F∀w∈Gz∩w≠∅∧z⊆x→∃w∈Gw⊆y→x∩y≠∅
49 34 48 syl ⊢∀z∈F∀w∈Gz∩w≠∅∧∃z∈Fz⊆x→∃w∈Gw⊆y→x∩y≠∅
50 49 expimpd ⊢∀z∈F∀w∈Gz∩w≠∅→∃z∈Fz⊆x∧∃w∈Gw⊆y→x∩y≠∅
51 50 com12 ⊢∃z∈Fz⊆x∧∃w∈Gw⊆y→∀z∈F∀w∈Gz∩w≠∅→x∩y≠∅
52 32 33 51 syl2an ⊢F∈fBas⁡X∧x∈fi⁡F∧G∈fBas⁡Y∧y∈fi⁡G→∀z∈F∀w∈Gz∩w≠∅→x∩y≠∅
53 52 an4s ⊢F∈fBas⁡X∧G∈fBas⁡Y∧x∈fi⁡F∧y∈fi⁡G→∀z∈F∀w∈Gz∩w≠∅→x∩y≠∅
54 53 ralrimdvva ⊢F∈fBas⁡X∧G∈fBas⁡Y→∀z∈F∀w∈Gz∩w≠∅→∀x∈fi⁡F∀y∈fi⁡Gx∩y≠∅
55 31 54 biimtrid ⊢F∈fBas⁡X∧G∈fBas⁡Y→∀x∈F∀y∈Gx∩y≠∅→∀x∈fi⁡F∀y∈fi⁡Gx∩y≠∅
56 26 55 impbid ⊢F∈fBas⁡X∧G∈fBas⁡Y→∀x∈fi⁡F∀y∈fi⁡Gx∩y≠∅↔∀x∈F∀y∈Gx∩y≠∅
57 6 18 56 3bitrd ⊢F∈fBas⁡X∧G∈fBas⁡Y→¬∅∈fi⁡F∪G↔∀x∈F∀y∈Gx∩y≠∅