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

Metamath Proof Explorer

Theorem supfil

Description: The supersets of a nonempty set which are also subsets of a given base set form a filter. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Stefan O'Rear, 7-Aug-2015)

Ref Expression
Assertion supfil ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∈ 𝒫 𝐴 ∣ 𝐵 ⊆ 𝑥 } ∈ ( Fil ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sseq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦 ) )
2 1 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝐵 ⊆ 𝑥 } ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝐵 ⊆ 𝑦 ) )
3 velpw ⊢ ( 𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴 )
4 3 anbi1i ⊢ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝐵 ⊆ 𝑦 ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝑦 ) )
5 2 4 bitri ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝐵 ⊆ 𝑥 } ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝑦 ) )
6 5 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ 𝐵 ⊆ 𝑥 } ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝑦 ) ) )
7 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → 𝐴 ∈ 𝑉 )
8 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → 𝐵 ⊆ 𝐴 )
9 sseq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝐴 ) )
10 9 sbcieg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑦 ] 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝐴 ) )
11 7 10 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ( [ 𝐴 / 𝑦 ] 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝐴 ) )
12 8 11 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → [ 𝐴 / 𝑦 ] 𝐵 ⊆ 𝑦 )
13 ss0 ⊢ ( 𝐵 ⊆ ∅ → 𝐵 = ∅ )
14 13 necon3ai ⊢ ( 𝐵 ≠ ∅ → ¬ 𝐵 ⊆ ∅ )
15 14 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ¬ 𝐵 ⊆ ∅ )
16 0ex ⊢ ∅ ∈ V
17 sseq2 ⊢ ( 𝑦 = ∅ → ( 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ ∅ ) )
18 16 17 sbcie ⊢ ( [ ∅ / 𝑦 ] 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ ∅ )
19 15 18 sylnibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ¬ [ ∅ / 𝑦 ] 𝐵 ⊆ 𝑦 )
20 sstr ⊢ ( ( 𝐵 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) → 𝐵 ⊆ 𝑧 )
21 20 expcom ⊢ ( 𝑤 ⊆ 𝑧 → ( 𝐵 ⊆ 𝑤 → 𝐵 ⊆ 𝑧 ) )
22 vex ⊢ 𝑤 ∈ V
23 sseq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝑤 ) )
24 22 23 sbcie ⊢ ( [ 𝑤 / 𝑦 ] 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝑤 )
25 vex ⊢ 𝑧 ∈ V
26 sseq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝑧 ) )
27 25 26 sbcie ⊢ ( [ 𝑧 / 𝑦 ] 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝑧 )
28 21 24 27 3imtr4g ⊢ ( 𝑤 ⊆ 𝑧 → ( [ 𝑤 / 𝑦 ] 𝐵 ⊆ 𝑦 → [ 𝑧 / 𝑦 ] 𝐵 ⊆ 𝑦 ) )
29 28 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑧 ⊆ 𝐴 ∧ 𝑤 ⊆ 𝑧 ) → ( [ 𝑤 / 𝑦 ] 𝐵 ⊆ 𝑦 → [ 𝑧 / 𝑦 ] 𝐵 ⊆ 𝑦 ) )
30 ssin ⊢ ( ( 𝐵 ⊆ 𝑧 ∧ 𝐵 ⊆ 𝑤 ) ↔ 𝐵 ⊆ ( 𝑧 ∩ 𝑤 ) )
31 30 biimpi ⊢ ( ( 𝐵 ⊆ 𝑧 ∧ 𝐵 ⊆ 𝑤 ) → 𝐵 ⊆ ( 𝑧 ∩ 𝑤 ) )
32 27 24 31 syl2anb ⊢ ( ( [ 𝑧 / 𝑦 ] 𝐵 ⊆ 𝑦 ∧ [ 𝑤 / 𝑦 ] 𝐵 ⊆ 𝑦 ) → 𝐵 ⊆ ( 𝑧 ∩ 𝑤 ) )
33 25 inex1 ⊢ ( 𝑧 ∩ 𝑤 ) ∈ V
34 sseq2 ⊢ ( 𝑦 = ( 𝑧 ∩ 𝑤 ) → ( 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ ( 𝑧 ∩ 𝑤 ) ) )
35 33 34 sbcie ⊢ ( [ ( 𝑧 ∩ 𝑤 ) / 𝑦 ] 𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ ( 𝑧 ∩ 𝑤 ) )
36 32 35 sylibr ⊢ ( ( [ 𝑧 / 𝑦 ] 𝐵 ⊆ 𝑦 ∧ [ 𝑤 / 𝑦 ] 𝐵 ⊆ 𝑦 ) → [ ( 𝑧 ∩ 𝑤 ) / 𝑦 ] 𝐵 ⊆ 𝑦 )
37 36 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑧 ⊆ 𝐴 ∧ 𝑤 ⊆ 𝐴 ) → ( ( [ 𝑧 / 𝑦 ] 𝐵 ⊆ 𝑦 ∧ [ 𝑤 / 𝑦 ] 𝐵 ⊆ 𝑦 ) → [ ( 𝑧 ∩ 𝑤 ) / 𝑦 ] 𝐵 ⊆ 𝑦 ) )
38 6 7 12 19 29 37 isfild ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∈ 𝒫 𝐴 ∣ 𝐵 ⊆ 𝑥 } ∈ ( Fil ‘ 𝐴 ) )