Theorem ufprim 15569

Description: An ultrafilter is a prime filter.

Hypothesis

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

Assertion

Ref	Expression
ufprim	|- ((F e. UFil /\ A C_ X /\ B C_ X) -> ((A e. F \/ B e. F) <-> (A u. B) e. F))

Proof of Theorem ufprim

Step	Hyp	Ref	Expression
1		ufilfil 15566	. . . . . . 7 |- (F e. UFil -> F e. Fil)
2	1	3ad2ant1 897	. . . . . 6 |- ((F e. UFil /\ A C_ X /\ B C_ X) -> F e. Fil)
3	2	adantr 425	. . . . 5 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ A e. F) -> F e. Fil)
4		simpr 350	. . . . . 6 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ A e. F) -> A e. F)
5		unss 2780	. . . . . . . . 9 |- ((A C_ X /\ B C_ X) <-> (A u. B) C_ X)
6	5	biimpi 168	. . . . . . . 8 |- ((A C_ X /\ B C_ X) -> (A u. B) C_ X)
7	6	3adant1 894	. . . . . . 7 |- ((F e. UFil /\ A C_ X /\ B C_ X) -> (A u. B) C_ X)
8	7	adantr 425	. . . . . 6 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ A e. F) -> (A u. B) C_ X)
9		ssun1 2767	. . . . . . 7 |- A C_ (A u. B)
10	9	a1i 8	. . . . . 6 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ A e. F) -> A C_ (A u. B))
11	4, 8, 10	3jca 1050	. . . . 5 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ A e. F) -> (A e. F /\ (A u. B) C_ X /\ A C_ (A u. B)))
12		ufprim.1	. . . . . 6 |- X = U.F
13	12	fillsb 10270	. . . . 5 |- (F e. Fil -> ((A e. F /\ (A u. B) C_ X /\ A C_ (A u. B)) -> (A u. B) e. F))
14	3, 11, 13	sylc 83	. . . 4 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ A e. F) -> (A u. B) e. F)
15	14	ex 402	. . 3 |- ((F e. UFil /\ A C_ X /\ B C_ X) -> (A e. F -> (A u. B) e. F))
16	2	adantr 425	. . . . 5 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ B e. F) -> F e. Fil)
17		simpr 350	. . . . . 6 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ B e. F) -> B e. F)
18	7	adantr 425	. . . . . 6 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ B e. F) -> (A u. B) C_ X)
19		ssun2 2768	. . . . . . 7 |- B C_ (A u. B)
20	19	a1i 8	. . . . . 6 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ B e. F) -> B C_ (A u. B))
21	17, 18, 20	3jca 1050	. . . . 5 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ B e. F) -> (B e. F /\ (A u. B) C_ X /\ B C_ (A u. B)))
22	12	fillsb 10270	. . . . 5 |- (F e. Fil -> ((B e. F /\ (A u. B) C_ X /\ B C_ (A u. B)) -> (A u. B) e. F))
23	16, 21, 22	sylc 83	. . . 4 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ B e. F) -> (A u. B) e. F)
24	23	ex 402	. . 3 |- ((F e. UFil /\ A C_ X /\ B C_ X) -> (B e. F -> (A u. B) e. F))
25	15, 24	jaod 469	. 2 |- ((F e. UFil /\ A C_ X /\ B C_ X) -> ((A e. F \/ B e. F) -> (A u. B) e. F))
26	12	ufilss 15567	. . . . . . . 8 |- ((F e. UFil /\ A C_ X) -> (A e. F \/ (X \ A) e. F))
27	26	3adant3 896	. . . . . . 7 |- ((F e. UFil /\ A C_ X /\ B C_ X) -> (A e. F \/ (X \ A) e. F))
28	27	adantr 425	. . . . . 6 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F) -> (A e. F \/ (X \ A) e. F))
29	28	ord 249	. . . . 5 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F) -> (-. A e. F -> (X \ A) e. F))
30	2	3ad2ant1 897	. . . . . . 7 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F /\ (X \ A) e. F) -> F e. Fil)
31		filint 10269	. . . . . . . . . . . 12 |- ((F e. Fil /\ (A u. B) e. F /\ (X \ A) e. F) -> ((A u. B) i^i (X \ A)) e. F)
32	31	3exp 1066	. . . . . . . . . . 11 |- (F e. Fil -> ((A u. B) e. F -> ((X \ A) e. F -> ((A u. B) i^i (X \ A)) e. F)))
33	1, 32	syl 12	. . . . . . . . . 10 |- (F e. UFil -> ((A u. B) e. F -> ((X \ A) e. F -> ((A u. B) i^i (X \ A)) e. F)))
34	33	3ad2ant1 897	. . . . . . . . 9 |- ((F e. UFil /\ A C_ X /\ B C_ X) -> ((A u. B) e. F -> ((X \ A) e. F -> ((A u. B) i^i (X \ A)) e. F)))
35	34	3imp 1061	. . . . . . . 8 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F /\ (X \ A) e. F) -> ((A u. B) i^i (X \ A)) e. F)
36		simp3 878	. . . . . . . . 9 |- ((F e. UFil /\ A C_ X /\ B C_ X) -> B C_ X)
37	36	3ad2ant1 897	. . . . . . . 8 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F /\ (X \ A) e. F) -> B C_ X)
38		elin 2786	. . . . . . . . . . 11 |- (x e. ((A u. B) i^i (X \ A)) <-> (x e. (A u. B) /\ x e. (X \ A)))
39		id 73	. . . . . . . . . . . . . 14 |- ((-. x e. A -> x e. B) -> (-. x e. A -> x e. B))
40	39	imp 377	. . . . . . . . . . . . 13 |- (((-. x e. A -> x e. B) /\ -. x e. A) -> x e. B)
41		eldifn 2731	. . . . . . . . . . . . 13 |- (x e. (X \ A) -> -. x e. A)
42	40, 41	sylan2 500	. . . . . . . . . . . 12 |- (((-. x e. A -> x e. B) /\ x e. (X \ A)) -> x e. B)
43		elun 2741	. . . . . . . . . . . . 13 |- (x e. (A u. B) <-> (x e. A \/ x e. B))
44		df-or 241	. . . . . . . . . . . . 13 |- ((x e. A \/ x e. B) <-> (-. x e. A -> x e. B))
45	43, 44	bitri 190	. . . . . . . . . . . 12 |- (x e. (A u. B) <-> (-. x e. A -> x e. B))
46	42, 45	sylanb 498	. . . . . . . . . . 11 |- ((x e. (A u. B) /\ x e. (X \ A)) -> x e. B)
47	38, 46	sylbi 216	. . . . . . . . . 10 |- (x e. ((A u. B) i^i (X \ A)) -> x e. B)
48	47	ssriv 2621	. . . . . . . . 9 |- ((A u. B) i^i (X \ A)) C_ B
49	48	a1i 8	. . . . . . . 8 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F /\ (X \ A) e. F) -> ((A u. B) i^i (X \ A)) C_ B)
50	35, 37, 49	3jca 1050	. . . . . . 7 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F /\ (X \ A) e. F) -> (((A u. B) i^i (X \ A)) e. F /\ B C_ X /\ ((A u. B) i^i (X \ A)) C_ B))
51	12	fillsb 10270	. . . . . . 7 |- (F e. Fil -> ((((A u. B) i^i (X \ A)) e. F /\ B C_ X /\ ((A u. B) i^i (X \ A)) C_ B) -> B e. F))
52	30, 50, 51	sylc 83	. . . . . 6 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F /\ (X \ A) e. F) -> B e. F)
53	52	3expia 1069	. . . . 5 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F) -> ((X \ A) e. F -> B e. F))
54	29, 53	syld 30	. . . 4 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F) -> (-. A e. F -> B e. F))
55	54	orrd 250	. . 3 |- (((F e. UFil /\ A C_ X /\ B C_ X) /\ (A u. B) e. F) -> (A e. F \/ B e. F))
56	55	ex 402	. 2 |- ((F e. UFil /\ A C_ X /\ B C_ X) -> ((A u. B) e. F -> (A e. F \/ B e. F)))
57	25, 56	impbid 574	1 |- ((F e. UFil /\ A C_ X /\ B C_ X) -> ((A e. F \/ B e. F) <-> (A u. B) e. F))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   \ cdif 2590   u. cun 2591   i^i cin 2592   C_ wss 2593  U.cuni 3177  Filcfil 10264  UFilcufil 15562

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-sep 3438  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pw 3035  df-uni 3178  df-fil 10265  df-ufil 15563

Copyright terms: Public domain