Metamath Proof Explorer

Theorem fbssfi

Description: A filter base contains subsets of its finite intersections. (Contributed by Mario Carneiro, 26-Nov-2013) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion fbssfi ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ ( fi ‘ 𝐹 ) ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 dffi2 ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ 𝐹 ) = ∩ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } )
2 sseq2 ⊢ ( 𝑡 = ( 𝑢 ∩ 𝑣 ) → ( 𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
3 2 rexbidv ⊢ ( 𝑡 = ( 𝑢 ∩ 𝑣 ) → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
4 inss1 ⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢
5 simp1r ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → 𝑢 ∈ 𝒫 ∪ 𝐹 )
6 5 elpwid ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → 𝑢 ⊆ ∪ 𝐹 )
7 4 6 sstrid ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ⊆ ∪ 𝐹 )
8 vex ⊢ 𝑢 ∈ V
9 8 inex1 ⊢ ( 𝑢 ∩ 𝑣 ) ∈ V
10 9 elpw ⊢ ( ( 𝑢 ∩ 𝑣 ) ∈ 𝒫 ∪ 𝐹 ↔ ( 𝑢 ∩ 𝑣 ) ⊆ ∪ 𝐹 )
11 7 10 sylibr ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝒫 ∪ 𝐹 )
12 simpl ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
13 simpl ⊢ ( ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) → 𝑦 ∈ 𝐹 )
14 simpl ⊢ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) → 𝑧 ∈ 𝐹 )
15 fbasssin ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) )
16 12 13 14 15 syl3an ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) )
17 ss2in ⊢ ( ( 𝑦 ⊆ 𝑢 ∧ 𝑧 ⊆ 𝑣 ) → ( 𝑦 ∩ 𝑧 ) ⊆ ( 𝑢 ∩ 𝑣 ) )
18 17 ad2ant2l ⊢ ( ( ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑦 ∩ 𝑧 ) ⊆ ( 𝑢 ∩ 𝑣 ) )
19 18 3adant1 ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑦 ∩ 𝑧 ) ⊆ ( 𝑢 ∩ 𝑣 ) )
20 sstr ⊢ ( ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ∧ ( 𝑦 ∩ 𝑧 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) → 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) )
21 20 expcom ⊢ ( ( 𝑦 ∩ 𝑧 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) → 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
22 19 21 syl ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) → 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
23 22 reximdv ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
24 16 23 mpd ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) )
25 3 11 24 elrabd ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } )
26 25 3expa ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } )
27 26 rexlimdvaa ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ) → ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 → ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
28 27 ralrimivw ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ) → ∀ 𝑣 ∈ 𝒫 ∪ 𝐹 ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 → ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
29 sseq2 ⊢ ( 𝑡 = 𝑣 → ( 𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ 𝑣 ) )
30 29 rexbidv ⊢ ( 𝑡 = 𝑣 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑣 ) )
31 sseq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ⊆ 𝑣 ↔ 𝑧 ⊆ 𝑣 ) )
32 31 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑣 ↔ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 )
33 30 32 bitrdi ⊢ ( 𝑡 = 𝑣 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 ) )
34 33 ralrab ⊢ ( ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ↔ ∀ 𝑣 ∈ 𝒫 ∪ 𝐹 ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 → ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
35 28 34 sylibr ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ) → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } )
36 35 rexlimdvaa ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
37 36 ralrimiva ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∀ 𝑢 ∈ 𝒫 ∪ 𝐹 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
38 sseq2 ⊢ ( 𝑡 = 𝑢 → ( 𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ 𝑢 ) )
39 38 rexbidv ⊢ ( 𝑡 = 𝑢 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑢 ) )
40 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝑢 ↔ 𝑦 ⊆ 𝑢 ) )
41 40 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑢 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 )
42 39 41 bitrdi ⊢ ( 𝑡 = 𝑢 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 ) )
43 42 ralrab ⊢ ( ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ↔ ∀ 𝑢 ∈ 𝒫 ∪ 𝐹 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
44 37 43 sylibr ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } )
45 pwuni ⊢ 𝐹 ⊆ 𝒫 ∪ 𝐹
46 ssid ⊢ 𝑡 ⊆ 𝑡
47 sseq1 ⊢ ( 𝑥 = 𝑡 → ( 𝑥 ⊆ 𝑡 ↔ 𝑡 ⊆ 𝑡 ) )
48 47 rspcev ⊢ ( ( 𝑡 ∈ 𝐹 ∧ 𝑡 ⊆ 𝑡 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 )
49 46 48 mpan2 ⊢ ( 𝑡 ∈ 𝐹 → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 )
50 49 rgen ⊢ ∀ 𝑡 ∈ 𝐹 ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡
51 ssrab ⊢ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ↔ ( 𝐹 ⊆ 𝒫 ∪ 𝐹 ∧ ∀ 𝑡 ∈ 𝐹 ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) )
52 45 50 51 mpbir2an ⊢ 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 }
53 44 52 jctil ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
54 uniexg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∪ 𝐹 ∈ V )
55 pwexg ⊢ ( ∪ 𝐹 ∈ V → 𝒫 ∪ 𝐹 ∈ V )
56 rabexg ⊢ ( 𝒫 ∪ 𝐹 ∈ V → { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ V )
57 sseq2 ⊢ ( 𝑧 = { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ( 𝐹 ⊆ 𝑧 ↔ 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
58 eleq2 ⊢ ( 𝑧 = { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ( ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ↔ ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
59 58 raleqbi1dv ⊢ ( 𝑧 = { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ( ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ↔ ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
60 59 raleqbi1dv ⊢ ( 𝑧 = { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ( ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ↔ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) )
61 57 60 anbi12d ⊢ ( 𝑧 = { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ( ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) ↔ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) )
62 61 elabg ⊢ ( { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ V → ( { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } ↔ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) )
63 54 55 56 62 4syl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } ↔ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) )
64 53 63 mpbird ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } )
65 intss1 ⊢ ( { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } → ∩ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } )
66 64 65 syl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∩ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } )
67 1 66 eqsstrd ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ 𝐹 ) ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } )
68 67 sselda ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ ( fi ‘ 𝐹 ) ) → 𝐴 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } )
69 sseq2 ⊢ ( 𝑡 = 𝐴 → ( 𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ 𝐴 ) )
70 69 rexbidv ⊢ ( 𝑡 = 𝐴 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) )
71 70 elrab ⊢ ( 𝐴 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ↔ ( 𝐴 ∈ 𝒫 ∪ 𝐹 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) )
72 71 simprbi ⊢ ( 𝐴 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 )
73 68 72 syl ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ ( fi ‘ 𝐹 ) ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 )