alexsublem

	Ref	Expression
Hypotheses	alexsub.1	$⊢ φ \to X \in UFL$
	alexsub.2	$⊢ φ \to X = ⋃ B$
	alexsub.3	$⊢ φ \to J = topGen (fi (B))$
	alexsub.4	$⊢ (φ \land (x \subseteq B \land X = ⋃ x)) \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y$
	alexsub.5	$⊢ φ \to F \in UFil (X)$
	alexsub.6	$⊢ φ \to J fLim F = \emptyset$
Assertion	alexsublem	$⊢ \neg φ$

Proof

Step	Hyp	Ref	Expression
1		alexsub.1	$⊢ φ \to X \in UFL$
2		alexsub.2	$⊢ φ \to X = ⋃ B$
3		alexsub.3	$⊢ φ \to J = topGen (fi (B))$
4		alexsub.4	$⊢ (φ \land (x \subseteq B \land X = ⋃ x)) \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y$
5		alexsub.5	$⊢ φ \to F \in UFil (X)$
6		alexsub.6	$⊢ φ \to J fLim F = \emptyset$
7		eldif	$⊢ x \in (X ∖ ⋃ (B ∖ F)) \leftrightarrow (x \in X \land \neg x \in ⋃ (B ∖ F))$
8	3	eleq2d	$⊢ φ \to (y \in J \leftrightarrow y \in topGen (fi (B)))$
9	8	anbi1d	$⊢ φ \to ((y \in J \land x \in y) \leftrightarrow (y \in topGen (fi (B)) \land x \in y))$
10	9	biimpa	$⊢ (φ \land (y \in J \land x \in y)) \to (y \in topGen (fi (B)) \land x \in y)$
11	10	adantlr	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \to (y \in topGen (fi (B)) \land x \in y)$
12		tg2	$⊢ (y \in topGen (fi (B)) \land x \in y) \to \exists z \in fi (B) (x \in z \land z \subseteq y)$
13	11 12	syl	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \to \exists z \in fi (B) (x \in z \land z \subseteq y)$
14		ufilfil	$⊢ F \in UFil (X) \to F \in Fil (X)$
15	5 14	syl	$⊢ φ \to F \in Fil (X)$
16	15	ad3antrrr	$⊢ (((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \land (z \in fi (B) \land (x \in z \land z \subseteq y))) \to F \in Fil (X)$
17	5	elfvexd	$⊢ φ \to X \in V$
18	2 17	eqeltrrd	$⊢ φ \to ⋃ B \in V$
19		uniexb	$⊢ B \in V \leftrightarrow ⋃ B \in V$
20	18 19	sylibr	$⊢ φ \to B \in V$
21		elfi2	$⊢ B \in V \to (z \in fi (B) \leftrightarrow \exists y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) z = ⋂ y)$
22	20 21	syl	$⊢ φ \to (z \in fi (B) \leftrightarrow \exists y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) z = ⋂ y)$
23	22	adantr	$⊢ (φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \to (z \in fi (B) \leftrightarrow \exists y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) z = ⋂ y)$
24	15	ad2antrr	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \to F \in Fil (X)$
25		simplrr	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y)) \to \neg x \in ⋃ (B ∖ F)$
26		intss1	$⊢ z \in y \to ⋂ y \subseteq z$
27	26	adantl	$⊢ ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y) \to ⋂ y \subseteq z$
28		simplr	$⊢ ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y) \to x \in ⋂ y$
29	27 28	sseldd	$⊢ ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y) \to x \in z$
30	29	ad2antlr	$⊢ (((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y)) \land \neg z \in F) \to x \in z$
31		eldifsn	$⊢ y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \leftrightarrow (y \in (𝒫 B \cap Fin) \land y \neq \emptyset)$
32	31	simplbi	$⊢ y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \to y \in (𝒫 B \cap Fin)$
33	32	ad2antrl	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \to y \in (𝒫 B \cap Fin)$
34		elfpw	$⊢ y \in (𝒫 B \cap Fin) \leftrightarrow (y \subseteq B \land y \in Fin)$
35	34	simplbi	$⊢ y \in (𝒫 B \cap Fin) \to y \subseteq B$
36	33 35	syl	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \to y \subseteq B$
37	36	sselda	$⊢ (((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \land z \in y) \to z \in B$
38	37	anasss	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y)) \to z \in B$
39	38	anim1i	$⊢ (((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y)) \land \neg z \in F) \to (z \in B \land \neg z \in F)$
40		eldif	$⊢ z \in (B ∖ F) \leftrightarrow (z \in B \land \neg z \in F)$
41	39 40	sylibr	$⊢ (((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y)) \land \neg z \in F) \to z \in (B ∖ F)$
42		elunii	$⊢ (x \in z \land z \in (B ∖ F)) \to x \in ⋃ (B ∖ F)$
43	30 41 42	syl2anc	$⊢ (((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y)) \land \neg z \in F) \to x \in ⋃ (B ∖ F)$
44	43	ex	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y)) \to (\neg z \in F \to x \in ⋃ (B ∖ F))$
45	25 44	mt3d	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land ((y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y) \land z \in y)) \to z \in F$
46	45	expr	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \to (z \in y \to z \in F)$
47	46	ssrdv	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \to y \subseteq F$
48		eldifsni	$⊢ y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \to y \neq \emptyset$
49	48	ad2antrl	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \to y \neq \emptyset$
50		elinel2	$⊢ y \in (𝒫 B \cap Fin) \to y \in Fin$
51	33 50	syl	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \to y \in Fin$
52		elfir	$⊢ (F \in Fil (X) \land (y \subseteq F \land y \neq \emptyset \land y \in Fin)) \to ⋂ y \in fi (F)$
53	24 47 49 51 52	syl13anc	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \to ⋂ y \in fi (F)$
54		filfi	$⊢ F \in Fil (X) \to fi (F) = F$
55	24 54	syl	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \to fi (F) = F$
56	53 55	eleqtrd	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) \land x \in ⋂ y)) \to ⋂ y \in F$
57	56	expr	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\})) \to (x \in ⋂ y \to ⋂ y \in F)$
58		eleq2	$⊢ z = ⋂ y \to (x \in z \leftrightarrow x \in ⋂ y)$
59		eleq1	$⊢ z = ⋂ y \to (z \in F \leftrightarrow ⋂ y \in F)$
60	58 59	imbi12d	$⊢ z = ⋂ y \to ((x \in z \to z \in F) \leftrightarrow (x \in ⋂ y \to ⋂ y \in F))$
61	57 60	syl5ibrcom	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\})) \to (z = ⋂ y \to (x \in z \to z \in F))$
62	61	rexlimdva	$⊢ (φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \to (\exists y \in ((𝒫 B \cap Fin) ∖ \{\emptyset\}) z = ⋂ y \to (x \in z \to z \in F))$
63	23 62	sylbid	$⊢ (φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \to (z \in fi (B) \to (x \in z \to z \in F))$
64	63	imp32	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (z \in fi (B) \land x \in z)) \to z \in F$
65	64	adantrrr	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (z \in fi (B) \land (x \in z \land z \subseteq y))) \to z \in F$
66	65	adantlr	$⊢ (((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \land (z \in fi (B) \land (x \in z \land z \subseteq y))) \to z \in F$
67		elssuni	$⊢ y \in J \to y \subseteq ⋃ J$
68	67	ad2antrl	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \to y \subseteq ⋃ J$
69		fibas	$⊢ fi (B) \in TopBases$
70		tgtopon	$⊢ fi (B) \in TopBases \to topGen (fi (B)) \in TopOn (⋃ fi (B))$
71	69 70	ax-mp	$⊢ topGen (fi (B)) \in TopOn (⋃ fi (B))$
72	3 71	eqeltrdi	$⊢ φ \to J \in TopOn (⋃ fi (B))$
73		fiuni	$⊢ B \in V \to ⋃ B = ⋃ fi (B)$
74	20 73	syl	$⊢ φ \to ⋃ B = ⋃ fi (B)$
75	2 74	eqtrd	$⊢ φ \to X = ⋃ fi (B)$
76	75	fveq2d	$⊢ φ \to TopOn (X) = TopOn (⋃ fi (B))$
77	72 76	eleqtrrd	$⊢ φ \to J \in TopOn (X)$
78		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
79	77 78	syl	$⊢ φ \to X = ⋃ J$
80	79	ad2antrr	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \to X = ⋃ J$
81	68 80	sseqtrrd	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \to y \subseteq X$
82	81	adantr	$⊢ (((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \land (z \in fi (B) \land (x \in z \land z \subseteq y))) \to y \subseteq X$
83		simprrr	$⊢ (((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \land (z \in fi (B) \land (x \in z \land z \subseteq y))) \to z \subseteq y$
84		filss	$⊢ (F \in Fil (X) \land (z \in F \land y \subseteq X \land z \subseteq y)) \to y \in F$
85	16 66 82 83 84	syl13anc	$⊢ (((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \land (z \in fi (B) \land (x \in z \land z \subseteq y))) \to y \in F$
86	13 85	rexlimddv	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land (y \in J \land x \in y)) \to y \in F$
87	86	expr	$⊢ ((φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \land y \in J) \to (x \in y \to y \in F)$
88	87	ralrimiva	$⊢ (φ \land (x \in X \land \neg x \in ⋃ (B ∖ F))) \to \forall y \in J (x \in y \to y \in F)$
89	88	expr	$⊢ (φ \land x \in X) \to (\neg x \in ⋃ (B ∖ F) \to \forall y \in J (x \in y \to y \in F))$
90	89	imdistanda	$⊢ φ \to ((x \in X \land \neg x \in ⋃ (B ∖ F)) \to (x \in X \land \forall y \in J (x \in y \to y \in F)))$
91	7 90	biimtrid	$⊢ φ \to (x \in (X ∖ ⋃ (B ∖ F)) \to (x \in X \land \forall y \in J (x \in y \to y \in F)))$
92		flimopn	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (x \in (J fLim F) \leftrightarrow (x \in X \land \forall y \in J (x \in y \to y \in F)))$
93	77 15 92	syl2anc	$⊢ φ \to (x \in (J fLim F) \leftrightarrow (x \in X \land \forall y \in J (x \in y \to y \in F)))$
94	91 93	sylibrd	$⊢ φ \to (x \in (X ∖ ⋃ (B ∖ F)) \to x \in (J fLim F))$
95	94	ssrdv	$⊢ φ \to X ∖ ⋃ (B ∖ F) \subseteq J fLim F$
96		sseq0	$⊢ (X ∖ ⋃ (B ∖ F) \subseteq J fLim F \land J fLim F = \emptyset) \to X ∖ ⋃ (B ∖ F) = \emptyset$
97	95 6 96	syl2anc	$⊢ φ \to X ∖ ⋃ (B ∖ F) = \emptyset$
98		ssdif0	$⊢ X \subseteq ⋃ (B ∖ F) \leftrightarrow X ∖ ⋃ (B ∖ F) = \emptyset$
99	97 98	sylibr	$⊢ φ \to X \subseteq ⋃ (B ∖ F)$
100		difss	$⊢ B ∖ F \subseteq B$
101	100	unissi	$⊢ ⋃ (B ∖ F) \subseteq ⋃ B$
102	101 2	sseqtrrid	$⊢ φ \to ⋃ (B ∖ F) \subseteq X$
103	99 102	eqssd	$⊢ φ \to X = ⋃ (B ∖ F)$
104	103 100	jctil	$⊢ φ \to (B ∖ F \subseteq B \land X = ⋃ (B ∖ F))$
105	20	difexd	$⊢ φ \to B ∖ F \in V$
106	105	adantr	$⊢ (φ \land (B ∖ F \subseteq B \land X = ⋃ (B ∖ F))) \to B ∖ F \in V$
107		sseq1	$⊢ x = B ∖ F \to (x \subseteq B \leftrightarrow B ∖ F \subseteq B)$
108		unieq	$⊢ x = B ∖ F \to ⋃ x = ⋃ (B ∖ F)$
109	108	eqeq2d	$⊢ x = B ∖ F \to (X = ⋃ x \leftrightarrow X = ⋃ (B ∖ F))$
110	107 109	anbi12d	$⊢ x = B ∖ F \to ((x \subseteq B \land X = ⋃ x) \leftrightarrow (B ∖ F \subseteq B \land X = ⋃ (B ∖ F)))$
111	110	anbi2d	$⊢ x = B ∖ F \to ((φ \land (x \subseteq B \land X = ⋃ x)) \leftrightarrow (φ \land (B ∖ F \subseteq B \land X = ⋃ (B ∖ F))))$
112		pweq	$⊢ x = B ∖ F \to 𝒫 x = 𝒫 (B ∖ F)$
113	112	ineq1d	$⊢ x = B ∖ F \to 𝒫 x \cap Fin = 𝒫 (B ∖ F) \cap Fin$
114	113	rexeqdv	$⊢ x = B ∖ F \to (\exists y \in (𝒫 x \cap Fin) X = ⋃ y \leftrightarrow \exists y \in (𝒫 (B ∖ F) \cap Fin) X = ⋃ y)$
115	111 114	imbi12d	$⊢ x = B ∖ F \to (((φ \land (x \subseteq B \land X = ⋃ x)) \to \exists y \in (𝒫 x \cap Fin) X = ⋃ y) \leftrightarrow ((φ \land (B ∖ F \subseteq B \land X = ⋃ (B ∖ F))) \to \exists y \in (𝒫 (B ∖ F) \cap Fin) X = ⋃ y))$
116	115 4	vtoclg	$⊢ B ∖ F \in V \to ((φ \land (B ∖ F \subseteq B \land X = ⋃ (B ∖ F))) \to \exists y \in (𝒫 (B ∖ F) \cap Fin) X = ⋃ y)$
117	106 116	mpcom	$⊢ (φ \land (B ∖ F \subseteq B \land X = ⋃ (B ∖ F))) \to \exists y \in (𝒫 (B ∖ F) \cap Fin) X = ⋃ y$
118	104 117	mpdan	$⊢ φ \to \exists y \in (𝒫 (B ∖ F) \cap Fin) X = ⋃ y$
119		unieq	$⊢ y = \emptyset \to ⋃ y = ⋃ \emptyset$
120		uni0	$⊢ ⋃ \emptyset = \emptyset$
121	119 120	eqtrdi	$⊢ y = \emptyset \to ⋃ y = \emptyset$
122	121	neeq2d	$⊢ y = \emptyset \to (X \neq ⋃ y \leftrightarrow X \neq \emptyset)$
123		difssd	$⊢ (φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \to X ∖ z \subseteq X$
124	123	ralrimivw	$⊢ (φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \to \forall z \in y X ∖ z \subseteq X$
125		riinn0	$⊢ (\forall z \in y X ∖ z \subseteq X \land y \neq \emptyset) \to X \cap ⋂_{z \in y} (X ∖ z) = ⋂_{z \in y} (X ∖ z)$
126	124 125	sylan	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to X \cap ⋂_{z \in y} (X ∖ z) = ⋂_{z \in y} (X ∖ z)$
127	17	ad2antrr	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to X \in V$
128	127	difexd	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to X ∖ z \in V$
129	128	ralrimivw	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to \forall z \in y X ∖ z \in V$
130		dfiin2g	$⊢ \forall z \in y X ∖ z \in V \to ⋂_{z \in y} (X ∖ z) = ⋂ \{x \| \exists z \in y x = X ∖ z\}$
131	129 130	syl	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to ⋂_{z \in y} (X ∖ z) = ⋂ \{x \| \exists z \in y x = X ∖ z\}$
132		eqid	$⊢ (z \in y ⟼ X ∖ z) = (z \in y ⟼ X ∖ z)$
133	132	rnmpt	$⊢ ran (z \in y ⟼ X ∖ z) = \{x \| \exists z \in y x = X ∖ z\}$
134	133	inteqi	$⊢ ⋂ ran (z \in y ⟼ X ∖ z) = ⋂ \{x \| \exists z \in y x = X ∖ z\}$
135	131 134	eqtr4di	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to ⋂_{z \in y} (X ∖ z) = ⋂ ran (z \in y ⟼ X ∖ z)$
136	126 135	eqtrd	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to X \cap ⋂_{z \in y} (X ∖ z) = ⋂ ran (z \in y ⟼ X ∖ z)$
137	15	ad2antrr	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to F \in Fil (X)$
138		elfpw	$⊢ y \in (𝒫 (B ∖ F) \cap Fin) \leftrightarrow (y \subseteq B ∖ F \land y \in Fin)$
139	138	simplbi	$⊢ y \in (𝒫 (B ∖ F) \cap Fin) \to y \subseteq B ∖ F$
140	139	ad2antlr	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to y \subseteq B ∖ F$
141	140	sselda	$⊢ (((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \land z \in y) \to z \in (B ∖ F)$
142	141	eldifbd	$⊢ (((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \land z \in y) \to \neg z \in F$
143	5	ad3antrrr	$⊢ (((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \land z \in y) \to F \in UFil (X)$
144	140	difss2d	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to y \subseteq B$
145	144	sselda	$⊢ (((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \land z \in y) \to z \in B$
146		elssuni	$⊢ z \in B \to z \subseteq ⋃ B$
147	145 146	syl	$⊢ (((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \land z \in y) \to z \subseteq ⋃ B$
148	2	ad3antrrr	$⊢ (((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \land z \in y) \to X = ⋃ B$
149	147 148	sseqtrrd	$⊢ (((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \land z \in y) \to z \subseteq X$
150		ufilb	$⊢ (F \in UFil (X) \land z \subseteq X) \to (\neg z \in F \leftrightarrow X ∖ z \in F)$
151	143 149 150	syl2anc	$⊢ (((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \land z \in y) \to (\neg z \in F \leftrightarrow X ∖ z \in F)$
152	142 151	mpbid	$⊢ (((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \land z \in y) \to X ∖ z \in F$
153	152	fmpttd	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to (z \in y ⟼ X ∖ z) : y ⟶ F$
154	153	frnd	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to ran (z \in y ⟼ X ∖ z) \subseteq F$
155	132 152	dmmptd	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to dom (z \in y ⟼ X ∖ z) = y$
156		simpr	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to y \neq \emptyset$
157	155 156	eqnetrd	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to dom (z \in y ⟼ X ∖ z) \neq \emptyset$
158		dm0rn0	$⊢ dom (z \in y ⟼ X ∖ z) = \emptyset \leftrightarrow ran (z \in y ⟼ X ∖ z) = \emptyset$
159	158	necon3bii	$⊢ dom (z \in y ⟼ X ∖ z) \neq \emptyset \leftrightarrow ran (z \in y ⟼ X ∖ z) \neq \emptyset$
160	157 159	sylib	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to ran (z \in y ⟼ X ∖ z) \neq \emptyset$
161		elinel2	$⊢ y \in (𝒫 (B ∖ F) \cap Fin) \to y \in Fin$
162	161	ad2antlr	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to y \in Fin$
163		abrexfi	$⊢ y \in Fin \to \{x \| \exists z \in y x = X ∖ z\} \in Fin$
164	133 163	eqeltrid	$⊢ y \in Fin \to ran (z \in y ⟼ X ∖ z) \in Fin$
165	162 164	syl	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to ran (z \in y ⟼ X ∖ z) \in Fin$
166		filintn0	$⊢ (F \in Fil (X) \land (ran (z \in y ⟼ X ∖ z) \subseteq F \land ran (z \in y ⟼ X ∖ z) \neq \emptyset \land ran (z \in y ⟼ X ∖ z) \in Fin)) \to ⋂ ran (z \in y ⟼ X ∖ z) \neq \emptyset$
167	137 154 160 165 166	syl13anc	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to ⋂ ran (z \in y ⟼ X ∖ z) \neq \emptyset$
168	136 167	eqnetrd	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to X \cap ⋂_{z \in y} (X ∖ z) \neq \emptyset$
169		disj3	$⊢ X \cap ⋂_{z \in y} (X ∖ z) = \emptyset \leftrightarrow X = X ∖ ⋂_{z \in y} (X ∖ z)$
170	169	necon3bii	$⊢ X \cap ⋂_{z \in y} (X ∖ z) \neq \emptyset \leftrightarrow X \neq X ∖ ⋂_{z \in y} (X ∖ z)$
171	168 170	sylib	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to X \neq X ∖ ⋂_{z \in y} (X ∖ z)$
172		iundif2	$⊢ ⋃_{z \in y} (X ∖ (X ∖ z)) = X ∖ ⋂_{z \in y} (X ∖ z)$
173		dfss4	$⊢ z \subseteq X \leftrightarrow X ∖ (X ∖ z) = z$
174	149 173	sylib	$⊢ (((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \land z \in y) \to X ∖ (X ∖ z) = z$
175	174	iuneq2dv	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to ⋃_{z \in y} (X ∖ (X ∖ z)) = ⋃_{z \in y} z$
176		uniiun	$⊢ ⋃ y = ⋃_{z \in y} z$
177	175 176	eqtr4di	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to ⋃_{z \in y} (X ∖ (X ∖ z)) = ⋃ y$
178	172 177	eqtr3id	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to X ∖ ⋂_{z \in y} (X ∖ z) = ⋃ y$
179	171 178	neeqtrd	$⊢ ((φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \land y \neq \emptyset) \to X \neq ⋃ y$
180	15	adantr	$⊢ (φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \to F \in Fil (X)$
181		filtop	$⊢ F \in Fil (X) \to X \in F$
182		fileln0	$⊢ (F \in Fil (X) \land X \in F) \to X \neq \emptyset$
183	180 181 182	syl2anc2	$⊢ (φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \to X \neq \emptyset$
184	122 179 183	pm2.61ne	$⊢ (φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \to X \neq ⋃ y$
185	184	neneqd	$⊢ (φ \land y \in (𝒫 (B ∖ F) \cap Fin)) \to \neg X = ⋃ y$
186	185	nrexdv	$⊢ φ \to \neg \exists y \in (𝒫 (B ∖ F) \cap Fin) X = ⋃ y$
187	118 186	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem alexsublem

Proof