# 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 ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge 𝒫𝒫{X}\in \mathrm{dom}\mathrm{card}\right)\to \exists {f}\in \mathrm{UFil}\left({X}\right)\phantom{\rule{.4em}{0ex}}{F}\subseteq {f}$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge 𝒫𝒫{X}\in \mathrm{dom}\mathrm{card}\right)\to 𝒫𝒫{X}\in \mathrm{dom}\mathrm{card}$
2 rabss ${⊢}\left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\subseteq 𝒫𝒫{X}↔\forall {g}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({F}\subseteq {g}\to {g}\in 𝒫𝒫{X}\right)$
3 filsspw ${⊢}{g}\in \mathrm{Fil}\left({X}\right)\to {g}\subseteq 𝒫{X}$
4 velpw ${⊢}{g}\in 𝒫𝒫{X}↔{g}\subseteq 𝒫{X}$
5 3 4 sylibr ${⊢}{g}\in \mathrm{Fil}\left({X}\right)\to {g}\in 𝒫𝒫{X}$
6 5 a1d ${⊢}{g}\in \mathrm{Fil}\left({X}\right)\to \left({F}\subseteq {g}\to {g}\in 𝒫𝒫{X}\right)$
7 2 6 mprgbir ${⊢}\left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\subseteq 𝒫𝒫{X}$
8 ssnum ${⊢}\left(𝒫𝒫{X}\in \mathrm{dom}\mathrm{card}\wedge \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\subseteq 𝒫𝒫{X}\right)\to \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\in \mathrm{dom}\mathrm{card}$
9 1 7 8 sylancl ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge 𝒫𝒫{X}\in \mathrm{dom}\mathrm{card}\right)\to \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\in \mathrm{dom}\mathrm{card}$
10 ssid ${⊢}{F}\subseteq {F}$
11 10 jctr ${⊢}{F}\in \mathrm{Fil}\left({X}\right)\to \left({F}\in \mathrm{Fil}\left({X}\right)\wedge {F}\subseteq {F}\right)$
12 sseq2 ${⊢}{g}={F}\to \left({F}\subseteq {g}↔{F}\subseteq {F}\right)$
13 12 elrab ${⊢}{F}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}↔\left({F}\in \mathrm{Fil}\left({X}\right)\wedge {F}\subseteq {F}\right)$
14 11 13 sylibr ${⊢}{F}\in \mathrm{Fil}\left({X}\right)\to {F}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}$
15 14 ne0d ${⊢}{F}\in \mathrm{Fil}\left({X}\right)\to \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\ne \varnothing$
16 15 adantr ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge 𝒫𝒫{X}\in \mathrm{dom}\mathrm{card}\right)\to \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\ne \varnothing$
17 sseq2 ${⊢}{g}=\bigcup {x}\to \left({F}\subseteq {g}↔{F}\subseteq \bigcup {x}\right)$
18 simpr1 ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge \left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\right)\to {x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}$
19 ssrab ${⊢}{x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}↔\left({x}\subseteq \mathrm{Fil}\left({X}\right)\wedge \forall {g}\in {x}\phantom{\rule{.4em}{0ex}}{F}\subseteq {g}\right)$
20 18 19 sylib ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge \left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\right)\to \left({x}\subseteq \mathrm{Fil}\left({X}\right)\wedge \forall {g}\in {x}\phantom{\rule{.4em}{0ex}}{F}\subseteq {g}\right)$
21 20 simpld ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge \left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\right)\to {x}\subseteq \mathrm{Fil}\left({X}\right)$
22 simpr2 ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge \left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\right)\to {x}\ne \varnothing$
23 simpr3 ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge \left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\right)\to \left[\subset \right]\mathrm{Or}{x}$
24 sorpssun ${⊢}\left(\left[\subset \right]\mathrm{Or}{x}\wedge \left({g}\in {x}\wedge {h}\in {x}\right)\right)\to {g}\cup {h}\in {x}$
25 24 ralrimivva ${⊢}\left[\subset \right]\mathrm{Or}{x}\to \forall {g}\in {x}\phantom{\rule{.4em}{0ex}}\forall {h}\in {x}\phantom{\rule{.4em}{0ex}}{g}\cup {h}\in {x}$
26 23 25 syl ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge \left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\right)\to \forall {g}\in {x}\phantom{\rule{.4em}{0ex}}\forall {h}\in {x}\phantom{\rule{.4em}{0ex}}{g}\cup {h}\in {x}$
27 filuni ${⊢}\left({x}\subseteq \mathrm{Fil}\left({X}\right)\wedge {x}\ne \varnothing \wedge \forall {g}\in {x}\phantom{\rule{.4em}{0ex}}\forall {h}\in {x}\phantom{\rule{.4em}{0ex}}{g}\cup {h}\in {x}\right)\to \bigcup {x}\in \mathrm{Fil}\left({X}\right)$
28 21 22 26 27 syl3anc ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge \left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\right)\to \bigcup {x}\in \mathrm{Fil}\left({X}\right)$
29 n0 ${⊢}{x}\ne \varnothing ↔\exists {h}\phantom{\rule{.4em}{0ex}}{h}\in {x}$
30 ssel2 ${⊢}\left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {h}\in {x}\right)\to {h}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}$
31 sseq2 ${⊢}{g}={h}\to \left({F}\subseteq {g}↔{F}\subseteq {h}\right)$
32 31 elrab ${⊢}{h}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}↔\left({h}\in \mathrm{Fil}\left({X}\right)\wedge {F}\subseteq {h}\right)$
33 30 32 sylib ${⊢}\left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {h}\in {x}\right)\to \left({h}\in \mathrm{Fil}\left({X}\right)\wedge {F}\subseteq {h}\right)$
34 33 simprd ${⊢}\left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {h}\in {x}\right)\to {F}\subseteq {h}$
35 ssuni ${⊢}\left({F}\subseteq {h}\wedge {h}\in {x}\right)\to {F}\subseteq \bigcup {x}$
36 34 35 sylancom ${⊢}\left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {h}\in {x}\right)\to {F}\subseteq \bigcup {x}$
37 36 ex ${⊢}{x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\to \left({h}\in {x}\to {F}\subseteq \bigcup {x}\right)$
38 37 exlimdv ${⊢}{x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\to \left(\exists {h}\phantom{\rule{.4em}{0ex}}{h}\in {x}\to {F}\subseteq \bigcup {x}\right)$
39 29 38 syl5bi ${⊢}{x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\to \left({x}\ne \varnothing \to {F}\subseteq \bigcup {x}\right)$
40 18 22 39 sylc ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge \left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\right)\to {F}\subseteq \bigcup {x}$
41 17 28 40 elrabd ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge \left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\right)\to \bigcup {x}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}$
42 41 ex ${⊢}{F}\in \mathrm{Fil}\left({X}\right)\to \left(\left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\to \bigcup {x}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\right)$
43 42 alrimiv ${⊢}{F}\in \mathrm{Fil}\left({X}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\to \bigcup {x}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\right)$
44 43 adantr ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge 𝒫𝒫{X}\in \mathrm{dom}\mathrm{card}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\to \bigcup {x}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\right)$
45 zornn0g ${⊢}\left(\left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\in \mathrm{dom}\mathrm{card}\wedge \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\ne \varnothing \wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge {x}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{x}\right)\to \bigcup {x}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\right)\right)\to \exists {f}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\phantom{\rule{.4em}{0ex}}\forall {h}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\phantom{\rule{.4em}{0ex}}¬{f}\subset {h}$
46 9 16 44 45 syl3anc ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge 𝒫𝒫{X}\in \mathrm{dom}\mathrm{card}\right)\to \exists {f}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\phantom{\rule{.4em}{0ex}}\forall {h}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\phantom{\rule{.4em}{0ex}}¬{f}\subset {h}$
47 sseq2 ${⊢}{g}={f}\to \left({F}\subseteq {g}↔{F}\subseteq {f}\right)$
48 47 elrab ${⊢}{f}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}↔\left({f}\in \mathrm{Fil}\left({X}\right)\wedge {F}\subseteq {f}\right)$
49 31 ralrab ${⊢}\forall {h}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\phantom{\rule{.4em}{0ex}}¬{f}\subset {h}↔\forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({F}\subseteq {h}\to ¬{f}\subset {h}\right)$
50 simpll ${⊢}\left(\left({f}\in \mathrm{Fil}\left({X}\right)\wedge {F}\subseteq {f}\right)\wedge \forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({F}\subseteq {h}\to ¬{f}\subset {h}\right)\right)\to {f}\in \mathrm{Fil}\left({X}\right)$
51 sstr2 ${⊢}{F}\subseteq {f}\to \left({f}\subseteq {h}\to {F}\subseteq {h}\right)$
52 51 imim1d ${⊢}{F}\subseteq {f}\to \left(\left({F}\subseteq {h}\to ¬{f}\subset {h}\right)\to \left({f}\subseteq {h}\to ¬{f}\subset {h}\right)\right)$
53 df-pss ${⊢}{f}\subset {h}↔\left({f}\subseteq {h}\wedge {f}\ne {h}\right)$
54 53 simplbi2 ${⊢}{f}\subseteq {h}\to \left({f}\ne {h}\to {f}\subset {h}\right)$
55 54 necon1bd ${⊢}{f}\subseteq {h}\to \left(¬{f}\subset {h}\to {f}={h}\right)$
56 55 a2i ${⊢}\left({f}\subseteq {h}\to ¬{f}\subset {h}\right)\to \left({f}\subseteq {h}\to {f}={h}\right)$
57 52 56 syl6 ${⊢}{F}\subseteq {f}\to \left(\left({F}\subseteq {h}\to ¬{f}\subset {h}\right)\to \left({f}\subseteq {h}\to {f}={h}\right)\right)$
58 57 ralimdv ${⊢}{F}\subseteq {f}\to \left(\forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({F}\subseteq {h}\to ¬{f}\subset {h}\right)\to \forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({f}\subseteq {h}\to {f}={h}\right)\right)$
59 58 imp ${⊢}\left({F}\subseteq {f}\wedge \forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({F}\subseteq {h}\to ¬{f}\subset {h}\right)\right)\to \forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({f}\subseteq {h}\to {f}={h}\right)$
60 59 adantll ${⊢}\left(\left({f}\in \mathrm{Fil}\left({X}\right)\wedge {F}\subseteq {f}\right)\wedge \forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({F}\subseteq {h}\to ¬{f}\subset {h}\right)\right)\to \forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({f}\subseteq {h}\to {f}={h}\right)$
61 isufil2 ${⊢}{f}\in \mathrm{UFil}\left({X}\right)↔\left({f}\in \mathrm{Fil}\left({X}\right)\wedge \forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({f}\subseteq {h}\to {f}={h}\right)\right)$
62 50 60 61 sylanbrc ${⊢}\left(\left({f}\in \mathrm{Fil}\left({X}\right)\wedge {F}\subseteq {f}\right)\wedge \forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({F}\subseteq {h}\to ¬{f}\subset {h}\right)\right)\to {f}\in \mathrm{UFil}\left({X}\right)$
63 simplr ${⊢}\left(\left({f}\in \mathrm{Fil}\left({X}\right)\wedge {F}\subseteq {f}\right)\wedge \forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({F}\subseteq {h}\to ¬{f}\subset {h}\right)\right)\to {F}\subseteq {f}$
64 62 63 jca ${⊢}\left(\left({f}\in \mathrm{Fil}\left({X}\right)\wedge {F}\subseteq {f}\right)\wedge \forall {h}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}\left({F}\subseteq {h}\to ¬{f}\subset {h}\right)\right)\to \left({f}\in \mathrm{UFil}\left({X}\right)\wedge {F}\subseteq {f}\right)$
65 48 49 64 syl2anb ${⊢}\left({f}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\wedge \forall {h}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\phantom{\rule{.4em}{0ex}}¬{f}\subset {h}\right)\to \left({f}\in \mathrm{UFil}\left({X}\right)\wedge {F}\subseteq {f}\right)$
66 65 reximi2 ${⊢}\exists {f}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\phantom{\rule{.4em}{0ex}}\forall {h}\in \left\{{g}\in \mathrm{Fil}\left({X}\right)|{F}\subseteq {g}\right\}\phantom{\rule{.4em}{0ex}}¬{f}\subset {h}\to \exists {f}\in \mathrm{UFil}\left({X}\right)\phantom{\rule{.4em}{0ex}}{F}\subseteq {f}$
67 46 66 syl ${⊢}\left({F}\in \mathrm{Fil}\left({X}\right)\wedge 𝒫𝒫{X}\in \mathrm{dom}\mathrm{card}\right)\to \exists {f}\in \mathrm{UFil}\left({X}\right)\phantom{\rule{.4em}{0ex}}{F}\subseteq {f}$