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 ‘ ( 𝐹 ∪ 𝐺 ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐺 ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) ) |