Theorem uffixfr 15575

Description: An ultrafilter is either fixed or free. A fixed ultrafilter is called principal, and a free ultrafilter is called nonprincipal. Note that free ultrafilters cannot be constructed.

Hypothesis

Ref	Expression
uffixfr.1	|- X = U.F

Assertion

Ref	Expression
uffixfr	|- (F e. UFil -> (|^|F = (/) \/ E.x e. X A.y e. ~P X(y e. F <-> x e. y)))

Distinct variable groups:   x,y,F   x,X,y

Proof of Theorem uffixfr

Step	Hyp	Ref	Expression
1		r19.2z 2958	. . . . . . . . 9 |- ((F =/= (/) /\ A.x e. F z e. x) -> E.x e. F z e. x)
2		elssuni 3206	. . . . . . . . . . . 12 |- (x e. F -> x C_ U.F)
3		uffixfr.1	. . . . . . . . . . . 12 |- X = U.F
4	2, 3	syl6ssr 2664	. . . . . . . . . . 11 |- (x e. F -> x C_ X)
5	4	sseld 2619	. . . . . . . . . 10 |- (x e. F -> (z e. x -> z e. X))
6	5	r19.23aiv 2211	. . . . . . . . 9 |- (E.x e. F z e. x -> z e. X)
7	1, 6	syl 12	. . . . . . . 8 |- ((F =/= (/) /\ A.x e. F z e. x) -> z e. X)
8		ufilfil 15566	. . . . . . . . 9 |- (F e. UFil -> F e. Fil)
9	3	filusb 10267	. . . . . . . . 9 |- (F e. Fil -> X e. F)
10		ne0i 2881	. . . . . . . . 9 |- (X e. F -> F =/= (/))
11	8, 9, 10	3syl 24	. . . . . . . 8 |- (F e. UFil -> F =/= (/))
12	7, 11	sylan 497	. . . . . . 7 |- ((F e. UFil /\ A.x e. F z e. x) -> z e. X)
13		visset 2295	. . . . . . . 8 |- z e. _V
14	13	elint2 3221	. . . . . . 7 |- (z e. |^|F <-> A.x e. F z e. x)
15	12, 14	sylan2b 501	. . . . . 6 |- ((F e. UFil /\ z e. |^|F) -> z e. X)
16		elinti 3223	. . . . . . . . . . 11 |- (z e. |^|F -> (y e. F -> z e. y))
17	16	ad2antlr 441	. . . . . . . . . 10 |- (((F e. UFil /\ z e. |^|F) /\ y C_ X) -> (y e. F -> z e. y))
18		snex 3492	. . . . . . . . . . . . . . . . 17 |- {z} e. _V
19	18	a1i 8	. . . . . . . . . . . . . . . 16 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> {z} e. _V)
20		snnzg 3118	. . . . . . . . . . . . . . . . 17 |- (z e. y -> {z} =/= (/))
21	20	ad2antll 443	. . . . . . . . . . . . . . . 16 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> {z} =/= (/))
22		oefil2 10275	. . . . . . . . . . . . . . . . 17 |- (({z} e. _V /\ {z} =/= (/)) -> {{z}} e. Fil)
23		filfbas 10276	. . . . . . . . . . . . . . . . 17 |- ({{z}} e. Fil -> {{z}} e. fBas)
24	22, 23	syl 12	. . . . . . . . . . . . . . . 16 |- (({z} e. _V /\ {z} =/= (/)) -> {{z}} e. fBas)
25	19, 21, 24	syl11anc 524	. . . . . . . . . . . . . . 15 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> {{z}} e. fBas)
26	15	snssd 3130	. . . . . . . . . . . . . . . 16 |- ((F e. UFil /\ z e. |^|F) -> {z} C_ X)
27	26	adantr 425	. . . . . . . . . . . . . . 15 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> {z} C_ X)
28	18	unisn 3193	. . . . . . . . . . . . . . . . 17 |- U.{{z}} = {z}
29	28	eqcomi 1888	. . . . . . . . . . . . . . . 16 |- {z} = U.{{z}}
30	29	extbas1 10291	. . . . . . . . . . . . . . 15 |- (({{z}} e. fBas /\ {z} C_ X) -> ({{z}} u. {X}) e. fBas)
31	25, 27, 30	syl11anc 524	. . . . . . . . . . . . . 14 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> ({{z}} u. {X}) e. fBas)
32		uniun 3196	. . . . . . . . . . . . . . . 16 |- U.({{z}} u. {X}) = (U.{{z}} u. U.{X})
33	32	eqcomi 1888	. . . . . . . . . . . . . . 15 |- (U.{{z}} u. U.{X}) = U.({{z}} u. {X})
34	33	elfg 10284	. . . . . . . . . . . . . 14 |- (({{z}} u. {X}) e. fBas -> (y e. (filGen` ({{z}} u. {X})) <-> (y C_ (U.{{z}} u. U.{X}) /\ E.x e. ({{z}} u. {X})x C_ y)))
35	31, 34	syl 12	. . . . . . . . . . . . 13 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> (y e. (filGen` ({{z}} u. {X})) <-> (y C_ (U.{{z}} u. U.{X}) /\ E.x e. ({{z}} u. {X})x C_ y)))
36		simpr 350	. . . . . . . . . . . . . . . 16 |- ((F e. UFil /\ y C_ X) -> y C_ X)
37		uniexg 3795	. . . . . . . . . . . . . . . . . . 19 |- (F e. UFil -> U.F e. _V)
38	37, 3	syl5eqel 1975	. . . . . . . . . . . . . . . . . 18 |- (F e. UFil -> X e. _V)
39		unisng 3194	. . . . . . . . . . . . . . . . . 18 |- (X e. _V -> U.{X} = X)
40	38, 39	syl 12	. . . . . . . . . . . . . . . . 17 |- (F e. UFil -> U.{X} = X)
41	40	adantr 425	. . . . . . . . . . . . . . . 16 |- ((F e. UFil /\ y C_ X) -> U.{X} = X)
42	36, 41	sseqtr4d 2654	. . . . . . . . . . . . . . 15 |- ((F e. UFil /\ y C_ X) -> y C_ U.{X})
43		ssun2 2768	. . . . . . . . . . . . . . . 16 |- U.{X} C_ (U.{{z}} u. U.{X})
44	43	a1i 8	. . . . . . . . . . . . . . 15 |- ((F e. UFil /\ y C_ X) -> U.{X} C_ (U.{{z}} u. U.{X}))
45	42, 44	sstrd 2627	. . . . . . . . . . . . . 14 |- ((F e. UFil /\ y C_ X) -> y C_ (U.{{z}} u. U.{X}))
46	45	ad2ant2r 445	. . . . . . . . . . . . 13 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> y C_ (U.{{z}} u. U.{X}))
47		ssun1 2767	. . . . . . . . . . . . . . . 16 |- {{z}} C_ ({{z}} u. {X})
48	18	snid 3069	. . . . . . . . . . . . . . . 16 |- {z} e. {{z}}
49	47, 48	sselii 2618	. . . . . . . . . . . . . . 15 |- {z} e. ({{z}} u. {X})
50	49	a1i 8	. . . . . . . . . . . . . 14 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> {z} e. ({{z}} u. {X}))
51		snssi 3129	. . . . . . . . . . . . . . 15 |- (z e. y -> {z} C_ y)
52	51	ad2antll 443	. . . . . . . . . . . . . 14 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> {z} C_ y)
53		sseq1 2637	. . . . . . . . . . . . . . 15 |- (x = {z} -> (x C_ y <-> {z} C_ y))
54	53	rcla4ev 2381	. . . . . . . . . . . . . 14 |- (({z} e. ({{z}} u. {X}) /\ {z} C_ y) -> E.x e. ({{z}} u. {X})x C_ y)
55	50, 52, 54	syl11anc 524	. . . . . . . . . . . . 13 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> E.x e. ({{z}} u. {X})x C_ y)
56	35, 46, 55	mpbir2and 802	. . . . . . . . . . . 12 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> y e. (filGen` ({{z}} u. {X})))
57		simpll 448	. . . . . . . . . . . . 13 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> F e. UFil)
58		fgfil 10290	. . . . . . . . . . . . . 14 |- (({{z}} u. {X}) e. fBas -> (filGen` ({{z}} u. {X})) e. Fil)
59	31, 58	syl 12	. . . . . . . . . . . . 13 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> (filGen` ({{z}} u. {X})) e. Fil)
60	28	a1i 8	. . . . . . . . . . . . . . 15 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> U.{{z}} = {z})
61	40	ad2antrr 440	. . . . . . . . . . . . . . 15 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> U.{X} = X)
62	60, 61	uneq12d 2756	. . . . . . . . . . . . . 14 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> (U.{{z}} u. U.{X}) = ({z} u. X))
63	33	fgbas 10286	. . . . . . . . . . . . . . 15 |- (({{z}} u. {X}) e. fBas -> (U.{{z}} u. U.{X}) = U.(filGen` ({{z}} u. {X})))
64	31, 63	syl 12	. . . . . . . . . . . . . 14 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> (U.{{z}} u. U.{X}) = U.(filGen` ({{z}} u. {X})))
65		ssequn1 2775	. . . . . . . . . . . . . . 15 |- ({z} C_ X <-> ({z} u. X) = X)
66	27, 65	sylib 215	. . . . . . . . . . . . . 14 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> ({z} u. X) = X)
67	62, 64, 66	3eqtr3rd 1936	. . . . . . . . . . . . 13 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> X = U.(filGen` ({{z}} u. {X})))
68	33	elfg 10284	. . . . . . . . . . . . . . . . . 18 |- (({{z}} u. {X}) e. fBas -> (x e. (filGen` ({{z}} u. {X})) <-> (x C_ (U.{{z}} u. U.{X}) /\ E.w e. ({{z}} u. {X})w C_ x)))
69	31, 68	syl 12	. . . . . . . . . . . . . . . . 17 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> (x e. (filGen` ({{z}} u. {X})) <-> (x C_ (U.{{z}} u. U.{X}) /\ E.w e. ({{z}} u. {X})w C_ x)))
70	69	adantr 425	. . . . . . . . . . . . . . . 16 |- ((((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) /\ x e. F) -> (x e. (filGen` ({{z}} u. {X})) <-> (x C_ (U.{{z}} u. U.{X}) /\ E.w e. ({{z}} u. {X})w C_ x)))
71	4	adantl 424	. . . . . . . . . . . . . . . . . . . 20 |- ((F e. UFil /\ x e. F) -> x C_ X)
72	40	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((F e. UFil /\ x e. F) -> U.{X} = X)
73	71, 72	sseqtr4d 2654	. . . . . . . . . . . . . . . . . . 19 |- ((F e. UFil /\ x e. F) -> x C_ U.{X})
74	43	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- ((F e. UFil /\ x e. F) -> U.{X} C_ (U.{{z}} u. U.{X}))
75	73, 74	sstrd 2627	. . . . . . . . . . . . . . . . . 18 |- ((F e. UFil /\ x e. F) -> x C_ (U.{{z}} u. U.{X}))
76	75	adantlr 429	. . . . . . . . . . . . . . . . 17 |- (((F e. UFil /\ z e. |^|F) /\ x e. F) -> x C_ (U.{{z}} u. U.{X}))
77	76	adantlr 429	. . . . . . . . . . . . . . . 16 |- ((((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) /\ x e. F) -> x C_ (U.{{z}} u. U.{X}))
78	49	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- ((z e. |^|F /\ x e. F) -> {z} e. ({{z}} u. {X}))
79		elinti 3223	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. |^|F -> (x e. F -> z e. x))
80	79	imp 377	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. |^|F /\ x e. F) -> z e. x)
81	80	snssd 3130	. . . . . . . . . . . . . . . . . . 19 |- ((z e. |^|F /\ x e. F) -> {z} C_ x)
82		sseq1 2637	. . . . . . . . . . . . . . . . . . . 20 |- (w = {z} -> (w C_ x <-> {z} C_ x))
83	82	rcla4ev 2381	. . . . . . . . . . . . . . . . . . 19 |- (({z} e. ({{z}} u. {X}) /\ {z} C_ x) -> E.w e. ({{z}} u. {X})w C_ x)
84	78, 81, 83	syl11anc 524	. . . . . . . . . . . . . . . . . 18 |- ((z e. |^|F /\ x e. F) -> E.w e. ({{z}} u. {X})w C_ x)
85	84	adantll 428	. . . . . . . . . . . . . . . . 17 |- (((F e. UFil /\ z e. |^|F) /\ x e. F) -> E.w e. ({{z}} u. {X})w C_ x)
86	85	adantlr 429	. . . . . . . . . . . . . . . 16 |- ((((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) /\ x e. F) -> E.w e. ({{z}} u. {X})w C_ x)
87	70, 77, 86	mpbir2and 802	. . . . . . . . . . . . . . 15 |- ((((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) /\ x e. F) -> x e. (filGen` ({{z}} u. {X})))
88	87	ex 402	. . . . . . . . . . . . . 14 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> (x e. F -> x e. (filGen` ({{z}} u. {X}))))
89	88	ssrdv 2622	. . . . . . . . . . . . 13 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> F C_ (filGen` ({{z}} u. {X})))
90		eqid 1884	. . . . . . . . . . . . . 14 |- U.(filGen` ({{z}} u. {X})) = U.(filGen` ({{z}} u. {X}))
91	3, 90	ufilmax 15568	. . . . . . . . . . . . 13 |- (((F e. UFil /\ (filGen` ({{z}} u. {X})) e. Fil) /\ (X = U.(filGen` ({{z}} u. {X})) /\ F C_ (filGen` ({{z}} u. {X})))) -> F = (filGen` ({{z}} u. {X})))
92	57, 59, 67, 89, 91	syl22anc 1101	. . . . . . . . . . . 12 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> F = (filGen` ({{z}} u. {X})))
93	56, 92	eleqtrrd 1974	. . . . . . . . . . 11 |- (((F e. UFil /\ z e. |^|F) /\ (y C_ X /\ z e. y)) -> y e. F)
94	93	expr 418	. . . . . . . . . 10 |- (((F e. UFil /\ z e. |^|F) /\ y C_ X) -> (z e. y -> y e. F))
95	17, 94	impbid 574	. . . . . . . . 9 |- (((F e. UFil /\ z e. |^|F) /\ y C_ X) -> (y e. F <-> z e. y))
96	95	ex 402	. . . . . . . 8 |- ((F e. UFil /\ z e. |^|F) -> (y C_ X -> (y e. F <-> z e. y)))
97		visset 2295	. . . . . . . . 9 |- y e. _V
98	97	elpw 3037	. . . . . . . 8 |- (y e. ~PX <-> y C_ X)
99	96, 98	syl5ib 223	. . . . . . 7 |- ((F e. UFil /\ z e. |^|F) -> (y e. ~PX -> (y e. F <-> z e. y)))
100	99	r19.21aiv 2175	. . . . . 6 |- ((F e. UFil /\ z e. |^|F) -> A.y e. ~P X(y e. F <-> z e. y))
101		eleq1 1957	. . . . . . . . 9 |- (x = z -> (x e. y <-> z e. y))
102	101	bibi2d 680	. . . . . . . 8 |- (x = z -> ((y e. F <-> x e. y) <-> (y e. F <-> z e. y)))
103	102	ralbidv 2123	. . . . . . 7 |- (x = z -> (A.y e. ~P X(y e. F <-> x e. y) <-> A.y e. ~P X(y e. F <-> z e. y)))
104	103	rcla4ev 2381	. . . . . 6 |- ((z e. X /\ A.y e. ~P X(y e. F <-> z e. y)) -> E.x e. X A.y e. ~P X(y e. F <-> x e. y))
105	15, 100, 104	syl11anc 524	. . . . 5 |- ((F e. UFil /\ z e. |^|F) -> E.x e. X A.y e. ~P X(y e. F <-> x e. y))
106	105	ex 402	. . . 4 |- (F e. UFil -> (z e. |^|F -> E.x e. X A.y e. ~P X(y e. F <-> x e. y)))
107	106	19.23adv 1584	. . 3 |- (F e. UFil -> (E.z z e. |^|F -> E.x e. X A.y e. ~P X(y e. F <-> x e. y)))
108		neq0 2885	. . 3 |- (-. |^|F = (/) <-> E.z z e. |^|F)
109	107, 108	syl5ib 223	. 2 |- (F e. UFil -> (-. |^|F = (/) -> E.x e. X A.y e. ~P X(y e. F <-> x e. y)))
110	109	orrd 250	1 |- (F e. UFil -> (|^|F = (/) \/ E.x e. X A.y e. ~P X(y e. F <-> x e. y)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   u. cun 2591   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {csn 3044  U.cuni 3177  |^|cint 3214  ` cfv 3998  fBascfbas 10257  filGencfg 10258  Filcfil 10264  UFilcufil 15562

This theorem is referenced by:  uffinfix 15577

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430  df-fi 10211  df-fbas 10259  df-fg 10260  df-fil 10265  df-ufil 15563

Copyright terms: Public domain