Theorem islp2 7697

Description: The predicate "P is a limit point of S," in terms of neighborhoods. Definition of limit point in [Munkres] p. 97. Although Munkres uses open neighborhoods, it also works for our more general neighborhoods.

Hypothesis

Ref	Expression
lpfval.1	⊢ X = ∪J

Assertion

Ref	Expression
islp2	⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (P ∈ ((limPt ‘J) ‘S) ↔ ∀n ∈ ((nei ‘J) ‘{P})(n ∩ (S ∖ {P})) ≠ ∅))

Distinct variable groups:   n,J   S,n   n,X   P,n

Proof of Theorem islp2

Step	Hyp	Ref	Expression
1		lpfval.1	. . . . 5 ⊢ X = ∪J
2	1	islp 7694	. . . 4 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (P ∈ ((limPt ‘J) ‘S) ↔ P ∈ ((cls ‘J) ‘(S ∖ {P}))))
3	1	clsval 7627	. . . . . 6 ⊢ ((J ∈ Top ⋀ (S ∖ {P}) ⊆ X) → ((cls ‘J) ‘(S ∖ {P})) = ∩{x ∈ (Clsd ‘J)∣(S ∖ {P}) ⊆ x})
4		ssdifss 2164	. . . . . 6 ⊢ (S ⊆ X → (S ∖ {P}) ⊆ X)
5	3, 4	sylan2 451	. . . . 5 ⊢ ((J ∈ Top ⋀ S ⊆ X) → ((cls ‘J) ‘(S ∖ {P})) = ∩{x ∈ (Clsd ‘J)∣(S ∖ {P}) ⊆ x})
6	5	eleq2d 1538	. . . 4 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (P ∈ ((cls ‘J) ‘(S ∖ {P})) ↔ P ∈ ∩{x ∈ (Clsd ‘J)∣(S ∖ {P}) ⊆ x}))
7	2, 6	bitrd 527	. . 3 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (P ∈ ((limPt ‘J) ‘S) ↔ P ∈ ∩{x ∈ (Clsd ‘J)∣(S ∖ {P}) ⊆ x}))
8	7	3adant3 798	. 2 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (P ∈ ((limPt ‘J) ‘S) ↔ P ∈ ∩{x ∈ (Clsd ‘J)∣(S ∖ {P}) ⊆ x}))
9		elintrabg 2541	. . . 4 ⊢ (P ∈ X → (P ∈ ∩{x ∈ (Clsd ‘J)∣(S ∖ {P}) ⊆ x} ↔ ∀x ∈ (Clsd ‘J)((S ∖ {P}) ⊆ x → P ∈ x)))
10	1	iscld 7619	. . . . . . 7 ⊢ (J ∈ Top → (x ∈ (Clsd ‘J) ↔ (x ⊆ X ⋀ (X ∖ x) ∈ J)))
11	10	imbi1d 612	. . . . . 6 ⊢ (J ∈ Top → ((x ∈ (Clsd ‘J) → ((S ∖ {P}) ⊆ x → P ∈ x)) ↔ ((x ⊆ X ⋀ (X ∖ x) ∈ J) → ((S ∖ {P}) ⊆ x → P ∈ x))))
12	11	albidv 1276	. . . . 5 ⊢ (J ∈ Top → (∀x(x ∈ (Clsd ‘J) → ((S ∖ {P}) ⊆ x → P ∈ x)) ↔ ∀x((x ⊆ X ⋀ (X ∖ x) ∈ J) → ((S ∖ {P}) ⊆ x → P ∈ x))))
13		df-ral 1646	. . . . 5 ⊢ (∀x ∈ (Clsd ‘J)((S ∖ {P}) ⊆ x → P ∈ x) ↔ ∀x(x ∈ (Clsd ‘J) → ((S ∖ {P}) ⊆ x → P ∈ x)))
14	12, 13	syl5bb 531	. . . 4 ⊢ (J ∈ Top → (∀x ∈ (Clsd ‘J)((S ∖ {P}) ⊆ x → P ∈ x) ↔ ∀x((x ⊆ X ⋀ (X ∖ x) ∈ J) → ((S ∖ {P}) ⊆ x → P ∈ x))))
15	9, 14	sylan9bbr 540	. . 3 ⊢ ((J ∈ Top ⋀ P ∈ X) → (P ∈ ∩{x ∈ (Clsd ‘J)∣(S ∖ {P}) ⊆ x} ↔ ∀x((x ⊆ X ⋀ (X ∖ x) ∈ J) → ((S ∖ {P}) ⊆ x → P ∈ x))))
16	15	3adant2 797	. 2 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (P ∈ ∩{x ∈ (Clsd ‘J)∣(S ∖ {P}) ⊆ x} ↔ ∀x((x ⊆ X ⋀ (X ∖ x) ∈ J) → ((S ∖ {P}) ⊆ x → P ∈ x))))
17	1	isneip 7670	. . . . . . . 8 ⊢ ((J ∈ Top ⋀ P ∈ X) → (n ∈ ((nei ‘J) ‘{P}) ↔ (n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n))))
18	17	imbi1d 612	. . . . . . 7 ⊢ ((J ∈ Top ⋀ P ∈ X) → ((n ∈ ((nei ‘J) ‘{P}) → (n ∩ (S ∖ {P})) ≠ ∅) ↔ ((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅)))
19	18	albidv 1276	. . . . . 6 ⊢ ((J ∈ Top ⋀ P ∈ X) → (∀n(n ∈ ((nei ‘J) ‘{P}) → (n ∩ (S ∖ {P})) ≠ ∅) ↔ ∀n((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅)))
20		df-ral 1646	. . . . . 6 ⊢ (∀n ∈ ((nei ‘J) ‘{P})(n ∩ (S ∖ {P})) ≠ ∅ ↔ ∀n(n ∈ ((nei ‘J) ‘{P}) → (n ∩ (S ∖ {P})) ≠ ∅))
21	19, 20	syl5bb 531	. . . . 5 ⊢ ((J ∈ Top ⋀ P ∈ X) → (∀n ∈ ((nei ‘J) ‘{P})(n ∩ (S ∖ {P})) ≠ ∅ ↔ ∀n((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅)))
22	21	3adant2 797	. . . 4 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (∀n ∈ ((nei ‘J) ‘{P})(n ∩ (S ∖ {P})) ≠ ∅ ↔ ∀n((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅)))
23		elpwi 2402	. . . . . . . . . . . 12 ⊢ (n ∈ ℘X → n ⊆ X)
24		dfss4 2238	. . . . . . . . . . . 12 ⊢ (n ⊆ X ↔ (X ∖ (X ∖ n)) = n)
25	23, 24	sylib 198	. . . . . . . . . . 11 ⊢ (n ∈ ℘X → (X ∖ (X ∖ n)) = n)
26	25	eqcomd 1477	. . . . . . . . . 10 ⊢ (n ∈ ℘X → n = (X ∖ (X ∖ n)))
27	26	eleq1d 1537	. . . . . . . . 9 ⊢ (n ∈ ℘X → (n ∈ J ↔ (X ∖ (X ∖ n)) ∈ J))
28	27	adantl 388	. . . . . . . 8 ⊢ (((S ⊆ X ⋀ P ∈ X) ⋀ n ∈ ℘X) → (n ∈ J ↔ (X ∖ (X ∖ n)) ∈ J))
29		reldisj 2309	. . . . . . . . . . . . . 14 ⊢ ((S ∖ {P}) ⊆ X → (((S ∖ {P}) ∩ n) = ∅ ↔ (S ∖ {P}) ⊆ (X ∖ n)))
30	4, 29	syl 10	. . . . . . . . . . . . 13 ⊢ (S ⊆ X → (((S ∖ {P}) ∩ n) = ∅ ↔ (S ∖ {P}) ⊆ (X ∖ n)))
31		incom 2204	. . . . . . . . . . . . . 14 ⊢ (n ∩ (S ∖ {P})) = ((S ∖ {P}) ∩ n)
32	31	eqeq1i 1479	. . . . . . . . . . . . 13 ⊢ ((n ∩ (S ∖ {P})) = ∅ ↔ ((S ∖ {P}) ∩ n) = ∅)
33	30, 32	syl5bb 531	. . . . . . . . . . . 12 ⊢ (S ⊆ X → ((n ∩ (S ∖ {P})) = ∅ ↔ (S ∖ {P}) ⊆ (X ∖ n)))
34	33	adantr 389	. . . . . . . . . . 11 ⊢ ((S ⊆ X ⋀ P ∈ X) → ((n ∩ (S ∖ {P})) = ∅ ↔ (S ∖ {P}) ⊆ (X ∖ n)))
35		eldif 2053	. . . . . . . . . . . . 13 ⊢ (P ∈ (X ∖ n) ↔ (P ∈ X ⋀ ¬ P ∈ n))
36	35	baibr 685	. . . . . . . . . . . 12 ⊢ (P ∈ X → (¬ P ∈ n ↔ P ∈ (X ∖ n)))
37	36	adantl 388	. . . . . . . . . . 11 ⊢ ((S ⊆ X ⋀ P ∈ X) → (¬ P ∈ n ↔ P ∈ (X ∖ n)))
38	34, 37	imbi12d 625	. . . . . . . . . 10 ⊢ ((S ⊆ X ⋀ P ∈ X) → (((n ∩ (S ∖ {P})) = ∅ → ¬ P ∈ n) ↔ ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n))))
39		df-ne 1584	. . . . . . . . . . . 12 ⊢ ((n ∩ (S ∖ {P})) ≠ ∅ ↔ ¬ (n ∩ (S ∖ {P})) = ∅)
40	39	imbi2i 185	. . . . . . . . . . 11 ⊢ ((P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅) ↔ (P ∈ n → ¬ (n ∩ (S ∖ {P})) = ∅))
41		bi2.03 165	. . . . . . . . . . 11 ⊢ ((P ∈ n → ¬ (n ∩ (S ∖ {P})) = ∅) ↔ ((n ∩ (S ∖ {P})) = ∅ → ¬ P ∈ n))
42	40, 41	bitr 173	. . . . . . . . . 10 ⊢ ((P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅) ↔ ((n ∩ (S ∖ {P})) = ∅ → ¬ P ∈ n))
43	38, 42	syl5bb 531	. . . . . . . . 9 ⊢ ((S ⊆ X ⋀ P ∈ X) → ((P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅) ↔ ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n))))
44	43	adantr 389	. . . . . . . 8 ⊢ (((S ⊆ X ⋀ P ∈ X) ⋀ n ∈ ℘X) → ((P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅) ↔ ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n))))
45	28, 44	imbi12d 625	. . . . . . 7 ⊢ (((S ⊆ X ⋀ P ∈ X) ⋀ n ∈ ℘X) → ((n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅)) ↔ ((X ∖ (X ∖ n)) ∈ J → ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n)))))
46	45	ralbidva 1656	. . . . . 6 ⊢ ((S ⊆ X ⋀ P ∈ X) → (∀n ∈ ℘ X(n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅)) ↔ ∀n ∈ ℘ X((X ∖ (X ∖ n)) ∈ J → ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n)))))
47	46	3adant1 796	. . . . 5 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (∀n ∈ ℘ X(n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅)) ↔ ∀n ∈ ℘ X((X ∖ (X ∖ n)) ∈ J → ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n)))))
48		eleq2 1532	. . . . . . . . . . . . . 14 ⊢ (y = n → (P ∈ y ↔ P ∈ n))
49		sseq1 2078	. . . . . . . . . . . . . 14 ⊢ (y = n → (y ⊆ n ↔ n ⊆ n))
50	48, 49	anbi12d 627	. . . . . . . . . . . . 13 ⊢ (y = n → ((P ∈ y ⋀ y ⊆ n) ↔ (P ∈ n ⋀ n ⊆ n)))
51		ssid 2076	. . . . . . . . . . . . . 14 ⊢ n ⊆ n
52	51	biantru 723	. . . . . . . . . . . . 13 ⊢ (P ∈ n ↔ (P ∈ n ⋀ n ⊆ n))
53	50, 52	syl6bbr 537	. . . . . . . . . . . 12 ⊢ (y = n → ((P ∈ y ⋀ y ⊆ n) ↔ P ∈ n))
54	53	rcla4ev 1873	. . . . . . . . . . 11 ⊢ ((n ∈ J ⋀ P ∈ n) → ∃y ∈ J (P ∈ y ⋀ y ⊆ n))
55	54	anim2i 335	. . . . . . . . . 10 ⊢ ((n ⊆ X ⋀ (n ∈ J ⋀ P ∈ n)) → (n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)))
56	55	anassrs 441	. . . . . . . . 9 ⊢ (((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)))
57	56	imim1i 16	. . . . . . . 8 ⊢ (((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅) → (((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅))
58	57	19.20i 990	. . . . . . 7 ⊢ (∀n((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅) → ∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅))
59		ax-17 969	. . . . . . . . 9 ⊢ ((J ∈ Top ⋀ P ∈ X) → ∀n(J ∈ Top ⋀ P ∈ X))
60		hba1 1001	. . . . . . . . 9 ⊢ (∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅) → ∀n∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅))
61	1	eltopss 7553	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((J ∈ Top ⋀ y ∈ J) → y ⊆ X)
62	61	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y ∈ J ⋀ J ∈ Top) → y ⊆ X)
63		pm3.26 319	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y ∈ J ⋀ J ∈ Top) → y ∈ J)
64	62, 63	jca 288	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∈ J ⋀ J ∈ Top) → (y ⊆ X ⋀ y ∈ J))
65	64	anim1i 334	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((y ∈ J ⋀ J ∈ Top) ⋀ P ∈ y) → ((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y))
66	65	adantrr 395	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((y ∈ J ⋀ J ∈ Top) ⋀ (P ∈ y ⋀ P ∈ X)) → ((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y))
67	66	an4s 508	. . . . . . . . . . . . . . . . . . 19 ⊢ (((y ∈ J ⋀ P ∈ y) ⋀ (J ∈ Top ⋀ P ∈ X)) → ((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y))
68	67	adantlrr 399	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ J ⋀ (P ∈ y ⋀ y ⊆ n)) ⋀ (J ∈ Top ⋀ P ∈ X)) → ((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y))
69		ssrin 2230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y ⊆ n → (y ∩ (S ∖ {P})) ⊆ (n ∩ (S ∖ {P})))
70		ssne0 2301	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((y ∩ (S ∖ {P})) ⊆ (n ∩ (S ∖ {P})) ⋀ (y ∩ (S ∖ {P})) ≠ ∅) → (n ∩ (S ∖ {P})) ≠ ∅)
71	70	ex 373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∩ (S ∖ {P})) ⊆ (n ∩ (S ∖ {P})) → ((y ∩ (S ∖ {P})) ≠ ∅ → (n ∩ (S ∖ {P})) ≠ ∅))
72	69, 71	syl 10	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y ⊆ n → ((y ∩ (S ∖ {P})) ≠ ∅ → (n ∩ (S ∖ {P})) ≠ ∅))
73	72	adantl 388	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((P ∈ y ⋀ y ⊆ n) → ((y ∩ (S ∖ {P})) ≠ ∅ → (n ∩ (S ∖ {P})) ≠ ∅))
74	73	ad2antlr 405	. . . . . . . . . . . . . . . . . . 19 ⊢ (((y ∈ J ⋀ (P ∈ y ⋀ y ⊆ n)) ⋀ (J ∈ Top ⋀ P ∈ X)) → ((y ∩ (S ∖ {P})) ≠ ∅ → (n ∩ (S ∖ {P})) ≠ ∅))
75	74	imim2d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ J ⋀ (P ∈ y ⋀ y ⊆ n)) ⋀ (J ∈ Top ⋀ P ∈ X)) → ((((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y) → (y ∩ (S ∖ {P})) ≠ ∅) → (((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y) → (n ∩ (S ∖ {P})) ≠ ∅)))
76	68, 75	mpid 47	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ J ⋀ (P ∈ y ⋀ y ⊆ n)) ⋀ (J ∈ Top ⋀ P ∈ X)) → ((((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y) → (y ∩ (S ∖ {P})) ≠ ∅) → (n ∩ (S ∖ {P})) ≠ ∅))
77	76	exp31 376	. . . . . . . . . . . . . . . 16 ⊢ (y ∈ J → ((P ∈ y ⋀ y ⊆ n) → ((J ∈ Top ⋀ P ∈ X) → ((((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y) → (y ∩ (S ∖ {P})) ≠ ∅) → (n ∩ (S ∖ {P})) ≠ ∅))))
78	77	com4t 40	. . . . . . . . . . . . . . 15 ⊢ ((J ∈ Top ⋀ P ∈ X) → ((((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y) → (y ∩ (S ∖ {P})) ≠ ∅) → (y ∈ J → ((P ∈ y ⋀ y ⊆ n) → (n ∩ (S ∖ {P})) ≠ ∅))))
79	78	imp 350	. . . . . . . . . . . . . 14 ⊢ (((J ∈ Top ⋀ P ∈ X) ⋀ (((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y) → (y ∩ (S ∖ {P})) ≠ ∅)) → (y ∈ J → ((P ∈ y ⋀ y ⊆ n) → (n ∩ (S ∖ {P})) ≠ ∅)))
80		sseq1 2078	. . . . . . . . . . . . . . . . . 18 ⊢ (n = y → (n ⊆ X ↔ y ⊆ X))
81		eleq1 1531	. . . . . . . . . . . . . . . . . 18 ⊢ (n = y → (n ∈ J ↔ y ∈ J))
82	80, 81	anbi12d 627	. . . . . . . . . . . . . . . . 17 ⊢ (n = y → ((n ⊆ X ⋀ n ∈ J) ↔ (y ⊆ X ⋀ y ∈ J)))
83		eleq2 1532	. . . . . . . . . . . . . . . . 17 ⊢ (n = y → (P ∈ n ↔ P ∈ y))
84	82, 83	anbi12d 627	. . . . . . . . . . . . . . . 16 ⊢ (n = y → (((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) ↔ ((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y)))
85		ineq1 2206	. . . . . . . . . . . . . . . . 17 ⊢ (n = y → (n ∩ (S ∖ {P})) = (y ∩ (S ∖ {P})))
86	85	neeq1d 1591	. . . . . . . . . . . . . . . 16 ⊢ (n = y → ((n ∩ (S ∖ {P})) ≠ ∅ ↔ (y ∩ (S ∖ {P})) ≠ ∅))
87	84, 86	imbi12d 625	. . . . . . . . . . . . . . 15 ⊢ (n = y → ((((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅) ↔ (((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y) → (y ∩ (S ∖ {P})) ≠ ∅)))
88	87	a4v 1270	. . . . . . . . . . . . . 14 ⊢ (∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅) → (((y ⊆ X ⋀ y ∈ J) ⋀ P ∈ y) → (y ∩ (S ∖ {P})) ≠ ∅))
89	79, 88	sylan2 451	. . . . . . . . . . . . 13 ⊢ (((J ∈ Top ⋀ P ∈ X) ⋀ ∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅)) → (y ∈ J → ((P ∈ y ⋀ y ⊆ n) → (n ∩ (S ∖ {P})) ≠ ∅)))
90	89	r19.23adv 1743	. . . . . . . . . . . 12 ⊢ (((J ∈ Top ⋀ P ∈ X) ⋀ ∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅)) → (∃y ∈ J (P ∈ y ⋀ y ⊆ n) → (n ∩ (S ∖ {P})) ≠ ∅))
91	90	ex 373	. . . . . . . . . . 11 ⊢ ((J ∈ Top ⋀ P ∈ X) → (∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅) → (∃y ∈ J (P ∈ y ⋀ y ⊆ n) → (n ∩ (S ∖ {P})) ≠ ∅)))
92	91	a1dd 42	. . . . . . . . . 10 ⊢ ((J ∈ Top ⋀ P ∈ X) → (∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅) → (n ⊆ X → (∃y ∈ J (P ∈ y ⋀ y ⊆ n) → (n ∩ (S ∖ {P})) ≠ ∅))))
93	92	imp4a 364	. . . . . . . . 9 ⊢ ((J ∈ Top ⋀ P ∈ X) → (∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅) → ((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅)))
94	59, 60, 93	19.21ad 1057	. . . . . . . 8 ⊢ ((J ∈ Top ⋀ P ∈ X) → (∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅) → ∀n((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅)))
95	94	3adant2 797	. . . . . . 7 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅) → ∀n((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅)))
96	58, 95	impbid2 517	. . . . . 6 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (∀n((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅) ↔ ∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅)))
97		df-ral 1646	. . . . . . 7 ⊢ (∀n ∈ ℘ X(n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅)) ↔ ∀n(n ∈ ℘X → (n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅))))
98		impexp 347	. . . . . . . . 9 ⊢ (((n ⊆ X ⋀ n ∈ J) → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅)) ↔ (n ⊆ X → (n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅))))
99		impexp 347	. . . . . . . . 9 ⊢ ((((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅) ↔ ((n ⊆ X ⋀ n ∈ J) → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅)))
100		visset 1809	. . . . . . . . . . 11 ⊢ n ∈ V
101	100	elpw 2400	. . . . . . . . . 10 ⊢ (n ∈ ℘X ↔ n ⊆ X)
102	101	imbi1i 186	. . . . . . . . 9 ⊢ ((n ∈ ℘X → (n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅))) ↔ (n ⊆ X → (n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅))))
103	98, 99, 102	3bitr4r 184	. . . . . . . 8 ⊢ ((n ∈ ℘X → (n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅))) ↔ (((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅))
104	103	albii 997	. . . . . . 7 ⊢ (∀n(n ∈ ℘X → (n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅))) ↔ ∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅))
105	97, 104	bitr2 174	. . . . . 6 ⊢ (∀n(((n ⊆ X ⋀ n ∈ J) ⋀ P ∈ n) → (n ∩ (S ∖ {P})) ≠ ∅) ↔ ∀n ∈ ℘ X(n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅)))
106	96, 105	syl6bb 535	. . . . 5 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (∀n((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅) ↔ ∀n ∈ ℘ X(n ∈ J → (P ∈ n → (n ∩ (S ∖ {P})) ≠ ∅))))
107		uniexg 2866	. . . . . . . 8 ⊢ (J ∈ Top → ∪J ∈ V)
108	107, 1	syl5eqel 1549	. . . . . . 7 ⊢ (J ∈ Top → X ∈ V)
109	108	3ad2ant1 799	. . . . . 6 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → X ∈ V)
110		difss 2163	. . . . . . . . 9 ⊢ (X ∖ n) ⊆ X
111		elpw2g 2722	. . . . . . . . 9 ⊢ (X ∈ V → ((X ∖ n) ∈ ℘X ↔ (X ∖ n) ⊆ X))
112	110, 111	mpbiri 194	. . . . . . . 8 ⊢ (X ∈ V → (X ∖ n) ∈ ℘X)
113	112	adantr 389	. . . . . . 7 ⊢ ((X ∈ V ⋀ n ∈ ℘X) → (X ∖ n) ∈ ℘X)
114		difeq2 2150	. . . . . . . . . 10 ⊢ (n = (X ∖ x) → (X ∖ n) = (X ∖ (X ∖ x)))
115	114	eqeq2d 1483	. . . . . . . . 9 ⊢ (n = (X ∖ x) → (x = (X ∖ n) ↔ x = (X ∖ (X ∖ x))))
116	115	rcla4ev 1873	. . . . . . . 8 ⊢ (((X ∖ x) ∈ ℘X ⋀ x = (X ∖ (X ∖ x))) → ∃n ∈ ℘ Xx = (X ∖ n))
117		difss 2163	. . . . . . . . 9 ⊢ (X ∖ x) ⊆ X
118		elpw2g 2722	. . . . . . . . 9 ⊢ (X ∈ V → ((X ∖ x) ∈ ℘X ↔ (X ∖ x) ⊆ X))
119	117, 118	mpbiri 194	. . . . . . . 8 ⊢ (X ∈ V → (X ∖ x) ∈ ℘X)
120		elpwi 2402	. . . . . . . . . 10 ⊢ (x ∈ ℘X → x ⊆ X)
121		dfss4 2238	. . . . . . . . . 10 ⊢ (x ⊆ X ↔ (X ∖ (X ∖ x)) = x)
122	120, 121	sylib 198	. . . . . . . . 9 ⊢ (x ∈ ℘X → (X ∖ (X ∖ x)) = x)
123	122	eqcomd 1477	. . . . . . . 8 ⊢ (x ∈ ℘X → x = (X ∖ (X ∖ x)))
124	116, 119, 123	syl2an 454	. . . . . . 7 ⊢ ((X ∈ V ⋀ x ∈ ℘X) → ∃n ∈ ℘ Xx = (X ∖ n))
125		difeq2 2150	. . . . . . . . . 10 ⊢ (x = (X ∖ n) → (X ∖ x) = (X ∖ (X ∖ n)))
126	125	eleq1d 1537	. . . . . . . . 9 ⊢ (x = (X ∖ n) → ((X ∖ x) ∈ J ↔ (X ∖ (X ∖ n)) ∈ J))
127		sseq2 2079	. . . . . . . . . 10 ⊢ (x = (X ∖ n) → ((S ∖ {P}) ⊆ x ↔ (S ∖ {P}) ⊆ (X ∖ n)))
128		eleq2 1532	. . . . . . . . . 10 ⊢ (x = (X ∖ n) → (P ∈ x ↔ P ∈ (X ∖ n)))
129	127, 128	imbi12d 625	. . . . . . . . 9 ⊢ (x = (X ∖ n) → (((S ∖ {P}) ⊆ x → P ∈ x) ↔ ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n))))
130	126, 129	imbi12d 625	. . . . . . . 8 ⊢ (x = (X ∖ n) → (((X ∖ x) ∈ J → ((S ∖ {P}) ⊆ x → P ∈ x)) ↔ ((X ∖ (X ∖ n)) ∈ J → ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n)))))
131	130	adantl 388	. . . . . . 7 ⊢ ((X ∈ V ⋀ x = (X ∖ n)) → (((X ∖ x) ∈ J → ((S ∖ {P}) ⊆ x → P ∈ x)) ↔ ((X ∖ (X ∖ n)) ∈ J → ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n)))))
132	113, 124, 131	ralxfrd 2892	. . . . . 6 ⊢ (X ∈ V → (∀x ∈ ℘ X((X ∖ x) ∈ J → ((S ∖ {P}) ⊆ x → P ∈ x)) ↔ ∀n ∈ ℘ X((X ∖ (X ∖ n)) ∈ J → ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n)))))
133	109, 132	syl 10	. . . . 5 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (∀x ∈ ℘ X((X ∖ x) ∈ J → ((S ∖ {P}) ⊆ x → P ∈ x)) ↔ ∀n ∈ ℘ X((X ∖ (X ∖ n)) ∈ J → ((S ∖ {P}) ⊆ (X ∖ n) → P ∈ (X ∖ n)))))
134	47, 106, 133	3bitr4d 549	. . . 4 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (∀n((n ⊆ X ⋀ ∃y ∈ J (P ∈ y ⋀ y ⊆ n)) → (n ∩ (S ∖ {P})) ≠ ∅) ↔ ∀x ∈ ℘ X((X ∖ x) ∈ J → ((S ∖ {P}) ⊆ x → P ∈ x))))
135	22, 134	bitrd 527	. . 3 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ P ∈ X) → (∀n ∈ ((nei ‘J) ‘{P})(n ∩ (S ∖ {P})) ≠ ∅ ↔ ∀x ∈ ℘ X((X ∖ x) ∈ J → ((S ∖ {P}) ⊆ x → P ∈ x))))
136		df-ral 1646	. . . 4 ⊢ (∀x ∈ ℘ X((X ∖ x) ∈ J → ((S ∖ {P}) ⊆ x → P ∈ x)) ↔ ∀x(x ∈ ℘X → ((X ∖ x) ∈ J → ((S ∖ {P}) ⊆ x → P ∈ x))))
137		visset 1809	. . . . . . . 8 ⊢ x ∈ V
138	137	elpw 2400	. . . . . . 7 ⊢ (x ∈ ℘X ↔ x ⊆ X)
139	138	imbi1i 186	. . . . . 6 ⊢ ((x ∈ ℘X → ((X ∖ x) ∈ J → ((S ∖ {P}) ⊆ x → P ∈ x))) ↔ (x ⊆ X → ((X ∖ x) ∈ J → ((S ∖ {P}) ⊆ x → P ∈ x))))
140		impexp 347	. . . . . 6 ⊢ (((x ⊆ X ⋀ (X ∖