Theorem fbfgss 10288

Description: A condition for a filter to be finer than another involving their filter bases. (Contributed by Jeff Hankins, 3-Sep-2009.)

Hypotheses

Ref	Expression
fbfgss.1	|- X = U.F
fbfgss.2	|- Y = U.G

Assertion

Ref	Expression
fbfgss	|- ((F e. fBas /\ G e. fBas /\ X = Y) -> ((filGen` F) C_ (filGen` G) <-> A.x e. F E.y e. G y C_ x))

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

Proof of Theorem fbfgss

Step	Hyp	Ref	Expression
1		fbfgss.2	. . . . . . . . 9 |- Y = U.G
2	1	elfg 10284	. . . . . . . 8 |- (G e. fBas -> (x e. (filGen` G) <-> (x C_ Y /\ E.y e. G y C_ x)))
3		simpr 350	. . . . . . . 8 |- ((x C_ Y /\ E.y e. G y C_ x) -> E.y e. G y C_ x)
4	2, 3	syl6bi 231	. . . . . . 7 |- (G e. fBas -> (x e. (filGen` G) -> E.y e. G y C_ x))
5	4	3ad2ant2 898	. . . . . 6 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> (x e. (filGen` G) -> E.y e. G y C_ x))
6		ssel2 2616	. . . . . 6 |- (((filGen` F) C_ (filGen` G) /\ x e. (filGen` F)) -> x e. (filGen` G))
7	5, 6	syl5 20	. . . . 5 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> (((filGen` F) C_ (filGen` G) /\ x e. (filGen` F)) -> E.y e. G y C_ x))
8	7	exp3a 405	. . . 4 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> ((filGen` F) C_ (filGen` G) -> (x e. (filGen` F) -> E.y e. G y C_ x)))
9		fbssfg 10285	. . . . . 6 |- (F e. fBas -> F C_ (filGen` F))
10	9	3ad2ant1 897	. . . . 5 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> F C_ (filGen` F))
11	10	sseld 2619	. . . 4 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> (x e. F -> x e. (filGen` F)))
12	8, 11	syl5d 66	. . 3 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> ((filGen` F) C_ (filGen` G) -> (x e. F -> E.y e. G y C_ x)))
13	12	r19.21adv 2181	. 2 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> ((filGen` F) C_ (filGen` G) -> A.x e. F E.y e. G y C_ x))
14		sseq2 2639	. . . . . . . . . . . . . . 15 |- (x = u -> (y C_ x <-> y C_ u))
15	14	rexbidv 2124	. . . . . . . . . . . . . 14 |- (x = u -> (E.y e. G y C_ x <-> E.y e. G y C_ u))
16	15	rcla4v 2376	. . . . . . . . . . . . 13 |- (u e. F -> (A.x e. F E.y e. G y C_ x -> E.y e. G y C_ u))
17	16	adantl 424	. . . . . . . . . . . 12 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) -> (A.x e. F E.y e. G y C_ x -> E.y e. G y C_ u))
18		simpll3 917	. . . . . . . . . . . . . . . . 17 |- ((((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) /\ (y e. G /\ (y C_ u /\ u C_ t))) -> X = Y)
19	18	sseq2d 2645	. . . . . . . . . . . . . . . 16 |- ((((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) /\ (y e. G /\ (y C_ u /\ u C_ t))) -> (t C_ X <-> t C_ Y))
20	19	biimpd 170	. . . . . . . . . . . . . . 15 |- ((((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) /\ (y e. G /\ (y C_ u /\ u C_ t))) -> (t C_ X -> t C_ Y))
21		sseq1 2637	. . . . . . . . . . . . . . . . . . 19 |- (v = y -> (v C_ t <-> y C_ t))
22	21	rcla4ev 2381	. . . . . . . . . . . . . . . . . 18 |- ((y e. G /\ y C_ t) -> E.v e. G v C_ t)
23	22	adantl 424	. . . . . . . . . . . . . . . . 17 |- ((((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) /\ (y e. G /\ y C_ t)) -> E.v e. G v C_ t)
24	23	a1d 15	. . . . . . . . . . . . . . . 16 |- ((((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) /\ (y e. G /\ y C_ t)) -> (t C_ X -> E.v e. G v C_ t))
25		sstr 2625	. . . . . . . . . . . . . . . 16 |- ((y C_ u /\ u C_ t) -> y C_ t)
26	24, 25	sylanr2 512	. . . . . . . . . . . . . . 15 |- ((((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) /\ (y e. G /\ (y C_ u /\ u C_ t))) -> (t C_ X -> E.v e. G v C_ t))
27	20, 26	jcad 661	. . . . . . . . . . . . . 14 |- ((((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) /\ (y e. G /\ (y C_ u /\ u C_ t))) -> (t C_ X -> (t C_ Y /\ E.v e. G v C_ t)))
28	27	exp45 417	. . . . . . . . . . . . 13 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) -> (y e. G -> (y C_ u -> (u C_ t -> (t C_ X -> (t C_ Y /\ E.v e. G v C_ t))))))
29	28	r19.23adv 2215	. . . . . . . . . . . 12 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) -> (E.y e. G y C_ u -> (u C_ t -> (t C_ X -> (t C_ Y /\ E.v e. G v C_ t)))))
30	17, 29	syld 30	. . . . . . . . . . 11 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ u e. F) -> (A.x e. F E.y e. G y C_ x -> (u C_ t -> (t C_ X -> (t C_ Y /\ E.v e. G v C_ t)))))
31	30	ex 402	. . . . . . . . . 10 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> (u e. F -> (A.x e. F E.y e. G y C_ x -> (u C_ t -> (t C_ X -> (t C_ Y /\ E.v e. G v C_ t))))))
32	31	com23 36	. . . . . . . . 9 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> (A.x e. F E.y e. G y C_ x -> (u e. F -> (u C_ t -> (t C_ X -> (t C_ Y /\ E.v e. G v C_ t))))))
33	32	imp 377	. . . . . . . 8 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ A.x e. F E.y e. G y C_ x) -> (u e. F -> (u C_ t -> (t C_ X -> (t C_ Y /\ E.v e. G v C_ t)))))
34	33	r19.23adv 2215	. . . . . . 7 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ A.x e. F E.y e. G y C_ x) -> (E.u e. F u C_ t -> (t C_ X -> (t C_ Y /\ E.v e. G v C_ t))))
35	34	com23 36	. . . . . 6 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ A.x e. F E.y e. G y C_ x) -> (t C_ X -> (E.u e. F u C_ t -> (t C_ Y /\ E.v e. G v C_ t))))
36	35	imp3a 388	. . . . 5 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ A.x e. F E.y e. G y C_ x) -> ((t C_ X /\ E.u e. F u C_ t) -> (t C_ Y /\ E.v e. G v C_ t)))
37		fbfgss.1	. . . . . . . 8 |- X = U.F
38	37	elfg 10284	. . . . . . 7 |- (F e. fBas -> (t e. (filGen` F) <-> (t C_ X /\ E.u e. F u C_ t)))
39	38	3ad2ant1 897	. . . . . 6 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> (t e. (filGen` F) <-> (t C_ X /\ E.u e. F u C_ t)))
40	39	adantr 425	. . . . 5 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ A.x e. F E.y e. G y C_ x) -> (t e. (filGen` F) <-> (t C_ X /\ E.u e. F u C_ t)))
41	1	elfg 10284	. . . . . . 7 |- (G e. fBas -> (t e. (filGen` G) <-> (t C_ Y /\ E.v e. G v C_ t)))
42	41	3ad2ant2 898	. . . . . 6 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> (t e. (filGen` G) <-> (t C_ Y /\ E.v e. G v C_ t)))
43	42	adantr 425	. . . . 5 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ A.x e. F E.y e. G y C_ x) -> (t e. (filGen` G) <-> (t C_ Y /\ E.v e. G v C_ t)))
44	36, 40, 43	3imtr4d 602	. . . 4 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ A.x e. F E.y e. G y C_ x) -> (t e. (filGen` F) -> t e. (filGen` G)))
45	44	ssrdv 2622	. . 3 |- (((F e. fBas /\ G e. fBas /\ X = Y) /\ A.x e. F E.y e. G y C_ x) -> (filGen` F) C_ (filGen` G))
46	45	ex 402	. 2 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> (A.x e. F E.y e. G y C_ x -> (filGen` F) C_ (filGen` G)))
47	13, 46	impbid 574	1 |- ((F e. fBas /\ G e. fBas /\ X = Y) -> ((filGen` F) C_ (filGen` G) <-> A.x e. F E.y e. G y C_ x))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106   C_ wss 2593  U.cuni 3177  ` cfv 3998  fBascfbas 10257  filGencfg 10258

This theorem is referenced by:  fbfgss2 14937

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-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-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-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  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-fv 4014  df-fg 10260

Copyright terms: Public domain