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

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 ‘ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐺 ∃ 𝑧 ∈ ( 𝐹 ∪ 𝐺 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )