Theorem rcfpfil 10569

Description: Relative complements of the finite parts of an infinite set is a filter. When A = NN the set of the relative complements is called Frechet's filter and is used to define the concept of limit of a sequence.

Assertion

Ref	Expression
rcfpfil	|- ((A e. B /\ -. A e. Fin) -> {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} e. Fil)

Distinct variable groups:   A,b,x   B,b,x

Proof of Theorem rcfpfil

Step	Hyp	Ref	Expression
1		rcfpfillem2 10564	. . . . 5 |- (-. A e. Fin -> -. (/) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
2	1	adantl 390	. . . 4 |- ((A e. B /\ -. A e. Fin) -> -. (/) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
3		rcfpfillem3 10565	. . . . . 6 |- (A e. B -> U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} = A)
4		rcfpfillem5 10567	. . . . . 6 |- (A e. B -> A e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
5	3, 4	eqeltrd 1551	. . . . 5 |- (A e. B -> U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
6	5	adantr 391	. . . 4 |- ((A e. B /\ -. A e. Fin) -> U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
7	2, 6	jca 288	. . 3 |- ((A e. B /\ -. A e. Fin) -> (-. (/) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}))
8		rcfpfillem6 10568	. . . . . 6 |- ((u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ v (_ A /\ u (_ v) -> v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
9		unissb 2532	. . . . . . . 8 |- (U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} (_ A <-> A.y e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}y (_ A)
10		visset 1816	. . . . . . . . . 10 |- y e. V
11		eqeq1 1484	. . . . . . . . . . . 12 |- (x = y -> (x = (A \ b) <-> y = (A \ b)))
12	11	3anbi3d 901	. . . . . . . . . . 11 |- (x = y -> ((b (_ A /\ b e. Fin /\ x = (A \ b)) <-> (b (_ A /\ b e. Fin /\ y = (A \ b))))
13	12	exbidv 1281	. . . . . . . . . 10 |- (x = y -> (E.b(b (_ A /\ b e. Fin /\ x = (A \ b)) <-> E.b(b (_ A /\ b e. Fin /\ y = (A \ b))))
14	10, 13	elab 1900	. . . . . . . . 9 |- (y e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} <-> E.b(b (_ A /\ b e. Fin /\ y = (A \ b)))
15		difss 2170	. . . . . . . . . . . 12 |- (A \ b) (_ A
16		sseq1 2085	. . . . . . . . . . . 12 |- (y = (A \ b) -> (y (_ A <-> (A \ b) (_ A))
17	15, 16	mpbiri 194	. . . . . . . . . . 11 |- (y = (A \ b) -> y (_ A)
18	17	3ad2ant3 804	. . . . . . . . . 10 |- ((b (_ A /\ b e. Fin /\ y = (A \ b)) -> y (_ A)
19	18	19.23aiv 1297	. . . . . . . . 9 |- (E.b(b (_ A /\ b e. Fin /\ y = (A \ b)) -> y (_ A)
20	14, 19	sylbi 199	. . . . . . . 8 |- (y e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} -> y (_ A)
21	9, 20	mprgbir 1704	. . . . . . 7 |- U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} (_ A
22		sstr2 2074	. . . . . . 7 |- (v (_ U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} -> (U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} (_ A -> v (_ A))
23	21, 22	mpi 44	. . . . . 6 |- (v (_ U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} -> v (_ A)
24	8, 23	syl3an2 862	. . . . 5 |- ((u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ v (_ U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ u (_ v) -> v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
25	24	a1i 8	. . . 4 |- ((A e. B /\ -. A e. Fin) -> ((u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ v (_ U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ u (_ v) -> v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}))
26	25	19.21aivv 1289	. . 3 |- ((A e. B /\ -. A e. Fin) -> A.uA.v((u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ v (_ U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ u (_ v) -> v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}))
27		rcfpfillem4 10566	. . . 4 |- (A e. B -> A.u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}A.v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} (u i^i v) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
28	27	adantr 391	. . 3 |- ((A e. B /\ -. A e. Fin) -> A.u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}A.v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} (u i^i v) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))})
29	7, 26, 28	3jca 821	. 2 |- ((A e. B /\ -. A e. Fin) -> ((-. (/) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}) /\ A.uA.v((u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ v (_ U.{x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} /\ u (_ v) -> v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}) /\ A.u e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}A.v e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))} (u i^i v) e. {x | E.b(b (_ A /\ b e. Fin /\ x = (A \ b))}))
30		elpw2g 2732	. . . . . . . . . 10 |- (A e. B -> (b e. P~A <-> b (_ A))
31	30	bicomd 523	. . . . . . . . 9 |- (A e. B -> (b (_ A <-> b e. P~A))
32	31	3anbi1d 899	. . . . . . . 8 |- (A e. B -> ((b (_ A /\ b e. Fin /\ x = (A \ b)) <-> (b e. P~A /\ b e. Fin /\ x = (A \ b))))
33	32	opabbidv 2675	. . . . . . 7 |- (A e. B -> {<.b, x>. | (b (_ A /\ b e. Fin /\ x = (A \ b))} = {<.b, x>. | (b e. P~A /\ b e. Fin /\ x = (A \ b))})
34		pwexg 2752	. . . . . . . . . 10 |- (A e. B -> P~A e. V)
35		opabex2g 3617	. . . . . . . . . 10 |- (P~A e. V -> {<.b, x>. | (b e. P~A /\ x = (A \ b))} e. V)
36	34, 35	syl 10	. . . . . . . . 9 |- (A e. B -> {<.b, x>. | (b e. P~A /\ x = (A \ b))} e. V)
37		3simpb 788	. . . . . . . . . 10 |- ((b e. P~A /\ b e. Fin /\ x = (A \ b)) -> (b e. P~A /\ x = (A \ b)))
38	37	ssopab2i 2829	. . . . . . . . 9 |- {<.b, x>. | (b e. P~A /\ b e. Fin /\ x = (A \ b))} (_ {<.b, x>. | (b e. P~A /\ x = (A \ b))}
39	36, 38	jctil 292	. . . . . . . 8 |- (A e. B -> ({<.b, x>. | (b e. P~A /\ b e. Fin /\ x = (A \ b))} (_ {<.b, x>. | (b e. P~A /\ x = (A \ b))} /\ {<.b, x>. | (b e. P~A /\ x = (A \ b))} e. V))
40		ssexg 2726	. . . . . . . 8 |- (({<.b, x>. | (b e. P~A