Theorem filunirn

Description: Two ways to express a filter on an unspecified base. (Contributed by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	filunirn	⊢ ( 𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( fBas ‘ 𝑦 ) ∈ V
2	1	rabex	⊢ { 𝑤 ∈ ( fBas ‘ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝒫 𝑦 ( ( 𝑤 ∩ 𝒫 𝑧 ) ≠ ∅ → 𝑧 ∈ 𝑤 ) } ∈ V
3		df-fil	⊢ Fil = ( 𝑦 ∈ V ↦ { 𝑤 ∈ ( fBas ‘ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝒫 𝑦 ( ( 𝑤 ∩ 𝒫 𝑧 ) ≠ ∅ → 𝑧 ∈ 𝑤 ) } )
4	2 3	fnmpti	⊢ Fil Fn V
5		fnunirn	⊢ ( Fil Fn V → ( 𝐹 ∈ ∪ ran Fil ↔ ∃ 𝑥 ∈ V 𝐹 ∈ ( Fil ‘ 𝑥 ) ) )
6	4 5	ax-mp	⊢ ( 𝐹 ∈ ∪ ran Fil ↔ ∃ 𝑥 ∈ V 𝐹 ∈ ( Fil ‘ 𝑥 ) )
7		filunibas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑥 ) → ∪ 𝐹 = 𝑥 )
8	7	fveq2d	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑥 ) → ( Fil ‘ ∪ 𝐹 ) = ( Fil ‘ 𝑥 ) )
9	8	eleq2d	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑥 ) → ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ↔ 𝐹 ∈ ( Fil ‘ 𝑥 ) ) )
10	9	ibir	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑥 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
11	10	rexlimivw	⊢ ( ∃ 𝑥 ∈ V 𝐹 ∈ ( Fil ‘ 𝑥 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
12	6 11	sylbi	⊢ ( 𝐹 ∈ ∪ ran Fil → 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
13		fvssunirn	⊢ ( Fil ‘ ∪ 𝐹 ) ⊆ ∪ ran Fil
14	13	sseli	⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → 𝐹 ∈ ∪ ran Fil )
15	12 14	impbii	⊢ ( 𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )