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 ∈ G x ∩ 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 syl6bbr ⊢ 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 ⁡ G x ∩ y ≠ ∅ ↔ ∀ y ∈ fi ⁡ G ¬ ∅ = x ∩ y
9 ralnex ⊢ ∀ y ∈ fi ⁡ G ¬ ∅ = x ∩ y ↔ ¬ ∃ y ∈ fi ⁡ G ∅ = x ∩ y
10 8 9 bitri ⊢ ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅ ↔ ¬ ∃ y ∈ fi ⁡ G ∅ = x ∩ y
11 10 ralbii ⊢ ∀ x ∈ fi ⁡ F ∀ y ∈ fi ⁡ G x ∩ 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 ⁡ G x ∩ 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 syl5rbb ⊢ F ∈ fBas ⁡ X ∧ G ∈ fBas ⁡ Y → ¬ ∅ ∈ fi ⁡ F ∧ ¬ ∅ ∈ fi ⁡ G ∧ ¬ ∃ x ∈ fi ⁡ F ∃ y ∈ fi ⁡ G ∅ = x ∩ y ↔ ∀ x ∈ fi ⁡ F ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅
19 ssfii ⊢ F ∈ fBas ⁡ X → F ⊆ fi ⁡ F
20 ssralv ⊢ F ⊆ fi ⁡ F → ∀ x ∈ fi ⁡ F ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅ → ∀ x ∈ F ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅
21 19 20 syl ⊢ F ∈ fBas ⁡ X → ∀ x ∈ fi ⁡ F ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅ → ∀ x ∈ F ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅
22 ssfii ⊢ G ∈ fBas ⁡ Y → G ⊆ fi ⁡ G
23 ssralv ⊢ G ⊆ fi ⁡ G → ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅ → ∀ y ∈ G x ∩ y ≠ ∅
24 22 23 syl ⊢ G ∈ fBas ⁡ Y → ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅ → ∀ y ∈ G x ∩ y ≠ ∅
25 24 ralimdv ⊢ G ∈ fBas ⁡ Y → ∀ x ∈ F ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅ → ∀ x ∈ F ∀ y ∈ G x ∩ y ≠ ∅
26 21 25 sylan9 ⊢ F ∈ fBas ⁡ X ∧ G ∈ fBas ⁡ Y → ∀ x ∈ fi ⁡ F ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅ → ∀ x ∈ F ∀ y ∈ G x ∩ 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 ∈ G x ∩ y ≠ ∅ ↔ ∀ z ∈ F ∀ w ∈ G z ∩ w ≠ ∅
32 fbssfi ⊢ F ∈ fBas ⁡ X ∧ x ∈ fi ⁡ F → ∃ z ∈ F z ⊆ x
33 fbssfi ⊢ G ∈ fBas ⁡ Y ∧ y ∈ fi ⁡ G → ∃ w ∈ G w ⊆ y
34 r19.29 ⊢ ∀ z ∈ F ∀ w ∈ G z ∩ w ≠ ∅ ∧ ∃ z ∈ F z ⊆ x → ∃ z ∈ F ∀ w ∈ G z ∩ w ≠ ∅ ∧ z ⊆ x
35 r19.29 ⊢ ∀ w ∈ G z ∩ w ≠ ∅ ∧ ∃ w ∈ G w ⊆ y → ∃ w ∈ G z ∩ 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 ∈ G z ∩ w ≠ ∅ ∧ w ⊆ y → z ⊆ x → x ∩ y ≠ ∅
46 35 45 syl ⊢ ∀ w ∈ G z ∩ w ≠ ∅ ∧ ∃ w ∈ G w ⊆ y → z ⊆ x → x ∩ y ≠ ∅
47 46 impancom ⊢ ∀ w ∈ G z ∩ w ≠ ∅ ∧ z ⊆ x → ∃ w ∈ G w ⊆ y → x ∩ y ≠ ∅
48 47 rexlimivw ⊢ ∃ z ∈ F ∀ w ∈ G z ∩ w ≠ ∅ ∧ z ⊆ x → ∃ w ∈ G w ⊆ y → x ∩ y ≠ ∅
49 34 48 syl ⊢ ∀ z ∈ F ∀ w ∈ G z ∩ w ≠ ∅ ∧ ∃ z ∈ F z ⊆ x → ∃ w ∈ G w ⊆ y → x ∩ y ≠ ∅
50 49 expimpd ⊢ ∀ z ∈ F ∀ w ∈ G z ∩ w ≠ ∅ → ∃ z ∈ F z ⊆ x ∧ ∃ w ∈ G w ⊆ y → x ∩ y ≠ ∅
51 50 com12 ⊢ ∃ z ∈ F z ⊆ x ∧ ∃ w ∈ G w ⊆ y → ∀ z ∈ F ∀ w ∈ G z ∩ w ≠ ∅ → x ∩ y ≠ ∅
52 32 33 51 syl2an ⊢ F ∈ fBas ⁡ X ∧ x ∈ fi ⁡ F ∧ G ∈ fBas ⁡ Y ∧ y ∈ fi ⁡ G → ∀ z ∈ F ∀ w ∈ G z ∩ w ≠ ∅ → x ∩ y ≠ ∅
53 52 an4s ⊢ F ∈ fBas ⁡ X ∧ G ∈ fBas ⁡ Y ∧ x ∈ fi ⁡ F ∧ y ∈ fi ⁡ G → ∀ z ∈ F ∀ w ∈ G z ∩ w ≠ ∅ → x ∩ y ≠ ∅
54 53 ralrimdvva ⊢ F ∈ fBas ⁡ X ∧ G ∈ fBas ⁡ Y → ∀ z ∈ F ∀ w ∈ G z ∩ w ≠ ∅ → ∀ x ∈ fi ⁡ F ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅
55 31 54 syl5bi ⊢ F ∈ fBas ⁡ X ∧ G ∈ fBas ⁡ Y → ∀ x ∈ F ∀ y ∈ G x ∩ y ≠ ∅ → ∀ x ∈ fi ⁡ F ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅
56 26 55 impbid ⊢ F ∈ fBas ⁡ X ∧ G ∈ fBas ⁡ Y → ∀ x ∈ fi ⁡ F ∀ y ∈ fi ⁡ G x ∩ y ≠ ∅ ↔ ∀ x ∈ F ∀ y ∈ G x ∩ y ≠ ∅
57 6 18 56 3bitrd ⊢ F ∈ fBas ⁡ X ∧ G ∈ fBas ⁡ Y → ¬ ∅ ∈ fi ⁡ F ∪ G ↔ ∀ x ∈ F ∀ y ∈ G x ∩ y ≠ ∅