Metamath Proof Explorer


Theorem fbun

Description: A necessary and sufficient condition for the union of two filter bases to also be a filter base. (Contributed by Mario Carneiro, 28-Nov-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fbun ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝐹𝐺 ) ∈ ( fBas ‘ 𝑋 ) ↔ ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 elun1 ( 𝑥𝐹𝑥 ∈ ( 𝐹𝐺 ) )
2 elun2 ( 𝑦𝐺𝑦 ∈ ( 𝐹𝐺 ) )
3 1 2 anim12i ( ( 𝑥𝐹𝑦𝐺 ) → ( 𝑥 ∈ ( 𝐹𝐺 ) ∧ 𝑦 ∈ ( 𝐹𝐺 ) ) )
4 fbasssin ( ( ( 𝐹𝐺 ) ∈ ( fBas ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐹𝐺 ) ∧ 𝑦 ∈ ( 𝐹𝐺 ) ) → ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
5 4 3expb ( ( ( 𝐹𝐺 ) ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝐹𝐺 ) ∧ 𝑦 ∈ ( 𝐹𝐺 ) ) ) → ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
6 3 5 sylan2 ( ( ( 𝐹𝐺 ) ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝑥𝐹𝑦𝐺 ) ) → ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
7 6 ralrimivva ( ( 𝐹𝐺 ) ∈ ( fBas ‘ 𝑋 ) → ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
8 fbsspw ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
9 8 adantr ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → 𝐹 ⊆ 𝒫 𝑋 )
10 fbsspw ( 𝐺 ∈ ( fBas ‘ 𝑋 ) → 𝐺 ⊆ 𝒫 𝑋 )
11 10 adantl ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → 𝐺 ⊆ 𝒫 𝑋 )
12 9 11 unssd ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐹𝐺 ) ⊆ 𝒫 𝑋 )
13 12 a1d ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ( 𝐹𝐺 ) ⊆ 𝒫 𝑋 ) )
14 ssun1 𝐹 ⊆ ( 𝐹𝐺 )
15 fbasne0 ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ≠ ∅ )
16 ssn0 ( ( 𝐹 ⊆ ( 𝐹𝐺 ) ∧ 𝐹 ≠ ∅ ) → ( 𝐹𝐺 ) ≠ ∅ )
17 14 15 16 sylancr ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐹𝐺 ) ≠ ∅ )
18 17 adantr ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐹𝐺 ) ≠ ∅ )
19 18 a1d ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ( 𝐹𝐺 ) ≠ ∅ ) )
20 0nelfb ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )
21 0nelfb ( 𝐺 ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ 𝐺 )
22 df-nel ( ∅ ∉ ( 𝐹𝐺 ) ↔ ¬ ∅ ∈ ( 𝐹𝐺 ) )
23 elun ( ∅ ∈ ( 𝐹𝐺 ) ↔ ( ∅ ∈ 𝐹 ∨ ∅ ∈ 𝐺 ) )
24 23 notbii ( ¬ ∅ ∈ ( 𝐹𝐺 ) ↔ ¬ ( ∅ ∈ 𝐹 ∨ ∅ ∈ 𝐺 ) )
25 ioran ( ¬ ( ∅ ∈ 𝐹 ∨ ∅ ∈ 𝐺 ) ↔ ( ¬ ∅ ∈ 𝐹 ∧ ¬ ∅ ∈ 𝐺 ) )
26 22 24 25 3bitri ( ∅ ∉ ( 𝐹𝐺 ) ↔ ( ¬ ∅ ∈ 𝐹 ∧ ¬ ∅ ∈ 𝐺 ) )
27 26 biimpri ( ( ¬ ∅ ∈ 𝐹 ∧ ¬ ∅ ∈ 𝐺 ) → ∅ ∉ ( 𝐹𝐺 ) )
28 20 21 27 syl2an ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ∅ ∉ ( 𝐹𝐺 ) )
29 28 a1d ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ∅ ∉ ( 𝐹𝐺 ) ) )
30 fbasssin ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑥𝐹𝑦𝐹 ) → ∃ 𝑧𝐹 𝑧 ⊆ ( 𝑥𝑦 ) )
31 ssrexv ( 𝐹 ⊆ ( 𝐹𝐺 ) → ( ∃ 𝑧𝐹 𝑧 ⊆ ( 𝑥𝑦 ) → ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )
32 14 30 31 mpsyl ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑥𝐹𝑦𝐹 ) → ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
33 32 3expb ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝑥𝐹𝑦𝐹 ) ) → ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
34 33 ralrimivva ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∀ 𝑥𝐹𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
35 34 adantr ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ∀ 𝑥𝐹𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
36 pm3.2 ( ∀ 𝑥𝐹𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ( ∀ 𝑥𝐹𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) ) )
37 35 36 syl ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ( ∀ 𝑥𝐹𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) ) )
38 r19.26 ( ∀ 𝑥𝐹 ( ∀ 𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) ↔ ( ∀ 𝑥𝐹𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )
39 ralun ( ( ∀ 𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) → ∀ 𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
40 39 ralimi ( ∀ 𝑥𝐹 ( ∀ 𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) → ∀ 𝑥𝐹𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
41 38 40 sylbir ( ( ∀ 𝑥𝐹𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) → ∀ 𝑥𝐹𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
42 37 41 syl6 ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ∀ 𝑥𝐹𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )
43 ralcom ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ↔ ∀ 𝑦𝐺𝑥𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
44 ineq1 ( 𝑥 = 𝑤 → ( 𝑥𝑦 ) = ( 𝑤𝑦 ) )
45 44 sseq2d ( 𝑥 = 𝑤 → ( 𝑧 ⊆ ( 𝑥𝑦 ) ↔ 𝑧 ⊆ ( 𝑤𝑦 ) ) )
46 45 rexbidv ( 𝑥 = 𝑤 → ( ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ↔ ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑤𝑦 ) ) )
47 46 cbvralvw ( ∀ 𝑥𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ↔ ∀ 𝑤𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑤𝑦 ) )
48 47 ralbii ( ∀ 𝑦𝐺𝑥𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ↔ ∀ 𝑦𝐺𝑤𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑤𝑦 ) )
49 ineq2 ( 𝑦 = 𝑥 → ( 𝑤𝑦 ) = ( 𝑤𝑥 ) )
50 49 sseq2d ( 𝑦 = 𝑥 → ( 𝑧 ⊆ ( 𝑤𝑦 ) ↔ 𝑧 ⊆ ( 𝑤𝑥 ) ) )
51 50 rexbidv ( 𝑦 = 𝑥 → ( ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑤𝑦 ) ↔ ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑤𝑥 ) ) )
52 ineq1 ( 𝑤 = 𝑦 → ( 𝑤𝑥 ) = ( 𝑦𝑥 ) )
53 incom ( 𝑦𝑥 ) = ( 𝑥𝑦 )
54 52 53 eqtrdi ( 𝑤 = 𝑦 → ( 𝑤𝑥 ) = ( 𝑥𝑦 ) )
55 54 sseq2d ( 𝑤 = 𝑦 → ( 𝑧 ⊆ ( 𝑤𝑥 ) ↔ 𝑧 ⊆ ( 𝑥𝑦 ) ) )
56 55 rexbidv ( 𝑤 = 𝑦 → ( ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑤𝑥 ) ↔ ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )
57 51 56 cbvral2vw ( ∀ 𝑦𝐺𝑤𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑤𝑦 ) ↔ ∀ 𝑥𝐺𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
58 43 48 57 3bitri ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ↔ ∀ 𝑥𝐺𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
59 58 biimpi ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ∀ 𝑥𝐺𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
60 ssun2 𝐺 ⊆ ( 𝐹𝐺 )
61 fbasssin ( ( 𝐺 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑥𝐺𝑦𝐺 ) → ∃ 𝑧𝐺 𝑧 ⊆ ( 𝑥𝑦 ) )
62 ssrexv ( 𝐺 ⊆ ( 𝐹𝐺 ) → ( ∃ 𝑧𝐺 𝑧 ⊆ ( 𝑥𝑦 ) → ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )
63 60 61 62 mpsyl ( ( 𝐺 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑥𝐺𝑦𝐺 ) → ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
64 63 3expb ( ( 𝐺 ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝑥𝐺𝑦𝐺 ) ) → ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
65 64 ralrimivva ( 𝐺 ∈ ( fBas ‘ 𝑋 ) → ∀ 𝑥𝐺𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
66 65 adantl ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ∀ 𝑥𝐺𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
67 59 66 anim12i ( ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) ) → ( ∀ 𝑥𝐺𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑥𝐺𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )
68 67 expcom ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ( ∀ 𝑥𝐺𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑥𝐺𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) ) )
69 r19.26 ( ∀ 𝑥𝐺 ( ∀ 𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) ↔ ( ∀ 𝑥𝐺𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑥𝐺𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )
70 39 ralimi ( ∀ 𝑥𝐺 ( ∀ 𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) → ∀ 𝑥𝐺𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
71 69 70 sylbir ( ( ∀ 𝑥𝐺𝑦𝐹𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑥𝐺𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) → ∀ 𝑥𝐺𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
72 68 71 syl6 ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ∀ 𝑥𝐺𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )
73 42 72 jcad ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ( ∀ 𝑥𝐹𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑥𝐺𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) ) )
74 ralun ( ( ∀ 𝑥𝐹𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ∧ ∀ 𝑥𝐺𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) → ∀ 𝑥 ∈ ( 𝐹𝐺 ) ∀ 𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) )
75 73 74 syl6 ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ∀ 𝑥 ∈ ( 𝐹𝐺 ) ∀ 𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )
76 19 29 75 3jcad ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ( ( 𝐹𝐺 ) ≠ ∅ ∧ ∅ ∉ ( 𝐹𝐺 ) ∧ ∀ 𝑥 ∈ ( 𝐹𝐺 ) ∀ 𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) ) )
77 13 76 jcad ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ( ( 𝐹𝐺 ) ⊆ 𝒫 𝑋 ∧ ( ( 𝐹𝐺 ) ≠ ∅ ∧ ∅ ∉ ( 𝐹𝐺 ) ∧ ∀ 𝑥 ∈ ( 𝐹𝐺 ) ∀ 𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) ) ) )
78 elfvdm ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ dom fBas )
79 78 adantr ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → 𝑋 ∈ dom fBas )
80 isfbas2 ( 𝑋 ∈ dom fBas → ( ( 𝐹𝐺 ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹𝐺 ) ⊆ 𝒫 𝑋 ∧ ( ( 𝐹𝐺 ) ≠ ∅ ∧ ∅ ∉ ( 𝐹𝐺 ) ∧ ∀ 𝑥 ∈ ( 𝐹𝐺 ) ∀ 𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) ) ) )
81 79 80 syl ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝐹𝐺 ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹𝐺 ) ⊆ 𝒫 𝑋 ∧ ( ( 𝐹𝐺 ) ≠ ∅ ∧ ∅ ∉ ( 𝐹𝐺 ) ∧ ∀ 𝑥 ∈ ( 𝐹𝐺 ) ∀ 𝑦 ∈ ( 𝐹𝐺 ) ∃ 𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) ) ) )
82 77 81 sylibrd ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) → ( 𝐹𝐺 ) ∈ ( fBas ‘ 𝑋 ) ) )
83 7 82 impbid2 ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐺 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝐹𝐺 ) ∈ ( fBas ‘ 𝑋 ) ↔ ∀ 𝑥𝐹𝑦𝐺𝑧 ∈ ( 𝐹𝐺 ) 𝑧 ⊆ ( 𝑥𝑦 ) ) )