hauscmplem

	Ref	Expression
Hypotheses	hauscmp.1	$⊢ X = ⋃ J$
	hauscmplem.2	$⊢ O = \{y \in J \| \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y)\}$
	hauscmplem.3	$⊢ φ \to J \in Haus$
	hauscmplem.4	$⊢ φ \to S \subseteq X$
	hauscmplem.5	$⊢ φ \to J ↾_{𝑡} S \in Comp$
	hauscmplem.6	$⊢ φ \to A \in (X ∖ S)$
Assertion	hauscmplem	$⊢ φ \to \exists z \in J (A \in z \land cls (J) (z) \subseteq X ∖ S)$

Proof

Step	Hyp	Ref	Expression
1		hauscmp.1	$⊢ X = ⋃ J$
2		hauscmplem.2	$⊢ O = \{y \in J \| \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y)\}$
3		hauscmplem.3	$⊢ φ \to J \in Haus$
4		hauscmplem.4	$⊢ φ \to S \subseteq X$
5		hauscmplem.5	$⊢ φ \to J ↾_{𝑡} S \in Comp$
6		hauscmplem.6	$⊢ φ \to A \in (X ∖ S)$
7		haustop	$⊢ J \in Haus \to J \in Top$
8	3 7	syl	$⊢ φ \to J \in Top$
9	8	ad3antrrr	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to J \in Top$
10	1	topopn	$⊢ J \in Top \to X \in J$
11	9 10	syl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to X \in J$
12	6	eldifad	$⊢ φ \to A \in X$
13	12	ad3antrrr	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to A \in X$
14	1	clstop	$⊢ J \in Top \to cls (J) (X) = X$
15	9 14	syl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to cls (J) (X) = X$
16		simplr	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to S \subseteq ⋃ x$
17		unieq	$⊢ x = \emptyset \to ⋃ x = ⋃ \emptyset$
18		uni0	$⊢ ⋃ \emptyset = \emptyset$
19	17 18	eqtrdi	$⊢ x = \emptyset \to ⋃ x = \emptyset$
20	19	adantl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to ⋃ x = \emptyset$
21	16 20	sseqtrd	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to S \subseteq \emptyset$
22		ss0	$⊢ S \subseteq \emptyset \to S = \emptyset$
23	21 22	syl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to S = \emptyset$
24	23	difeq2d	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to X ∖ S = X ∖ \emptyset$
25		dif0	$⊢ X ∖ \emptyset = X$
26	24 25	eqtrdi	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to X ∖ S = X$
27	15 26	eqtr4d	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to cls (J) (X) = X ∖ S$
28		eqimss	$⊢ cls (J) (X) = X ∖ S \to cls (J) (X) \subseteq X ∖ S$
29	27 28	syl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to cls (J) (X) \subseteq X ∖ S$
30		eleq2	$⊢ z = X \to (A \in z \leftrightarrow A \in X)$
31		fveq2	$⊢ z = X \to cls (J) (z) = cls (J) (X)$
32	31	sseq1d	$⊢ z = X \to (cls (J) (z) \subseteq X ∖ S \leftrightarrow cls (J) (X) \subseteq X ∖ S)$
33	30 32	anbi12d	$⊢ z = X \to ((A \in z \land cls (J) (z) \subseteq X ∖ S) \leftrightarrow (A \in X \land cls (J) (X) \subseteq X ∖ S))$
34	33	rspcev	$⊢ (X \in J \land (A \in X \land cls (J) (X) \subseteq X ∖ S)) \to \exists z \in J (A \in z \land cls (J) (z) \subseteq X ∖ S)$
35	11 13 29 34	syl12anc	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x = \emptyset) \to \exists z \in J (A \in z \land cls (J) (z) \subseteq X ∖ S)$
36		elin	$⊢ x \in (𝒫 O \cap Fin) \leftrightarrow (x \in 𝒫 O \land x \in Fin)$
37		id	$⊢ x \in Fin \to x \in Fin$
38		elpwi	$⊢ x \in 𝒫 O \to x \subseteq O$
39	38	sseld	$⊢ x \in 𝒫 O \to (z \in x \to z \in O)$
40		difeq2	$⊢ y = z \to X ∖ y = X ∖ z$
41	40	sseq2d	$⊢ y = z \to (cls (J) (w) \subseteq X ∖ y \leftrightarrow cls (J) (w) \subseteq X ∖ z)$
42	41	anbi2d	$⊢ y = z \to ((A \in w \land cls (J) (w) \subseteq X ∖ y) \leftrightarrow (A \in w \land cls (J) (w) \subseteq X ∖ z))$
43	42	rexbidv	$⊢ y = z \to (\exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y) \leftrightarrow \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ z))$
44	43 2	elrab2	$⊢ z \in O \leftrightarrow (z \in J \land \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ z))$
45	44	simprbi	$⊢ z \in O \to \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ z)$
46	39 45	syl6	$⊢ x \in 𝒫 O \to (z \in x \to \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ z))$
47	46	ralrimiv	$⊢ x \in 𝒫 O \to \forall z \in x \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ z)$
48		eleq2	$⊢ w = f (z) \to (A \in w \leftrightarrow A \in f (z))$
49		fveq2	$⊢ w = f (z) \to cls (J) (w) = cls (J) (f (z))$
50	49	sseq1d	$⊢ w = f (z) \to (cls (J) (w) \subseteq X ∖ z \leftrightarrow cls (J) (f (z)) \subseteq X ∖ z)$
51	48 50	anbi12d	$⊢ w = f (z) \to ((A \in w \land cls (J) (w) \subseteq X ∖ z) \leftrightarrow (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))$
52	51	ac6sfi	$⊢ (x \in Fin \land \forall z \in x \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ z)) \to \exists f (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))$
53	37 47 52	syl2anr	$⊢ (x \in 𝒫 O \land x \in Fin) \to \exists f (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))$
54	36 53	sylbi	$⊢ x \in (𝒫 O \cap Fin) \to \exists f (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))$
55	54	ad2antlr	$⊢ ((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \to \exists f (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))$
56	8	ad3antrrr	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to J \in Top$
57		frn	$⊢ f : x ⟶ J \to ran f \subseteq J$
58	57	ad2antrl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ran f \subseteq J$
59		simprr	$⊢ ((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \to x \neq \emptyset$
60		simpl	$⊢ (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z)) \to f : x ⟶ J$
61		fdm	$⊢ f : x ⟶ J \to dom f = x$
62	61	eqeq1d	$⊢ f : x ⟶ J \to (dom f = \emptyset \leftrightarrow x = \emptyset)$
63		dm0rn0	$⊢ dom f = \emptyset \leftrightarrow ran f = \emptyset$
64	62 63	bitr3di	$⊢ f : x ⟶ J \to (x = \emptyset \leftrightarrow ran f = \emptyset)$
65	64	necon3bid	$⊢ f : x ⟶ J \to (x \neq \emptyset \leftrightarrow ran f \neq \emptyset)$
66	65	biimpac	$⊢ (x \neq \emptyset \land f : x ⟶ J) \to ran f \neq \emptyset$
67	59 60 66	syl2an	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ran f \neq \emptyset$
68	36	simprbi	$⊢ x \in (𝒫 O \cap Fin) \to x \in Fin$
69	68	ad2antlr	$⊢ ((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \to x \in Fin$
70		ffn	$⊢ f : x ⟶ J \to f Fn x$
71		dffn4	$⊢ f Fn x \leftrightarrow f : x \underset{onto}{⟶} ran f$
72	70 71	sylib	$⊢ f : x ⟶ J \to f : x \underset{onto}{⟶} ran f$
73	72	adantr	$⊢ (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z)) \to f : x \underset{onto}{⟶} ran f$
74		fofi	$⊢ (x \in Fin \land f : x \underset{onto}{⟶} ran f) \to ran f \in Fin$
75	69 73 74	syl2an	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ran f \in Fin$
76		fiinopn	$⊢ J \in Top \to ((ran f \subseteq J \land ran f \neq \emptyset \land ran f \in Fin) \to ⋂ ran f \in J)$
77	76	imp	$⊢ (J \in Top \land (ran f \subseteq J \land ran f \neq \emptyset \land ran f \in Fin)) \to ⋂ ran f \in J$
78	56 58 67 75 77	syl13anc	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ⋂ ran f \in J$
79		simpl	$⊢ (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z) \to A \in f (z)$
80	79	ralimi	$⊢ \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z) \to \forall z \in x A \in f (z)$
81	80	ad2antll	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to \forall z \in x A \in f (z)$
82	6	ad3antrrr	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to A \in (X ∖ S)$
83		eliin	$⊢ A \in (X ∖ S) \to (A \in ⋂_{z \in x} f (z) \leftrightarrow \forall z \in x A \in f (z))$
84	82 83	syl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to (A \in ⋂_{z \in x} f (z) \leftrightarrow \forall z \in x A \in f (z))$
85	81 84	mpbird	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to A \in ⋂_{z \in x} f (z)$
86	70	ad2antrl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to f Fn x$
87		fnrnfv	$⊢ f Fn x \to ran f = \{y \| \exists z \in x y = f (z)\}$
88	87	inteqd	$⊢ f Fn x \to ⋂ ran f = ⋂ \{y \| \exists z \in x y = f (z)\}$
89		fvex	$⊢ f (z) \in V$
90	89	dfiin2	$⊢ ⋂_{z \in x} f (z) = ⋂ \{y \| \exists z \in x y = f (z)\}$
91	88 90	eqtr4di	$⊢ f Fn x \to ⋂ ran f = ⋂_{z \in x} f (z)$
92	86 91	syl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ⋂ ran f = ⋂_{z \in x} f (z)$
93	85 92	eleqtrrd	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to A \in ⋂ ran f$
94	59	adantr	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to x \neq \emptyset$
95	8	ad4antr	$⊢ ((((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land f : x ⟶ J) \land z \in x) \to J \in Top$
96		ffvelcdm	$⊢ (f : x ⟶ J \land z \in x) \to f (z) \in J$
97	96	adantll	$⊢ ((((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land f : x ⟶ J) \land z \in x) \to f (z) \in J$
98		elssuni	$⊢ f (z) \in J \to f (z) \subseteq ⋃ J$
99	97 98	syl	$⊢ ((((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land f : x ⟶ J) \land z \in x) \to f (z) \subseteq ⋃ J$
100	99 1	sseqtrrdi	$⊢ ((((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land f : x ⟶ J) \land z \in x) \to f (z) \subseteq X$
101	1	clscld	$⊢ (J \in Top \land f (z) \subseteq X) \to cls (J) (f (z)) \in Clsd (J)$
102	95 100 101	syl2anc	$⊢ ((((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land f : x ⟶ J) \land z \in x) \to cls (J) (f (z)) \in Clsd (J)$
103	102	ralrimiva	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land f : x ⟶ J) \to \forall z \in x cls (J) (f (z)) \in Clsd (J)$
104	103	adantrr	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to \forall z \in x cls (J) (f (z)) \in Clsd (J)$
105		iincld	$⊢ (x \neq \emptyset \land \forall z \in x cls (J) (f (z)) \in Clsd (J)) \to ⋂_{z \in x} cls (J) (f (z)) \in Clsd (J)$
106	94 104 105	syl2anc	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ⋂_{z \in x} cls (J) (f (z)) \in Clsd (J)$
107	1	sscls	$⊢ (J \in Top \land f (z) \subseteq X) \to f (z) \subseteq cls (J) (f (z))$
108	95 100 107	syl2anc	$⊢ ((((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land f : x ⟶ J) \land z \in x) \to f (z) \subseteq cls (J) (f (z))$
109	108	ralrimiva	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land f : x ⟶ J) \to \forall z \in x f (z) \subseteq cls (J) (f (z))$
110		ssel	$⊢ f (z) \subseteq cls (J) (f (z)) \to (y \in f (z) \to y \in cls (J) (f (z)))$
111	110	ral2imi	$⊢ \forall z \in x f (z) \subseteq cls (J) (f (z)) \to (\forall z \in x y \in f (z) \to \forall z \in x y \in cls (J) (f (z)))$
112		eliin	$⊢ y \in V \to (y \in ⋂_{z \in x} f (z) \leftrightarrow \forall z \in x y \in f (z))$
113	112	elv	$⊢ y \in ⋂_{z \in x} f (z) \leftrightarrow \forall z \in x y \in f (z)$
114		eliin	$⊢ y \in V \to (y \in ⋂_{z \in x} cls (J) (f (z)) \leftrightarrow \forall z \in x y \in cls (J) (f (z)))$
115	114	elv	$⊢ y \in ⋂_{z \in x} cls (J) (f (z)) \leftrightarrow \forall z \in x y \in cls (J) (f (z))$
116	111 113 115	3imtr4g	$⊢ \forall z \in x f (z) \subseteq cls (J) (f (z)) \to (y \in ⋂_{z \in x} f (z) \to y \in ⋂_{z \in x} cls (J) (f (z)))$
117	116	ssrdv	$⊢ \forall z \in x f (z) \subseteq cls (J) (f (z)) \to ⋂_{z \in x} f (z) \subseteq ⋂_{z \in x} cls (J) (f (z))$
118	109 117	syl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land f : x ⟶ J) \to ⋂_{z \in x} f (z) \subseteq ⋂_{z \in x} cls (J) (f (z))$
119	118	adantrr	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ⋂_{z \in x} f (z) \subseteq ⋂_{z \in x} cls (J) (f (z))$
120	92 119	eqsstrd	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ⋂ ran f \subseteq ⋂_{z \in x} cls (J) (f (z))$
121	1	clsss2	$⊢ (⋂_{z \in x} cls (J) (f (z)) \in Clsd (J) \land ⋂ ran f \subseteq ⋂_{z \in x} cls (J) (f (z))) \to cls (J) (⋂ ran f) \subseteq ⋂_{z \in x} cls (J) (f (z))$
122	106 120 121	syl2anc	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to cls (J) (⋂ ran f) \subseteq ⋂_{z \in x} cls (J) (f (z))$
123		ssel	$⊢ cls (J) (f (z)) \subseteq X ∖ z \to (y \in cls (J) (f (z)) \to y \in (X ∖ z))$
124	123	adantl	$⊢ (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z) \to (y \in cls (J) (f (z)) \to y \in (X ∖ z))$
125	124	ral2imi	$⊢ \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z) \to (\forall z \in x y \in cls (J) (f (z)) \to \forall z \in x y \in (X ∖ z))$
126		eliin	$⊢ y \in V \to (y \in ⋂_{z \in x} (X ∖ z) \leftrightarrow \forall z \in x y \in (X ∖ z))$
127	126	elv	$⊢ y \in ⋂_{z \in x} (X ∖ z) \leftrightarrow \forall z \in x y \in (X ∖ z)$
128	125 115 127	3imtr4g	$⊢ \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z) \to (y \in ⋂_{z \in x} cls (J) (f (z)) \to y \in ⋂_{z \in x} (X ∖ z))$
129	128	ssrdv	$⊢ \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z) \to ⋂_{z \in x} cls (J) (f (z)) \subseteq ⋂_{z \in x} (X ∖ z)$
130	129	ad2antll	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ⋂_{z \in x} cls (J) (f (z)) \subseteq ⋂_{z \in x} (X ∖ z)$
131		iindif2	$⊢ x \neq \emptyset \to ⋂_{z \in x} (X ∖ z) = X ∖ ⋃_{z \in x} z$
132	94 131	syl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ⋂_{z \in x} (X ∖ z) = X ∖ ⋃_{z \in x} z$
133		simplrl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to S \subseteq ⋃ x$
134		uniiun	$⊢ ⋃ x = ⋃_{z \in x} z$
135	134	sseq2i	$⊢ S \subseteq ⋃ x \leftrightarrow S \subseteq ⋃_{z \in x} z$
136		sscon	$⊢ S \subseteq ⋃_{z \in x} z \to X ∖ ⋃_{z \in x} z \subseteq X ∖ S$
137	135 136	sylbi	$⊢ S \subseteq ⋃ x \to X ∖ ⋃_{z \in x} z \subseteq X ∖ S$
138	133 137	syl	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to X ∖ ⋃_{z \in x} z \subseteq X ∖ S$
139	132 138	eqsstrd	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ⋂_{z \in x} (X ∖ z) \subseteq X ∖ S$
140	130 139	sstrd	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to ⋂_{z \in x} cls (J) (f (z)) \subseteq X ∖ S$
141	122 140	sstrd	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to cls (J) (⋂ ran f) \subseteq X ∖ S$
142		eleq2	$⊢ z = ⋂ ran f \to (A \in z \leftrightarrow A \in ⋂ ran f)$
143		fveq2	$⊢ z = ⋂ ran f \to cls (J) (z) = cls (J) (⋂ ran f)$
144	143	sseq1d	$⊢ z = ⋂ ran f \to (cls (J) (z) \subseteq X ∖ S \leftrightarrow cls (J) (⋂ ran f) \subseteq X ∖ S)$
145	142 144	anbi12d	$⊢ z = ⋂ ran f \to ((A \in z \land cls (J) (z) \subseteq X ∖ S) \leftrightarrow (A \in ⋂ ran f \land cls (J) (⋂ ran f) \subseteq X ∖ S))$
146	145	rspcev	$⊢ (⋂ ran f \in J \land (A \in ⋂ ran f \land cls (J) (⋂ ran f) \subseteq X ∖ S)) \to \exists z \in J (A \in z \land cls (J) (z) \subseteq X ∖ S)$
147	78 93 141 146	syl12anc	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \land (f : x ⟶ J \land \forall z \in x (A \in f (z) \land cls (J) (f (z)) \subseteq X ∖ z))) \to \exists z \in J (A \in z \land cls (J) (z) \subseteq X ∖ S)$
148	55 147	exlimddv	$⊢ ((φ \land x \in (𝒫 O \cap Fin)) \land (S \subseteq ⋃ x \land x \neq \emptyset)) \to \exists z \in J (A \in z \land cls (J) (z) \subseteq X ∖ S)$
149	148	anassrs	$⊢ (((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \land x \neq \emptyset) \to \exists z \in J (A \in z \land cls (J) (z) \subseteq X ∖ S)$
150	35 149	pm2.61dane	$⊢ ((φ \land x \in (𝒫 O \cap Fin)) \land S \subseteq ⋃ x) \to \exists z \in J (A \in z \land cls (J) (z) \subseteq X ∖ S)$
151	3	adantr	$⊢ (φ \land x \in S) \to J \in Haus$
152	4	sselda	$⊢ (φ \land x \in S) \to x \in X$
153	12	adantr	$⊢ (φ \land x \in S) \to A \in X$
154		id	$⊢ x \in S \to x \in S$
155	6	eldifbd	$⊢ φ \to \neg A \in S$
156		nelne2	$⊢ (x \in S \land \neg A \in S) \to x \neq A$
157	154 155 156	syl2anr	$⊢ (φ \land x \in S) \to x \neq A$
158	1	hausnei	$⊢ (J \in Haus \land (x \in X \land A \in X \land x \neq A)) \to \exists y \in J \exists w \in J (x \in y \land A \in w \land y \cap w = \emptyset)$
159	151 152 153 157 158	syl13anc	$⊢ (φ \land x \in S) \to \exists y \in J \exists w \in J (x \in y \land A \in w \land y \cap w = \emptyset)$
160		3anass	$⊢ (x \in y \land A \in w \land y \cap w = \emptyset) \leftrightarrow (x \in y \land (A \in w \land y \cap w = \emptyset))$
161		elssuni	$⊢ w \in J \to w \subseteq ⋃ J$
162	161 1	sseqtrrdi	$⊢ w \in J \to w \subseteq X$
163	162	adantl	$⊢ (((φ \land x \in S) \land y \in J) \land w \in J) \to w \subseteq X$
164		incom	$⊢ y \cap w = w \cap y$
165	164	eqeq1i	$⊢ y \cap w = \emptyset \leftrightarrow w \cap y = \emptyset$
166		reldisj	$⊢ w \subseteq X \to (w \cap y = \emptyset \leftrightarrow w \subseteq X ∖ y)$
167	165 166	bitrid	$⊢ w \subseteq X \to (y \cap w = \emptyset \leftrightarrow w \subseteq X ∖ y)$
168	163 167	syl	$⊢ (((φ \land x \in S) \land y \in J) \land w \in J) \to (y \cap w = \emptyset \leftrightarrow w \subseteq X ∖ y)$
169	151 7	syl	$⊢ (φ \land x \in S) \to J \in Top$
170	1	opncld	$⊢ (J \in Top \land y \in J) \to X ∖ y \in Clsd (J)$
171	169 170	sylan	$⊢ ((φ \land x \in S) \land y \in J) \to X ∖ y \in Clsd (J)$
172	171	adantr	$⊢ (((φ \land x \in S) \land y \in J) \land w \in J) \to X ∖ y \in Clsd (J)$
173	1	clsss2	$⊢ (X ∖ y \in Clsd (J) \land w \subseteq X ∖ y) \to cls (J) (w) \subseteq X ∖ y$
174	173	ex	$⊢ X ∖ y \in Clsd (J) \to (w \subseteq X ∖ y \to cls (J) (w) \subseteq X ∖ y)$
175	172 174	syl	$⊢ (((φ \land x \in S) \land y \in J) \land w \in J) \to (w \subseteq X ∖ y \to cls (J) (w) \subseteq X ∖ y)$
176	168 175	sylbid	$⊢ (((φ \land x \in S) \land y \in J) \land w \in J) \to (y \cap w = \emptyset \to cls (J) (w) \subseteq X ∖ y)$
177	176	anim2d	$⊢ (((φ \land x \in S) \land y \in J) \land w \in J) \to ((A \in w \land y \cap w = \emptyset) \to (A \in w \land cls (J) (w) \subseteq X ∖ y))$
178	177	anim2d	$⊢ (((φ \land x \in S) \land y \in J) \land w \in J) \to ((x \in y \land (A \in w \land y \cap w = \emptyset)) \to (x \in y \land (A \in w \land cls (J) (w) \subseteq X ∖ y)))$
179	160 178	biimtrid	$⊢ (((φ \land x \in S) \land y \in J) \land w \in J) \to ((x \in y \land A \in w \land y \cap w = \emptyset) \to (x \in y \land (A \in w \land cls (J) (w) \subseteq X ∖ y)))$
180	179	reximdva	$⊢ ((φ \land x \in S) \land y \in J) \to (\exists w \in J (x \in y \land A \in w \land y \cap w = \emptyset) \to \exists w \in J (x \in y \land (A \in w \land cls (J) (w) \subseteq X ∖ y)))$
181		r19.42v	$⊢ \exists w \in J (x \in y \land (A \in w \land cls (J) (w) \subseteq X ∖ y)) \leftrightarrow (x \in y \land \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y))$
182	180 181	imbitrdi	$⊢ ((φ \land x \in S) \land y \in J) \to (\exists w \in J (x \in y \land A \in w \land y \cap w = \emptyset) \to (x \in y \land \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y)))$
183	182	reximdva	$⊢ (φ \land x \in S) \to (\exists y \in J \exists w \in J (x \in y \land A \in w \land y \cap w = \emptyset) \to \exists y \in J (x \in y \land \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y)))$
184	159 183	mpd	$⊢ (φ \land x \in S) \to \exists y \in J (x \in y \land \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y))$
185	2	unieqi	$⊢ ⋃ O = ⋃ \{y \in J \| \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y)\}$
186	185	eleq2i	$⊢ x \in ⋃ O \leftrightarrow x \in ⋃ \{y \in J \| \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y)\}$
187		elunirab	$⊢ x \in ⋃ \{y \in J \| \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y)\} \leftrightarrow \exists y \in J (x \in y \land \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y))$
188	186 187	bitri	$⊢ x \in ⋃ O \leftrightarrow \exists y \in J (x \in y \land \exists w \in J (A \in w \land cls (J) (w) \subseteq X ∖ y))$
189	184 188	sylibr	$⊢ (φ \land x \in S) \to x \in ⋃ O$
190	189	ex	$⊢ φ \to (x \in S \to x \in ⋃ O)$
191	190	ssrdv	$⊢ φ \to S \subseteq ⋃ O$
192		unieq	$⊢ z = O \to ⋃ z = ⋃ O$
193	192	sseq2d	$⊢ z = O \to (S \subseteq ⋃ z \leftrightarrow S \subseteq ⋃ O)$
194		pweq	$⊢ z = O \to 𝒫 z = 𝒫 O$
195	194	ineq1d	$⊢ z = O \to 𝒫 z \cap Fin = 𝒫 O \cap Fin$
196	195	rexeqdv	$⊢ z = O \to (\exists x \in (𝒫 z \cap Fin) S \subseteq ⋃ x \leftrightarrow \exists x \in (𝒫 O \cap Fin) S \subseteq ⋃ x)$
197	193 196	imbi12d	$⊢ z = O \to ((S \subseteq ⋃ z \to \exists x \in (𝒫 z \cap Fin) S \subseteq ⋃ x) \leftrightarrow (S \subseteq ⋃ O \to \exists x \in (𝒫 O \cap Fin) S \subseteq ⋃ x))$
198	1	cmpsub	$⊢ (J \in Top \land S \subseteq X) \to (J ↾_{𝑡} S \in Comp \leftrightarrow \forall z \in 𝒫 J (S \subseteq ⋃ z \to \exists x \in (𝒫 z \cap Fin) S \subseteq ⋃ x))$
199	198	biimp3a	$⊢ (J \in Top \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \to \forall z \in 𝒫 J (S \subseteq ⋃ z \to \exists x \in (𝒫 z \cap Fin) S \subseteq ⋃ x)$
200	8 4 5 199	syl3anc	$⊢ φ \to \forall z \in 𝒫 J (S \subseteq ⋃ z \to \exists x \in (𝒫 z \cap Fin) S \subseteq ⋃ x)$
201	2	ssrab3	$⊢ O \subseteq J$
202		elpw2g	$⊢ J \in Haus \to (O \in 𝒫 J \leftrightarrow O \subseteq J)$
203	3 202	syl	$⊢ φ \to (O \in 𝒫 J \leftrightarrow O \subseteq J)$
204	201 203	mpbiri	$⊢ φ \to O \in 𝒫 J$
205	197 200 204	rspcdva	$⊢ φ \to (S \subseteq ⋃ O \to \exists x \in (𝒫 O \cap Fin) S \subseteq ⋃ x)$
206	191 205	mpd	$⊢ φ \to \exists x \in (𝒫 O \cap Fin) S \subseteq ⋃ x$
207	150 206	r19.29a	$⊢ φ \to \exists z \in J (A \in z \land cls (J) (z) \subseteq X ∖ S)$

Metamath Proof Explorer

Theorem hauscmplem

Proof