trfbas2

Description: Conditions for the trace of a filter base F to be a filter base. (Contributed by Mario Carneiro, 13-Oct-2015)

		Ref	Expression
	Assertion	trfbas2	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to (F ↾_{𝑡} A \in fBas (A) \leftrightarrow \neg \emptyset \in (F ↾_{𝑡} A))$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ F \in fBas (Y) \to Y \in dom fBas$
2		ssexg	$⊢ (A \subseteq Y \land Y \in dom fBas) \to A \in V$
3	2	ancoms	$⊢ (Y \in dom fBas \land A \subseteq Y) \to A \in V$
4	1 3	sylan	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to A \in V$
5		restsspw	$⊢ F ↾_{𝑡} A \subseteq 𝒫 A$
6	5	a1i	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to F ↾_{𝑡} A \subseteq 𝒫 A$
7		fbasne0	$⊢ F \in fBas (Y) \to F \neq \emptyset$
8	7	adantr	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to F \neq \emptyset$
9		n0	$⊢ F \neq \emptyset \leftrightarrow \exists x x \in F$
10	8 9	sylib	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to \exists x x \in F$
11		elrestr	$⊢ (F \in fBas (Y) \land A \in V \land x \in F) \to x \cap A \in (F ↾_{𝑡} A)$
12	11	3expia	$⊢ (F \in fBas (Y) \land A \in V) \to (x \in F \to x \cap A \in (F ↾_{𝑡} A))$
13	4 12	syldan	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to (x \in F \to x \cap A \in (F ↾_{𝑡} A))$
14		ne0i	$⊢ x \cap A \in (F ↾_{𝑡} A) \to F ↾_{𝑡} A \neq \emptyset$
15	13 14	syl6	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to (x \in F \to F ↾_{𝑡} A \neq \emptyset)$
16	15	exlimdv	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to (\exists x x \in F \to F ↾_{𝑡} A \neq \emptyset)$
17	10 16	mpd	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to F ↾_{𝑡} A \neq \emptyset$
18		fbasssin	$⊢ (F \in fBas (Y) \land z \in F \land w \in F) \to \exists x \in F x \subseteq z \cap w$
19	18	3expb	$⊢ (F \in fBas (Y) \land (z \in F \land w \in F)) \to \exists x \in F x \subseteq z \cap w$
20	19	adantlr	$⊢ ((F \in fBas (Y) \land A \subseteq Y) \land (z \in F \land w \in F)) \to \exists x \in F x \subseteq z \cap w$
21		simplll	$⊢ (((F \in fBas (Y) \land A \subseteq Y) \land (z \in F \land w \in F)) \land (x \in F \land x \subseteq z \cap w)) \to F \in fBas (Y)$
22	4	ad2antrr	$⊢ (((F \in fBas (Y) \land A \subseteq Y) \land (z \in F \land w \in F)) \land (x \in F \land x \subseteq z \cap w)) \to A \in V$
23		simprl	$⊢ (((F \in fBas (Y) \land A \subseteq Y) \land (z \in F \land w \in F)) \land (x \in F \land x \subseteq z \cap w)) \to x \in F$
24	21 22 23 11	syl3anc	$⊢ (((F \in fBas (Y) \land A \subseteq Y) \land (z \in F \land w \in F)) \land (x \in F \land x \subseteq z \cap w)) \to x \cap A \in (F ↾_{𝑡} A)$
25		ssrin	$⊢ x \subseteq z \cap w \to x \cap A \subseteq (z \cap w) \cap A$
26	25	ad2antll	$⊢ (((F \in fBas (Y) \land A \subseteq Y) \land (z \in F \land w \in F)) \land (x \in F \land x \subseteq z \cap w)) \to x \cap A \subseteq (z \cap w) \cap A$
27		vex	$⊢ x \in V$
28	27	inex1	$⊢ x \cap A \in V$
29	28	elpw	$⊢ x \cap A \in 𝒫 ((z \cap w) \cap A) \leftrightarrow x \cap A \subseteq (z \cap w) \cap A$
30	26 29	sylibr	$⊢ (((F \in fBas (Y) \land A \subseteq Y) \land (z \in F \land w \in F)) \land (x \in F \land x \subseteq z \cap w)) \to x \cap A \in 𝒫 ((z \cap w) \cap A)$
31		inelcm	$⊢ (x \cap A \in (F ↾_{𝑡} A) \land x \cap A \in 𝒫 ((z \cap w) \cap A)) \to (F ↾_{𝑡} A) \cap 𝒫 ((z \cap w) \cap A) \neq \emptyset$
32	24 30 31	syl2anc	$⊢ (((F \in fBas (Y) \land A \subseteq Y) \land (z \in F \land w \in F)) \land (x \in F \land x \subseteq z \cap w)) \to (F ↾_{𝑡} A) \cap 𝒫 ((z \cap w) \cap A) \neq \emptyset$
33	20 32	rexlimddv	$⊢ ((F \in fBas (Y) \land A \subseteq Y) \land (z \in F \land w \in F)) \to (F ↾_{𝑡} A) \cap 𝒫 ((z \cap w) \cap A) \neq \emptyset$
34	33	ralrimivva	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to \forall z \in F \forall w \in F (F ↾_{𝑡} A) \cap 𝒫 ((z \cap w) \cap A) \neq \emptyset$
35		vex	$⊢ z \in V$
36	35	inex1	$⊢ z \cap A \in V$
37	36	a1i	$⊢ ((F \in fBas (Y) \land A \subseteq Y) \land z \in F) \to z \cap A \in V$
38		elrest	$⊢ (F \in fBas (Y) \land A \in V) \to (x \in (F ↾_{𝑡} A) \leftrightarrow \exists z \in F x = z \cap A)$
39	4 38	syldan	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to (x \in (F ↾_{𝑡} A) \leftrightarrow \exists z \in F x = z \cap A)$
40		vex	$⊢ w \in V$
41	40	inex1	$⊢ w \cap A \in V$
42	41	a1i	$⊢ (((F \in fBas (Y) \land A \subseteq Y) \land x = z \cap A) \land w \in F) \to w \cap A \in V$
43		elrest	$⊢ (F \in fBas (Y) \land A \in V) \to (y \in (F ↾_{𝑡} A) \leftrightarrow \exists w \in F y = w \cap A)$
44	4 43	syldan	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to (y \in (F ↾_{𝑡} A) \leftrightarrow \exists w \in F y = w \cap A)$
45	44	adantr	$⊢ ((F \in fBas (Y) \land A \subseteq Y) \land x = z \cap A) \to (y \in (F ↾_{𝑡} A) \leftrightarrow \exists w \in F y = w \cap A)$
46		ineq12	$⊢ (x = z \cap A \land y = w \cap A) \to x \cap y = (z \cap A) \cap (w \cap A)$
47		inindir	$⊢ (z \cap w) \cap A = (z \cap A) \cap (w \cap A)$
48	46 47	eqtr4di	$⊢ (x = z \cap A \land y = w \cap A) \to x \cap y = (z \cap w) \cap A$
49	48	pweqd	$⊢ (x = z \cap A \land y = w \cap A) \to 𝒫 (x \cap y) = 𝒫 ((z \cap w) \cap A)$
50	49	ineq2d	$⊢ (x = z \cap A \land y = w \cap A) \to (F ↾_{𝑡} A) \cap 𝒫 (x \cap y) = (F ↾_{𝑡} A) \cap 𝒫 ((z \cap w) \cap A)$
51	50	neeq1d	$⊢ (x = z \cap A \land y = w \cap A) \to ((F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow (F ↾_{𝑡} A) \cap 𝒫 ((z \cap w) \cap A) \neq \emptyset)$
52	51	adantll	$⊢ (((F \in fBas (Y) \land A \subseteq Y) \land x = z \cap A) \land y = w \cap A) \to ((F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow (F ↾_{𝑡} A) \cap 𝒫 ((z \cap w) \cap A) \neq \emptyset)$
53	42 45 52	ralxfr2d	$⊢ ((F \in fBas (Y) \land A \subseteq Y) \land x = z \cap A) \to (\forall y \in (F ↾_{𝑡} A) (F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow \forall w \in F (F ↾_{𝑡} A) \cap 𝒫 ((z \cap w) \cap A) \neq \emptyset)$
54	37 39 53	ralxfr2d	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to (\forall x \in (F ↾_{𝑡} A) \forall y \in (F ↾_{𝑡} A) (F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow \forall z \in F \forall w \in F (F ↾_{𝑡} A) \cap 𝒫 ((z \cap w) \cap A) \neq \emptyset)$
55	34 54	mpbird	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to \forall x \in (F ↾_{𝑡} A) \forall y \in (F ↾_{𝑡} A) (F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset$
56		isfbas	$⊢ A \in V \to (F ↾_{𝑡} A \in fBas (A) \leftrightarrow (F ↾_{𝑡} A \subseteq 𝒫 A \land (F ↾_{𝑡} A \neq \emptyset \land \emptyset \notin (F ↾_{𝑡} A) \land \forall x \in (F ↾_{𝑡} A) \forall y \in (F ↾_{𝑡} A) (F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset)))$
57	56	baibd	$⊢ (A \in V \land F ↾_{𝑡} A \subseteq 𝒫 A) \to (F ↾_{𝑡} A \in fBas (A) \leftrightarrow (F ↾_{𝑡} A \neq \emptyset \land \emptyset \notin (F ↾_{𝑡} A) \land \forall x \in (F ↾_{𝑡} A) \forall y \in (F ↾_{𝑡} A) (F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset))$
58		3anan32	$⊢ (F ↾_{𝑡} A \neq \emptyset \land \emptyset \notin (F ↾_{𝑡} A) \land \forall x \in (F ↾_{𝑡} A) \forall y \in (F ↾_{𝑡} A) (F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset) \leftrightarrow ((F ↾_{𝑡} A \neq \emptyset \land \forall x \in (F ↾_{𝑡} A) \forall y \in (F ↾_{𝑡} A) (F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset) \land \emptyset \notin (F ↾_{𝑡} A))$
59	57 58	bitrdi	$⊢ (A \in V \land F ↾_{𝑡} A \subseteq 𝒫 A) \to (F ↾_{𝑡} A \in fBas (A) \leftrightarrow ((F ↾_{𝑡} A \neq \emptyset \land \forall x \in (F ↾_{𝑡} A) \forall y \in (F ↾_{𝑡} A) (F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset) \land \emptyset \notin (F ↾_{𝑡} A)))$
60	59	baibd	$⊢ ((A \in V \land F ↾_{𝑡} A \subseteq 𝒫 A) \land (F ↾_{𝑡} A \neq \emptyset \land \forall x \in (F ↾_{𝑡} A) \forall y \in (F ↾_{𝑡} A) (F ↾_{𝑡} A) \cap 𝒫 (x \cap y) \neq \emptyset)) \to (F ↾_{𝑡} A \in fBas (A) \leftrightarrow \emptyset \notin (F ↾_{𝑡} A))$
61	4 6 17 55 60	syl22anc	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to (F ↾_{𝑡} A \in fBas (A) \leftrightarrow \emptyset \notin (F ↾_{𝑡} A))$
62		df-nel	$⊢ \emptyset \notin (F ↾_{𝑡} A) \leftrightarrow \neg \emptyset \in (F ↾_{𝑡} A)$
63	61 62	bitrdi	$⊢ (F \in fBas (Y) \land A \subseteq Y) \to (F ↾_{𝑡} A \in fBas (A) \leftrightarrow \neg \emptyset \in (F ↾_{𝑡} A))$

Metamath Proof Explorer

Theorem trfbas2

Proof