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 ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑌 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹𝐺 ) ) ↔ ∀ 𝑥𝐹𝑦𝐺 ( 𝑥𝑦 ) ≠ ∅ ) )

Proof

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