Theorem uffix2

Description: A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	uffix2	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∩ 𝐹 ≠ ∅ ↔ ∃ 𝑥 ∈ 𝑋 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) )

Proof

Step	Hyp	Ref	Expression
1		ufilfil	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
2		filn0	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
3		intssuni	⊢ ( 𝐹 ≠ ∅ → ∩ 𝐹 ⊆ ∪ 𝐹 )
4	1 2 3	3syl	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ ∪ 𝐹 )
5		filunibas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
6	1 5	syl	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
7	4 6	sseqtrd	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ 𝑋 )
8	7	sseld	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ∩ 𝐹 → 𝑥 ∈ 𝑋 ) )
9	8	pm4.71rd	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ∩ 𝐹 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ ∩ 𝐹 ) ) )
10		uffixfr	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ∩ 𝐹 ↔ 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) )
11	10	anbi2d	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ ∩ 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) ) )
12	9 11	bitrd	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ∩ 𝐹 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) ) )
13	12	exbidv	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∃ 𝑥 𝑥 ∈ ∩ 𝐹 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) ) )
14		n0	⊢ ( ∩ 𝐹 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ∩ 𝐹 )
15		df-rex	⊢ ( ∃ 𝑥 ∈ 𝑋 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) )
16	13 14 15	3bitr4g	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∩ 𝐹 ≠ ∅ ↔ ∃ 𝑥 ∈ 𝑋 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) )