dfac14lem

Description: Lemma for dfac14 . By equipping S u. { P } for some P e/ S with the particular point topology, we can show that P is in the closure of S ; hence the sequence P ( x ) is in the product of the closures, and we can utilize this instance of ptcls to extract an element of the closure of X_ k e. I S . (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	dfac14lem.i	$⊢ φ \to I \in V$
	dfac14lem.s	$⊢ (φ \land x \in I) \to S \in W$
	dfac14lem.0	$⊢ (φ \land x \in I) \to S \neq \emptyset$
	dfac14lem.p	$⊢ P = 𝒫 ⋃ S$
	dfac14lem.r	$⊢ R = \{y \in 𝒫 (S \cup \{P\}) \| (P \in y \to y = S \cup \{P\})\}$
	dfac14lem.j	$⊢ J = \prod_{𝑡} ((x \in I ⟼ R))$
	dfac14lem.c	$⊢ φ \to cls (J) (\underset{x \in I}{⨉} S) = \underset{x \in I}{⨉} cls (R) (S)$
Assertion	dfac14lem	$⊢ φ \to \underset{x \in I}{⨉} S \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		dfac14lem.i	$⊢ φ \to I \in V$
2		dfac14lem.s	$⊢ (φ \land x \in I) \to S \in W$
3		dfac14lem.0	$⊢ (φ \land x \in I) \to S \neq \emptyset$
4		dfac14lem.p	$⊢ P = 𝒫 ⋃ S$
5		dfac14lem.r	$⊢ R = \{y \in 𝒫 (S \cup \{P\}) \| (P \in y \to y = S \cup \{P\})\}$
6		dfac14lem.j	$⊢ J = \prod_{𝑡} ((x \in I ⟼ R))$
7		dfac14lem.c	$⊢ φ \to cls (J) (\underset{x \in I}{⨉} S) = \underset{x \in I}{⨉} cls (R) (S)$
8		eleq2w	$⊢ y = z \to (P \in y \leftrightarrow P \in z)$
9		eqeq1	$⊢ y = z \to (y = S \cup \{P\} \leftrightarrow z = S \cup \{P\})$
10	8 9	imbi12d	$⊢ y = z \to ((P \in y \to y = S \cup \{P\}) \leftrightarrow (P \in z \to z = S \cup \{P\}))$
11	10 5	elrab2	$⊢ z \in R \leftrightarrow (z \in 𝒫 (S \cup \{P\}) \land (P \in z \to z = S \cup \{P\}))$
12	3	adantr	$⊢ ((φ \land x \in I) \land z \in 𝒫 (S \cup \{P\})) \to S \neq \emptyset$
13		ineq1	$⊢ z = S \cup \{P\} \to z \cap S = (S \cup \{P\}) \cap S$
14		ssun1	$⊢ S \subseteq S \cup \{P\}$
15		sseqin2	$⊢ S \subseteq S \cup \{P\} \leftrightarrow (S \cup \{P\}) \cap S = S$
16	14 15	mpbi	$⊢ (S \cup \{P\}) \cap S = S$
17	13 16	eqtrdi	$⊢ z = S \cup \{P\} \to z \cap S = S$
18	17	neeq1d	$⊢ z = S \cup \{P\} \to (z \cap S \neq \emptyset \leftrightarrow S \neq \emptyset)$
19	12 18	syl5ibrcom	$⊢ ((φ \land x \in I) \land z \in 𝒫 (S \cup \{P\})) \to (z = S \cup \{P\} \to z \cap S \neq \emptyset)$
20	19	imim2d	$⊢ ((φ \land x \in I) \land z \in 𝒫 (S \cup \{P\})) \to ((P \in z \to z = S \cup \{P\}) \to (P \in z \to z \cap S \neq \emptyset))$
21	20	expimpd	$⊢ (φ \land x \in I) \to ((z \in 𝒫 (S \cup \{P\}) \land (P \in z \to z = S \cup \{P\})) \to (P \in z \to z \cap S \neq \emptyset))$
22	11 21	biimtrid	$⊢ (φ \land x \in I) \to (z \in R \to (P \in z \to z \cap S \neq \emptyset))$
23	22	ralrimiv	$⊢ (φ \land x \in I) \to \forall z \in R (P \in z \to z \cap S \neq \emptyset)$
24		snex	$⊢ \{P\} \in V$
25		unexg	$⊢ (S \in W \land \{P\} \in V) \to S \cup \{P\} \in V$
26	2 24 25	sylancl	$⊢ (φ \land x \in I) \to S \cup \{P\} \in V$
27		ssun2	$⊢ \{P\} \subseteq S \cup \{P\}$
28		uniexg	$⊢ S \in W \to ⋃ S \in V$
29		pwexg	$⊢ ⋃ S \in V \to 𝒫 ⋃ S \in V$
30	2 28 29	3syl	$⊢ (φ \land x \in I) \to 𝒫 ⋃ S \in V$
31	4 30	eqeltrid	$⊢ (φ \land x \in I) \to P \in V$
32		snidg	$⊢ P \in V \to P \in \{P\}$
33	31 32	syl	$⊢ (φ \land x \in I) \to P \in \{P\}$
34	27 33	sselid	$⊢ (φ \land x \in I) \to P \in (S \cup \{P\})$
35		epttop	$⊢ (S \cup \{P\} \in V \land P \in (S \cup \{P\})) \to \{y \in 𝒫 (S \cup \{P\}) \| (P \in y \to y = S \cup \{P\})\} \in TopOn (S \cup \{P\})$
36	26 34 35	syl2anc	$⊢ (φ \land x \in I) \to \{y \in 𝒫 (S \cup \{P\}) \| (P \in y \to y = S \cup \{P\})\} \in TopOn (S \cup \{P\})$
37	5 36	eqeltrid	$⊢ (φ \land x \in I) \to R \in TopOn (S \cup \{P\})$
38		topontop	$⊢ R \in TopOn (S \cup \{P\}) \to R \in Top$
39	37 38	syl	$⊢ (φ \land x \in I) \to R \in Top$
40		toponuni	$⊢ R \in TopOn (S \cup \{P\}) \to S \cup \{P\} = ⋃ R$
41	37 40	syl	$⊢ (φ \land x \in I) \to S \cup \{P\} = ⋃ R$
42	14 41	sseqtrid	$⊢ (φ \land x \in I) \to S \subseteq ⋃ R$
43	34 41	eleqtrd	$⊢ (φ \land x \in I) \to P \in ⋃ R$
44		eqid	$⊢ ⋃ R = ⋃ R$
45	44	elcls	$⊢ (R \in Top \land S \subseteq ⋃ R \land P \in ⋃ R) \to (P \in cls (R) (S) \leftrightarrow \forall z \in R (P \in z \to z \cap S \neq \emptyset))$
46	39 42 43 45	syl3anc	$⊢ (φ \land x \in I) \to (P \in cls (R) (S) \leftrightarrow \forall z \in R (P \in z \to z \cap S \neq \emptyset))$
47	23 46	mpbird	$⊢ (φ \land x \in I) \to P \in cls (R) (S)$
48	47	ralrimiva	$⊢ φ \to \forall x \in I P \in cls (R) (S)$
49		mptelixpg	$⊢ I \in V \to ((x \in I ⟼ P) \in \underset{x \in I}{⨉} cls (R) (S) \leftrightarrow \forall x \in I P \in cls (R) (S))$
50	1 49	syl	$⊢ φ \to ((x \in I ⟼ P) \in \underset{x \in I}{⨉} cls (R) (S) \leftrightarrow \forall x \in I P \in cls (R) (S))$
51	48 50	mpbird	$⊢ φ \to (x \in I ⟼ P) \in \underset{x \in I}{⨉} cls (R) (S)$
52	51	ne0d	$⊢ φ \to \underset{x \in I}{⨉} cls (R) (S) \neq \emptyset$
53	37	ralrimiva	$⊢ φ \to \forall x \in I R \in TopOn (S \cup \{P\})$
54	6	pttopon	$⊢ (I \in V \land \forall x \in I R \in TopOn (S \cup \{P\})) \to J \in TopOn (\underset{x \in I}{⨉} (S \cup \{P\}))$
55	1 53 54	syl2anc	$⊢ φ \to J \in TopOn (\underset{x \in I}{⨉} (S \cup \{P\}))$
56		topontop	$⊢ J \in TopOn (\underset{x \in I}{⨉} (S \cup \{P\})) \to J \in Top$
57		cls0	$⊢ J \in Top \to cls (J) (\emptyset) = \emptyset$
58	55 56 57	3syl	$⊢ φ \to cls (J) (\emptyset) = \emptyset$
59	52 7 58	3netr4d	$⊢ φ \to cls (J) (\underset{x \in I}{⨉} S) \neq cls (J) (\emptyset)$
60		fveq2	$⊢ \underset{x \in I}{⨉} S = \emptyset \to cls (J) (\underset{x \in I}{⨉} S) = cls (J) (\emptyset)$
61	60	necon3i	$⊢ cls (J) (\underset{x \in I}{⨉} S) \neq cls (J) (\emptyset) \to \underset{x \in I}{⨉} S \neq \emptyset$
62	59 61	syl	$⊢ φ \to \underset{x \in I}{⨉} S \neq \emptyset$

Metamath Proof Explorer

Theorem dfac14lem

Proof