This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fixufil

Description: The condition describing a fixed ultrafilter always produces an ultrafilter. (Contributed by Jeff Hankins, 9-Dec-2009) (Revised by Mario Carneiro, 12-Dec-2013) (Revised by Stefan O'Rear, 29-Jul-2015)

Ref Expression
Assertion fixufil ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( UFil ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 uffix ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) ) )
2 1 simprd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) )
3 1 simpld ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) )
4 fgcl ⊢ ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen { { 𝐴 } } ) ∈ ( Fil ‘ 𝑋 ) )
5 3 4 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑋 filGen { { 𝐴 } } ) ∈ ( Fil ‘ 𝑋 ) )
6 2 5 eqeltrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( Fil ‘ 𝑋 ) )
7 undif2 ⊢ ( 𝑦 ∪ ( 𝑋 ∖ 𝑦 ) ) = ( 𝑦 ∪ 𝑋 )
8 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋 )
9 ssequn1 ⊢ ( 𝑦 ⊆ 𝑋 ↔ ( 𝑦 ∪ 𝑋 ) = 𝑋 )
10 8 9 sylib ⊢ ( 𝑦 ∈ 𝒫 𝑋 → ( 𝑦 ∪ 𝑋 ) = 𝑋 )
11 7 10 eqtr2id ⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑋 = ( 𝑦 ∪ ( 𝑋 ∖ 𝑦 ) ) )
12 11 eleq2d ⊢ ( 𝑦 ∈ 𝒫 𝑋 → ( 𝐴 ∈ 𝑋 ↔ 𝐴 ∈ ( 𝑦 ∪ ( 𝑋 ∖ 𝑦 ) ) ) )
13 12 biimpac ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝒫 𝑋 ) → 𝐴 ∈ ( 𝑦 ∪ ( 𝑋 ∖ 𝑦 ) ) )
14 elun ⊢ ( 𝐴 ∈ ( 𝑦 ∪ ( 𝑋 ∖ 𝑦 ) ) ↔ ( 𝐴 ∈ 𝑦 ∨ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) )
15 13 14 sylib ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( 𝐴 ∈ 𝑦 ∨ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) )
16 15 adantll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( 𝐴 ∈ 𝑦 ∨ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) )
17 ibar ⊢ ( 𝑦 ∈ 𝒫 𝑋 → ( 𝐴 ∈ 𝑦 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ) )
18 17 adantl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( 𝐴 ∈ 𝑦 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ) )
19 difss ⊢ ( 𝑋 ∖ 𝑦 ) ⊆ 𝑋
20 elpw2g ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑦 ) ⊆ 𝑋 ) )
21 19 20 mpbiri ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 )
22 21 ad2antrr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 )
23 22 biantrurd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ↔ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) )
24 18 23 orbi12d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ↔ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ∨ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) ) )
25 16 24 mpbid ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ∨ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) )
26 25 ralrimiva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝒫 𝑋 ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ∨ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) )
27 eleq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
28 27 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) )
29 eleq2 ⊢ ( 𝑥 = ( 𝑋 ∖ 𝑦 ) → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) )
30 29 elrab ⊢ ( ( 𝑋 ∖ 𝑦 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) )
31 28 30 orbi12i ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∨ ( 𝑋 ∖ 𝑦 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) ↔ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ∨ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) )
32 31 ralbii ⊢ ( ∀ 𝑦 ∈ 𝒫 𝑋 ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∨ ( 𝑋 ∖ 𝑦 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) ↔ ∀ 𝑦 ∈ 𝒫 𝑋 ( ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦 ) ∨ ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ 𝐴 ∈ ( 𝑋 ∖ 𝑦 ) ) ) )
33 26 32 sylibr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝒫 𝑋 ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∨ ( 𝑋 ∖ 𝑦 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) )
34 isufil ⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( UFil ‘ 𝑋 ) ↔ ( { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑋 ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∨ ( 𝑋 ∖ 𝑦 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) ) )
35 6 33 34 sylanbrc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( UFil ‘ 𝑋 ) )