Theorem 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	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	dfac14lem.s	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ 𝑊 )
	dfac14lem.0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ≠ ∅ )
	dfac14lem.p	⊢ 𝑃 = 𝒫 ∪ 𝑆
	dfac14lem.r	⊢ 𝑅 = { 𝑦 ∈ 𝒫 ( 𝑆 ∪ { 𝑃 } ) ∣ ( 𝑃 ∈ 𝑦 → 𝑦 = ( 𝑆 ∪ { 𝑃 } ) ) }
	dfac14lem.j	⊢ 𝐽 = ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
	dfac14lem.c	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ X 𝑥 ∈ 𝐼 𝑆 ) = X 𝑥 ∈ 𝐼 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
Assertion	dfac14lem	⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 𝑆 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		dfac14lem.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
2		dfac14lem.s	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ 𝑊 )
3		dfac14lem.0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ≠ ∅ )
4		dfac14lem.p	⊢ 𝑃 = 𝒫 ∪ 𝑆
5		dfac14lem.r	⊢ 𝑅 = { 𝑦 ∈ 𝒫 ( 𝑆 ∪ { 𝑃 } ) ∣ ( 𝑃 ∈ 𝑦 → 𝑦 = ( 𝑆 ∪ { 𝑃 } ) ) }
6		dfac14lem.j	⊢ 𝐽 = ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
7		dfac14lem.c	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ X 𝑥 ∈ 𝐼 𝑆 ) = X 𝑥 ∈ 𝐼 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
8		eleq2w	⊢ ( 𝑦 = 𝑧 → ( 𝑃 ∈ 𝑦 ↔ 𝑃 ∈ 𝑧 ) )
9		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = ( 𝑆 ∪ { 𝑃 } ) ↔ 𝑧 = ( 𝑆 ∪ { 𝑃 } ) ) )
10	8 9	imbi12d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑃 ∈ 𝑦 → 𝑦 = ( 𝑆 ∪ { 𝑃 } ) ) ↔ ( 𝑃 ∈ 𝑧 → 𝑧 = ( 𝑆 ∪ { 𝑃 } ) ) ) )
11	10 5	elrab2	⊢ ( 𝑧 ∈ 𝑅 ↔ ( 𝑧 ∈ 𝒫 ( 𝑆 ∪ { 𝑃 } ) ∧ ( 𝑃 ∈ 𝑧 → 𝑧 = ( 𝑆 ∪ { 𝑃 } ) ) ) )
12	3	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑧 ∈ 𝒫 ( 𝑆 ∪ { 𝑃 } ) ) → 𝑆 ≠ ∅ )
13		ineq1	⊢ ( 𝑧 = ( 𝑆 ∪ { 𝑃 } ) → ( 𝑧 ∩ 𝑆 ) = ( ( 𝑆 ∪ { 𝑃 } ) ∩ 𝑆 ) )
14		ssun1	⊢ 𝑆 ⊆ ( 𝑆 ∪ { 𝑃 } )
15		sseqin2	⊢ ( 𝑆 ⊆ ( 𝑆 ∪ { 𝑃 } ) ↔ ( ( 𝑆 ∪ { 𝑃 } ) ∩ 𝑆 ) = 𝑆 )
16	14 15	mpbi	⊢ ( ( 𝑆 ∪ { 𝑃 } ) ∩ 𝑆 ) = 𝑆
17	13 16	eqtrdi	⊢ ( 𝑧 = ( 𝑆 ∪ { 𝑃 } ) → ( 𝑧 ∩ 𝑆 ) = 𝑆 )
18	17	neeq1d	⊢ ( 𝑧 = ( 𝑆 ∪ { 𝑃 } ) → ( ( 𝑧 ∩ 𝑆 ) ≠ ∅ ↔ 𝑆 ≠ ∅ ) )
19	12 18	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑧 ∈ 𝒫 ( 𝑆 ∪ { 𝑃 } ) ) → ( 𝑧 = ( 𝑆 ∪ { 𝑃 } ) → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) )
20	19	imim2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑧 ∈ 𝒫 ( 𝑆 ∪ { 𝑃 } ) ) → ( ( 𝑃 ∈ 𝑧 → 𝑧 = ( 𝑆 ∪ { 𝑃 } ) ) → ( 𝑃 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) ) )
21	20	expimpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑧 ∈ 𝒫 ( 𝑆 ∪ { 𝑃 } ) ∧ ( 𝑃 ∈ 𝑧 → 𝑧 = ( 𝑆 ∪ { 𝑃 } ) ) ) → ( 𝑃 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) ) )
22	11 21	syl5bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑧 ∈ 𝑅 → ( 𝑃 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) ) )
23	22	ralrimiv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∀ 𝑧 ∈ 𝑅 ( 𝑃 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) )
24		snex	⊢ { 𝑃 } ∈ V
25		unexg	⊢ ( ( 𝑆 ∈ 𝑊 ∧ { 𝑃 } ∈ V ) → ( 𝑆 ∪ { 𝑃 } ) ∈ V )
26	2 24 25	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ∪ { 𝑃 } ) ∈ V )
27		ssun2	⊢ { 𝑃 } ⊆ ( 𝑆 ∪ { 𝑃 } )
28		uniexg	⊢ ( 𝑆 ∈ 𝑊 → ∪ 𝑆 ∈ V )
29		pwexg	⊢ ( ∪ 𝑆 ∈ V → 𝒫 ∪ 𝑆 ∈ V )
30	2 28 29	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝒫 ∪ 𝑆 ∈ V )
31	4 30	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑃 ∈ V )
32		snidg	⊢ ( 𝑃 ∈ V → 𝑃 ∈ { 𝑃 } )
33	31 32	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑃 ∈ { 𝑃 } )
34	27 33	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑃 ∈ ( 𝑆 ∪ { 𝑃 } ) )
35		epttop	⊢ ( ( ( 𝑆 ∪ { 𝑃 } ) ∈ V ∧ 𝑃 ∈ ( 𝑆 ∪ { 𝑃 } ) ) → { 𝑦 ∈ 𝒫 ( 𝑆 ∪ { 𝑃 } ) ∣ ( 𝑃 ∈ 𝑦 → 𝑦 = ( 𝑆 ∪ { 𝑃 } ) ) } ∈ ( TopOn ‘ ( 𝑆 ∪ { 𝑃 } ) ) )
36	26 34 35	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → { 𝑦 ∈ 𝒫 ( 𝑆 ∪ { 𝑃 } ) ∣ ( 𝑃 ∈ 𝑦 → 𝑦 = ( 𝑆 ∪ { 𝑃 } ) ) } ∈ ( TopOn ‘ ( 𝑆 ∪ { 𝑃 } ) ) )
37	5 36	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ ( TopOn ‘ ( 𝑆 ∪ { 𝑃 } ) ) )
38		topontop	⊢ ( 𝑅 ∈ ( TopOn ‘ ( 𝑆 ∪ { 𝑃 } ) ) → 𝑅 ∈ Top )
39	37 38	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ Top )
40		toponuni	⊢ ( 𝑅 ∈ ( TopOn ‘ ( 𝑆 ∪ { 𝑃 } ) ) → ( 𝑆 ∪ { 𝑃 } ) = ∪ 𝑅 )
41	37 40	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ∪ { 𝑃 } ) = ∪ 𝑅 )
42	14 41	sseqtrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ⊆ ∪ 𝑅 )
43	34 41	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑃 ∈ ∪ 𝑅 )
44		eqid	⊢ ∪ 𝑅 = ∪ 𝑅
45	44	elcls	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅 ∧ 𝑃 ∈ ∪ 𝑅 ) → ( 𝑃 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑅 ( 𝑃 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) ) )
46	39 42 43 45	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑃 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑅 ( 𝑃 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) ) )
47	23 46	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑃 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
48	47	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑃 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
49		mptelixpg	⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑃 ) ∈ X 𝑥 ∈ 𝐼 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝐼 𝑃 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) )
50	1 49	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑃 ) ∈ X 𝑥 ∈ 𝐼 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝐼 𝑃 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) )
51	48 50	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑃 ) ∈ X 𝑥 ∈ 𝐼 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
52	51	ne0d	⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ≠ ∅ )
53	37	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ ( TopOn ‘ ( 𝑆 ∪ { 𝑃 } ) ) )
54	6	pttopon	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐼 𝑅 ∈ ( TopOn ‘ ( 𝑆 ∪ { 𝑃 } ) ) ) → 𝐽 ∈ ( TopOn ‘ X 𝑥 ∈ 𝐼 ( 𝑆 ∪ { 𝑃 } ) ) )
55	1 53 54	syl2anc	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ X 𝑥 ∈ 𝐼 ( 𝑆 ∪ { 𝑃 } ) ) )
56		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ X 𝑥 ∈ 𝐼 ( 𝑆 ∪ { 𝑃 } ) ) → 𝐽 ∈ Top )
57		cls0	⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ ∅ ) = ∅ )
58	55 56 57	3syl	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ ∅ ) = ∅ )
59	52 7 58	3netr4d	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ X 𝑥 ∈ 𝐼 𝑆 ) ≠ ( ( cls ‘ 𝐽 ) ‘ ∅ ) )
60		fveq2	⊢ ( X 𝑥 ∈ 𝐼 𝑆 = ∅ → ( ( cls ‘ 𝐽 ) ‘ X 𝑥 ∈ 𝐼 𝑆 ) = ( ( cls ‘ 𝐽 ) ‘ ∅ ) )
61	60	necon3i	⊢ ( ( ( cls ‘ 𝐽 ) ‘ X 𝑥 ∈ 𝐼 𝑆 ) ≠ ( ( cls ‘ 𝐽 ) ‘ ∅ ) → X 𝑥 ∈ 𝐼 𝑆 ≠ ∅ )
62	59 61	syl	⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 𝑆 ≠ ∅ )