Metamath Proof Explorer

Theorem fgcl

Description: A generated filter is a filter. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fgcl ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 elfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑧 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑧 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ) ) )
2 elfvex ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ V )
3 fbasne0 ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ≠ ∅ )
4 n0 ⊢ ( 𝐹 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐹 )
5 3 4 sylib ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∃ 𝑦 𝑦 ∈ 𝐹 )
6 fbelss ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ⊆ 𝑋 )
7 6 ex ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑦 ∈ 𝐹 → 𝑦 ⊆ 𝑋 ) )
8 7 ancld ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑦 ∈ 𝐹 → ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ) ) )
9 8 eximdv ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ∃ 𝑦 𝑦 ∈ 𝐹 → ∃ 𝑦 ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ) ) )
10 5 9 mpd ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ) )
11 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ) )
12 10 11 sylibr ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋 )
13 elfvdm ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ dom fBas )
14 sseq2 ⊢ ( 𝑧 = 𝑋 → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑋 ) )
15 14 rexbidv ⊢ ( 𝑧 = 𝑋 → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋 ) )
16 15 sbcieg ⊢ ( 𝑋 ∈ dom fBas → ( [ 𝑋 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋 ) )
17 13 16 syl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( [ 𝑋 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋 ) )
18 12 17 mpbird ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → [ 𝑋 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 )
19 0nelfb ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )
20 0ex ⊢ ∅ ∈ V
21 sseq2 ⊢ ( 𝑧 = ∅ → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ ∅ ) )
22 21 rexbidv ⊢ ( 𝑧 = ∅ → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ∅ ) )
23 20 22 sbcie ⊢ ( [ ∅ / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ∅ )
24 ss0 ⊢ ( 𝑦 ⊆ ∅ → 𝑦 = ∅ )
25 24 eleq1d ⊢ ( 𝑦 ⊆ ∅ → ( 𝑦 ∈ 𝐹 ↔ ∅ ∈ 𝐹 ) )
26 25 biimpac ⊢ ( ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ ∅ ) → ∅ ∈ 𝐹 )
27 26 rexlimiva ⊢ ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ∅ → ∅ ∈ 𝐹 )
28 23 27 sylbi ⊢ ( [ ∅ / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → ∅ ∈ 𝐹 )
29 19 28 nsyl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ¬ [ ∅ / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 )
30 sstr ⊢ ( ( 𝑦 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑢 ) → 𝑦 ⊆ 𝑢 )
31 30 expcom ⊢ ( 𝑣 ⊆ 𝑢 → ( 𝑦 ⊆ 𝑣 → 𝑦 ⊆ 𝑢 ) )
32 31 reximdv ⊢ ( 𝑣 ⊆ 𝑢 → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 ) )
33 32 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢 ) → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 ) )
34 vex ⊢ 𝑣 ∈ V
35 sseq2 ⊢ ( 𝑧 = 𝑣 → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑣 ) )
36 35 rexbidv ⊢ ( 𝑧 = 𝑣 → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 ) )
37 34 36 sbcie ⊢ ( [ 𝑣 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 )
38 vex ⊢ 𝑢 ∈ V
39 sseq2 ⊢ ( 𝑧 = 𝑢 → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑢 ) )
40 39 rexbidv ⊢ ( 𝑧 = 𝑢 → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 ) )
41 38 40 sbcie ⊢ ( [ 𝑢 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 )
42 33 37 41 3imtr4g ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢 ) → ( [ 𝑣 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → [ 𝑢 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ) )
43 fbasssin ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑧 ∩ 𝑤 ) )
44 43 3expib ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑧 ∩ 𝑤 ) ) )
45 sstr2 ⊢ ( 𝑦 ⊆ ( 𝑧 ∩ 𝑤 ) → ( ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) → 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
46 45 com12 ⊢ ( ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( 𝑦 ⊆ ( 𝑧 ∩ 𝑤 ) → 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
47 46 reximdv ⊢ ( ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑧 ∩ 𝑤 ) → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
48 ss2in ⊢ ( ( 𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣 ) → ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) )
49 47 48 syl11 ⊢ ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑧 ∩ 𝑤 ) → ( ( 𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣 ) → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
50 44 49 syl6 ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) → ( ( 𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣 ) → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
51 50 exp5c ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑧 ∈ 𝐹 → ( 𝑤 ∈ 𝐹 → ( 𝑧 ⊆ 𝑢 → ( 𝑤 ⊆ 𝑣 → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) ) ) )
52 51 imp31 ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐹 ) ∧ 𝑤 ∈ 𝐹 ) → ( 𝑧 ⊆ 𝑢 → ( 𝑤 ⊆ 𝑣 → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
53 52 impancom ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐹 ) ∧ 𝑧 ⊆ 𝑢 ) → ( 𝑤 ∈ 𝐹 → ( 𝑤 ⊆ 𝑣 → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
54 53 rexlimdv ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐹 ) ∧ 𝑧 ⊆ 𝑢 ) → ( ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
55 54 rexlimdva2 ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 → ( ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
56 55 impd ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 ) → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
57 56 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋 ) → ( ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 ) → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
58 sseq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑢 ) )
59 58 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 ↔ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 )
60 41 59 bitri ⊢ ( [ 𝑢 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 )
61 sseq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑣 ) )
62 61 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 ↔ ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 )
63 37 62 bitri ⊢ ( [ 𝑣 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 )
64 60 63 anbi12i ⊢ ( ( [ 𝑢 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [ 𝑣 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ) ↔ ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃ 𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 ) )
65 38 inex1 ⊢ ( 𝑢 ∩ 𝑣 ) ∈ V
66 sseq2 ⊢ ( 𝑧 = ( 𝑢 ∩ 𝑣 ) → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
67 66 rexbidv ⊢ ( 𝑧 = ( 𝑢 ∩ 𝑣 ) → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
68 65 67 sbcie ⊢ ( [ ( 𝑢 ∩ 𝑣 ) / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ ( 𝑢 ∩ 𝑣 ) )
69 57 64 68 3imtr4g ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋 ) → ( ( [ 𝑢 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [ 𝑣 / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ) → [ ( 𝑢 ∩ 𝑣 ) / 𝑧 ] ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ) )
70 1 2 18 29 42 69 isfild ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )