Theorem elfilss

Description: An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	elfilss	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝐹 ↔ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ibar	⊢ ( 𝐴 ⊆ 𝑋 → ( ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) ) )
2	1	adantl	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) ) )
3		filfbas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
4		elfg	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) ) )
5	3 4	syl	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) ) )
6	5	adantr	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) ) )
7		fgfil	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = 𝐹 )
8	7	eleq2d	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ 𝐴 ∈ 𝐹 ) )
9	8	adantr	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ 𝐴 ∈ 𝐹 ) )
10	2 6 9	3bitr2rd	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝐹 ↔ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) )