Theorem uffixfr

Description: An ultrafilter is either fixed or free. A fixed ultrafilter is called principal (generated by a single element A ), and a free ultrafilter is called nonprincipal (having empty intersection). Note that examples of free ultrafilters cannot be defined in ZFC without some form of global choice. (Contributed by Jeff Hankins, 4-Dec-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	uffixfr	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐴 ∈ ∩ 𝐹 ↔ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) )
2		ufilfil	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
3		filtop	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
4	2 3	syl	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
5		filn0	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
6		intssuni	⊢ ( 𝐹 ≠ ∅ → ∩ 𝐹 ⊆ ∪ 𝐹 )
7	2 5 6	3syl	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ ∪ 𝐹 )
8		filunibas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
9	2 8	syl	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
10	7 9	sseqtrd	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ 𝑋 )
11	10	sselda	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐴 ∈ 𝑋 )
12		uffix	⊢ ( ( 𝑋 ∈ 𝐹 ∧ 𝐴 ∈ 𝑋 ) → ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) ) )
13	4 11 12	syl2an2r	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) ) )
14	13	simprd	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) )
15	13	simpld	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) )
16		fgcl	⊢ ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen { { 𝐴 } } ) ∈ ( Fil ‘ 𝑋 ) )
17	15 16	syl	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → ( 𝑋 filGen { { 𝐴 } } ) ∈ ( Fil ‘ 𝑋 ) )
18	14 17	eqeltrd	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( Fil ‘ 𝑋 ) )
19	2	adantr	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
20		filsspw	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
21	19 20	syl	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 ⊆ 𝒫 𝑋 )
22		elintg	⊢ ( 𝐴 ∈ ∩ 𝐹 → ( 𝐴 ∈ ∩ 𝐹 ↔ ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 ) )
23	22	ibi	⊢ ( 𝐴 ∈ ∩ 𝐹 → ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 )
24	23	adantl	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 )
25		ssrab	⊢ ( 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 ) )
26	21 24 25	sylanbrc	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
27		ufilmax	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
28	1 18 26 27	syl3anc	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
29		eqimss	⊢ ( 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } → 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
30	29	adantl	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
31	25	simprbi	⊢ ( 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } → ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 )
32	30 31	syl	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 )
33		eleq2	⊢ ( 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } → ( 𝑋 ∈ 𝐹 ↔ 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) )
34	33	biimpac	⊢ ( ( 𝑋 ∈ 𝐹 ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
35	4 34	sylan	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
36		eleq2	⊢ ( 𝑥 = 𝑋 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑋 ) )
37	36	elrab	⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ ( 𝑋 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑋 ) )
38	37	simprbi	⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } → 𝐴 ∈ 𝑋 )
39		elintg	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ ∩ 𝐹 ↔ ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 ) )
40	35 38 39	3syl	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → ( 𝐴 ∈ ∩ 𝐹 ↔ ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 ) )
41	32 40	mpbird	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → 𝐴 ∈ ∩ 𝐹 )
42	28 41	impbida	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐴 ∈ ∩ 𝐹 ↔ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) )