Theorem fillsb 10494

Description: A filter is closed under taking supersets.

Hypothesis

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

Assertion

Ref	Expression
fillsb	|- (F e. Fil -> ((A e. F /\ B (_ X /\ A (_ B) -> B e. F))

Proof of Theorem fillsb

Step	Hyp	Ref	Expression
1		uniexg 2867	. . . . 5 |- (F e. Fil -> U.F e. V)
2		fillsb.1	. . . . . . 7 |- X = U.F
3	2	eqcomi 1477	. . . . . 6 |- U.F = X
4	3	eleq1i 1535	. . . . 5 |- (U.F e. V <-> X e. V)
5	1, 4	sylib 198	. . . 4 |- (F e. Fil -> X e. V)
6		elpw2g 2723	. . . . . . . . . 10 |- (X e. V -> (B e. P~X <-> B (_ X))
7	6	bicomd 520	. . . . . . . . 9 |- (X e. V -> (B (_ X <-> B e. P~X))
8	7	anbi2d 615	. . . . . . . 8 |- (X e. V -> ((A e. F /\ B (_ X) <-> (A e. F /\ B e. P~X)))
9	8	biimpd 153	. . . . . . 7 |- (X e. V -> ((A e. F /\ B (_ X) -> (A e. F /\ B e. P~X)))
10		3simpa 784	. . . . . . . 8 |- ((A e. F /\ B (_ X /\ A (_ B) -> (A e. F /\ B (_ X))
11	10	imim1i 16	. . . . . . 7 |- (((A e. F /\ B (_ X) -> (A e. F /\ B e. P~X)) -> ((A e. F /\ B (_ X /\ A (_ B) -> (A e. F /\ B e. P~X)))
12	9, 11	syl 10	. . . . . 6 |- (X e. V -> ((A e. F /\ B (_ X /\ A (_ B) -> (A e. F /\ B e. P~X)))
13		eleq1 1532	. . . . . . . . . 10 |- (x = A -> (x e. F <-> A e. F))
14		sseq1 2079	. . . . . . . . . 10 |- (x = A -> (x (_ y <-> A (_ y))
15	13, 14	3anbi13d 894	. . . . . . . . 9 |- (x = A -> ((x e. F /\ y (_ X /\ x (_ y) <-> (A e. F /\ y (_ X /\ A (_ y)))
16	15	imbi1d 612	. . . . . . . 8 |- (x = A -> (((x e. F /\ y (_ X /\ x (_ y) -> y e. F) <-> ((A e. F /\ y (_ X /\ A (_ y) -> y e. F)))
17	16	imbi2d 611	. . . . . . 7 |- (x = A -> ((F e. Fil -> ((x e. F /\ y (_ X /\ x (_ y) -> y e. F)) <-> (F e. Fil -> ((A e. F /\ y (_ X /\ A (_ y) -> y e. F))))
18		sseq1 2079	. . . . . . . . . 10 |- (y = B -> (y (_ X <-> B (_ X))
19		sseq2 2080	. . . . . . . . . 10 |- (y = B -> (A (_ y <-> A (_ B))
20	18, 19	3anbi23d 895	. . . . . . . . 9 |- (y = B -> ((A e. F /\ y (_ X /\ A (_ y) <-> (A e. F /\ B (_ X /\ A (_ B)))
21		eleq1 1532	. . . . . . . . 9 |- (y = B -> (y e. F <-> B e. F))
22	20, 21	imbi12d 625	. . . . . . . 8 |- (y = B -> (((A e. F /\ y (_ X /\ A (_ y) -> y e. F) <-> ((A e. F /\ B (_ X /\ A (_ B) -> B e. F)))
23	22	imbi2d 611	. . . . . . 7 |- (y = B -> ((F e. Fil -> ((A e. F /\ y (_ X /\ A (_ y) -> y e. F)) <-> (F e. Fil -> ((A e. F /\ B (_ X /\ A (_ B) -> B e. F))))
24	2	isfil 10492	. . . . . . . . . . 11 |- (F e. Fil -> (F e. Fil <-> ((-. (/) e. F /\ X e. F) /\ A.xA.y((x e. F /\ y (_ X /\ x (_ y) -> y e. F) /\ A.x e. F A.y e. F (x i^i y) e. F)))
25	24	ibi 591	. . . . . . . . . 10 |- (F e. Fil -> ((-. (/) e. F /\ X e. F) /\ A.xA.y((x e. F /\ y (_ X /\ x (_ y) -> y e. F) /\ A.x e. F A.y e. F (x i^i y) e. F))
26	25	3simp2d 794	. . . . . . . . 9 |- (F e. Fil -> A.xA.y((x e. F /\ y (_ X /\ x (_ y) -> y e. F))
27	26	19.21bi 1059	. . . . . . . 8 |- (F e. Fil -> A.y((x e. F /\ y (_ X /\ x (_ y) -> y e. F))
28	27	19.21bi 1059	. . . . . . 7 |- (F e. Fil -> ((x e. F /\ y (_ X /\ x (_ y) -> y e. F))
29	17, 23, 28	vtocl2g 1847	. . . . . 6 |- ((A e. F /\ B e. P~X) -> (F e. Fil -> ((A e. F /\ B (_ X /\ A (_ B) -> B e. F)))
30	12, 29	syl6 22	. . . . 5 |- (X e. V -> ((A e. F /\ B (_ X /\ A (_ B) -> (F e. Fil -> ((A e. F /\ B (_ X /\ A (_ B) -> B e. F))))
31	30	com23 32	. . . 4 |- (X e. V -> (F e. Fil -> ((A e. F /\ B (_ X /\ A (_ B) -> ((A e. F /\ B (_ X /\ A (_ B) -> B e. F))))
32	5, 31	syl 10	. . 3 |- (F e. Fil -> (F e. Fil -> ((A e. F /\ B (_ X /\ A (_ B) -> ((A e. F /\ B (_ X /\ A (_ B) -> B e. F))))
33	32	pm2.43i 64	. 2 |- (F e. Fil -> ((A e. F /\ B (_ X /\ A (_ B) -> ((A e. F /\ B (_ X /\ A (_ B) -> B e. F)))
34	33	pm2.43d 65	1 |- (F e. Fil -> ((A e. F /\ B (_ X /\ A (_ B) -> B e. F))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   /\ w3a 774  A.wal 953   = wceq 955   e. wcel 957  A.wral 1643  Vcvv 1808   i^i cin 2043   (_ wss 2044  (/)c0 2277  P~cpw 2398  U.cuni 2499  Filcfil 10490

This theorem is referenced by:  filintf 10502

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-un 2862

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-ral 1647  df-v 1809  df-in 2048  df-ss 2050  df-pw 2399  df-uni 2500  df-fil 10491

Copyright terms: Public domain