Metamath Proof Explorer


Theorem filssufilg

Description: A filter is contained in some ultrafilter. This version of filssufil contains the choice as a hypothesis (in the assumption that ~P ~P X is well-orderable). (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion filssufilg ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹𝑓 )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → 𝒫 𝒫 𝑋 ∈ dom card )
2 rabss ( { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ⊆ 𝒫 𝒫 𝑋 ↔ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹𝑔𝑔 ∈ 𝒫 𝒫 𝑋 ) )
3 filsspw ( 𝑔 ∈ ( Fil ‘ 𝑋 ) → 𝑔 ⊆ 𝒫 𝑋 )
4 velpw ( 𝑔 ∈ 𝒫 𝒫 𝑋𝑔 ⊆ 𝒫 𝑋 )
5 3 4 sylibr ( 𝑔 ∈ ( Fil ‘ 𝑋 ) → 𝑔 ∈ 𝒫 𝒫 𝑋 )
6 5 a1d ( 𝑔 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹𝑔𝑔 ∈ 𝒫 𝒫 𝑋 ) )
7 2 6 mprgbir { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ⊆ 𝒫 𝒫 𝑋
8 ssnum ( ( 𝒫 𝒫 𝑋 ∈ dom card ∧ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ⊆ 𝒫 𝒫 𝑋 ) → { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∈ dom card )
9 1 7 8 sylancl ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∈ dom card )
10 ssid 𝐹𝐹
11 10 jctr ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹𝐹 ) )
12 sseq2 ( 𝑔 = 𝐹 → ( 𝐹𝑔𝐹𝐹 ) )
13 12 elrab ( 𝐹 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹𝐹 ) )
14 11 13 sylibr ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } )
15 14 ne0d ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ≠ ∅ )
16 15 adantr ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ≠ ∅ )
17 sseq2 ( 𝑔 = 𝑥 → ( 𝐹𝑔𝐹 𝑥 ) )
18 simpr1 ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) ) → 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } )
19 ssrab ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ↔ ( 𝑥 ⊆ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑔𝑥 𝐹𝑔 ) )
20 18 19 sylib ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) ) → ( 𝑥 ⊆ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑔𝑥 𝐹𝑔 ) )
21 20 simpld ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) ) → 𝑥 ⊆ ( Fil ‘ 𝑋 ) )
22 simpr2 ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) ) → 𝑥 ≠ ∅ )
23 simpr3 ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) ) → [] Or 𝑥 )
24 sorpssun ( ( [] Or 𝑥 ∧ ( 𝑔𝑥𝑥 ) ) → ( 𝑔 ) ∈ 𝑥 )
25 24 ralrimivva ( [] Or 𝑥 → ∀ 𝑔𝑥𝑥 ( 𝑔 ) ∈ 𝑥 )
26 23 25 syl ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) ) → ∀ 𝑔𝑥𝑥 ( 𝑔 ) ∈ 𝑥 )
27 filuni ( ( 𝑥 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑥 ≠ ∅ ∧ ∀ 𝑔𝑥𝑥 ( 𝑔 ) ∈ 𝑥 ) → 𝑥 ∈ ( Fil ‘ 𝑋 ) )
28 21 22 26 27 syl3anc ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) ) → 𝑥 ∈ ( Fil ‘ 𝑋 ) )
29 n0 ( 𝑥 ≠ ∅ ↔ ∃ 𝑥 )
30 ssel2 ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ) → ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } )
31 sseq2 ( 𝑔 = → ( 𝐹𝑔𝐹 ) )
32 31 elrab ( ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ↔ ( ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ) )
33 30 32 sylib ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ) → ( ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ) )
34 33 simprd ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ) → 𝐹 )
35 ssuni ( ( 𝐹𝑥 ) → 𝐹 𝑥 )
36 34 35 sylancom ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ) → 𝐹 𝑥 )
37 36 ex ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } → ( 𝑥𝐹 𝑥 ) )
38 37 exlimdv ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } → ( ∃ 𝑥𝐹 𝑥 ) )
39 29 38 syl5bi ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } → ( 𝑥 ≠ ∅ → 𝐹 𝑥 ) )
40 18 22 39 sylc ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) ) → 𝐹 𝑥 )
41 17 28 40 elrabd ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) ) → 𝑥 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } )
42 41 ex ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) → 𝑥 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ) )
43 42 alrimiv ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∀ 𝑥 ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) → 𝑥 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ) )
44 43 adantr ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → ∀ 𝑥 ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) → 𝑥 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ) )
45 zornn0g ( ( { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∈ dom card ∧ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ≠ ∅ ∧ ∀ 𝑥 ( ( 𝑥 ⊆ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ 𝑥 ≠ ∅ ∧ [] Or 𝑥 ) → 𝑥 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ) ) → ∃ 𝑓 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∀ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ¬ 𝑓 )
46 9 16 44 45 syl3anc ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → ∃ 𝑓 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∀ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ¬ 𝑓 )
47 sseq2 ( 𝑔 = 𝑓 → ( 𝐹𝑔𝐹𝑓 ) )
48 47 elrab ( 𝑓 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ↔ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹𝑓 ) )
49 31 ralrab ( ∀ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ¬ 𝑓 ↔ ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 → ¬ 𝑓 ) )
50 simpll ( ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹𝑓 ) ∧ ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 → ¬ 𝑓 ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
51 sstr2 ( 𝐹𝑓 → ( 𝑓𝐹 ) )
52 51 imim1d ( 𝐹𝑓 → ( ( 𝐹 → ¬ 𝑓 ) → ( 𝑓 → ¬ 𝑓 ) ) )
53 df-pss ( 𝑓 ↔ ( 𝑓𝑓 ) )
54 53 simplbi2 ( 𝑓 → ( 𝑓𝑓 ) )
55 54 necon1bd ( 𝑓 → ( ¬ 𝑓𝑓 = ) )
56 55 a2i ( ( 𝑓 → ¬ 𝑓 ) → ( 𝑓𝑓 = ) )
57 52 56 syl6 ( 𝐹𝑓 → ( ( 𝐹 → ¬ 𝑓 ) → ( 𝑓𝑓 = ) ) )
58 57 ralimdv ( 𝐹𝑓 → ( ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 → ¬ 𝑓 ) → ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝑓𝑓 = ) ) )
59 58 imp ( ( 𝐹𝑓 ∧ ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 → ¬ 𝑓 ) ) → ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝑓𝑓 = ) )
60 59 adantll ( ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹𝑓 ) ∧ ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 → ¬ 𝑓 ) ) → ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝑓𝑓 = ) )
61 isufil2 ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝑓𝑓 = ) ) )
62 50 60 61 sylanbrc ( ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹𝑓 ) ∧ ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 → ¬ 𝑓 ) ) → 𝑓 ∈ ( UFil ‘ 𝑋 ) )
63 simplr ( ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹𝑓 ) ∧ ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 → ¬ 𝑓 ) ) → 𝐹𝑓 )
64 62 63 jca ( ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹𝑓 ) ∧ ∀ ∈ ( Fil ‘ 𝑋 ) ( 𝐹 → ¬ 𝑓 ) ) → ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹𝑓 ) )
65 48 49 64 syl2anb ( ( 𝑓 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∧ ∀ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ¬ 𝑓 ) → ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹𝑓 ) )
66 65 reximi2 ( ∃ 𝑓 ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ∀ ∈ { 𝑔 ∈ ( Fil ‘ 𝑋 ) ∣ 𝐹𝑔 } ¬ 𝑓 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹𝑓 )
67 46 66 syl ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝒫 𝒫 𝑋 ∈ dom card ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹𝑓 )