This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ∩ 𝑤 ) = ∅ ) )
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 biimtrid ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑌 ) ) → ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐺 ( 𝑥 ∩ 𝑦 ) ≠ ∅ → ∀ 𝑥 ∈ ( fi ‘ 𝐹 ) ∀ 𝑦 ∈ ( fi ‘ 𝐺 ) ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) )
56 26 55 impbid ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑌 ) ) → ( ∀ 𝑥 ∈ ( fi ‘ 𝐹 ) ∀ 𝑦 ∈ ( fi ‘ 𝐺 ) ( 𝑥 ∩ 𝑦 ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐺 ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) )
57 6 18 56 3bitrd ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑌 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ 𝐺 ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐺 ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) )