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 biimtrid ⊢ ( 𝑥 ⊆ { 𝑔 ∈ ( 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 ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )