Theorem neik0pk1imk0

Description: Kuratowski's K0' and K1 axioms imply K0. Neighborhood version. (Contributed by RP, 3-Jun-2021)

	Ref	Expression
Hypotheses	neik0pk1imk0.bex	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	neik0pk1imk0.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
	neik0pk1imk0.k0p	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) ≠ ∅ )
	neik0pk1imk0.k1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
Assertion	neik0pk1imk0	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		neik0pk1imk0.bex	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2		neik0pk1imk0.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
3		neik0pk1imk0.k0p	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) ≠ ∅ )
4		neik0pk1imk0.k1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
5		pwidg	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵 )
6		sseq2	⊢ ( 𝑡 = 𝐵 → ( 𝑠 ⊆ 𝑡 ↔ 𝑠 ⊆ 𝐵 ) )
7	6	anbi2d	⊢ ( 𝑡 = 𝐵 → ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) ) )
8		eleq1	⊢ ( 𝑡 = 𝐵 → ( 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ↔ 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) )
9	7 8	imbi12d	⊢ ( 𝑡 = 𝐵 → ( ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
10	9	rspcv	⊢ ( 𝐵 ∈ 𝒫 𝐵 → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
11	1 5 10	3syl	⊢ ( 𝜑 → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
12	11	ralimdv	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ∀ 𝑠 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
13	12	ralimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝑡 ) → 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
14	4 13	mpd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) )
15		r19.23v	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) ↔ ( ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) )
16	15	biimpi	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) )
17	16	a1i	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
18	17	ralimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
19	14 18	mpd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) )
20		elmapi	⊢ ( 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
21	2 20	syl	⊢ ( 𝜑 → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
22	21	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑥 ) ∈ 𝒫 𝒫 𝐵 )
23	22	elpwid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑥 ) ⊆ 𝒫 𝐵 )
24	23	sseld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑠 ∈ 𝒫 𝐵 ) )
25	24	ancrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
26	25	eximdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑠 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
27		n0	⊢ ( ( 𝑁 ‘ 𝑥 ) ≠ ∅ ↔ ∃ 𝑠 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) )
28		df-rex	⊢ ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝐵 ∧ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
29	26 27 28	3imtr4g	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑥 ) ≠ ∅ → ∃ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
30	29	imp	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑥 ) ≠ ∅ ) → ∃ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) )
31		elpwi	⊢ ( 𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵 )
32	24 31	syl6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑠 ⊆ 𝐵 ) )
33	32	ralrimivw	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑠 ⊆ 𝐵 ) )
34	33	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑥 ) ≠ ∅ ) → ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) → 𝑠 ⊆ 𝐵 ) )
35	30 34	r19.29imd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑥 ) ≠ ∅ ) → ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) )
36	35	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑥 ) ≠ ∅ → ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) ) )
37	36	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑁 ‘ 𝑥 ) ≠ ∅ → ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) ) )
38	3 37	mpd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) )
39		ralim	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑠 ⊆ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) ) )
40	19 38 39	sylc	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) )