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 ‘ 𝐴 ) )