neik0pk1imk0

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

	Ref	Expression
Hypotheses	neik0pk1imk0.bex	$⊢ φ \to B \in V$
	neik0pk1imk0.n	$⊢ φ \to N \in ({𝒫 𝒫 B}^{B})$
	neik0pk1imk0.k0p	$⊢ φ \to \forall x \in B N (x) \neq \emptyset$
	neik0pk1imk0.k1	$⊢ φ \to \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x))$
Assertion	neik0pk1imk0	$⊢ φ \to \forall x \in B B \in N (x)$

Proof

Step	Hyp	Ref	Expression
1		neik0pk1imk0.bex	$⊢ φ \to B \in V$
2		neik0pk1imk0.n	$⊢ φ \to N \in ({𝒫 𝒫 B}^{B})$
3		neik0pk1imk0.k0p	$⊢ φ \to \forall x \in B N (x) \neq \emptyset$
4		neik0pk1imk0.k1	$⊢ φ \to \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x))$
5		pwidg	$⊢ B \in V \to B \in 𝒫 B$
6		sseq2	$⊢ t = B \to (s \subseteq t \leftrightarrow s \subseteq B)$
7	6	anbi2d	$⊢ t = B \to ((s \in N (x) \land s \subseteq t) \leftrightarrow (s \in N (x) \land s \subseteq B))$
8		eleq1	$⊢ t = B \to (t \in N (x) \leftrightarrow B \in N (x))$
9	7 8	imbi12d	$⊢ t = B \to (((s \in N (x) \land s \subseteq t) \to t \in N (x)) \leftrightarrow ((s \in N (x) \land s \subseteq B) \to B \in N (x)))$
10	9	rspcv	$⊢ B \in 𝒫 B \to (\forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x)) \to ((s \in N (x) \land s \subseteq B) \to B \in N (x)))$
11	1 5 10	3syl	$⊢ φ \to (\forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x)) \to ((s \in N (x) \land s \subseteq B) \to B \in N (x)))$
12	11	ralimdv	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x)) \to \forall s \in 𝒫 B ((s \in N (x) \land s \subseteq B) \to B \in N (x)))$
13	12	ralimdv	$⊢ φ \to (\forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B ((s \in N (x) \land s \subseteq t) \to t \in N (x)) \to \forall x \in B \forall s \in 𝒫 B ((s \in N (x) \land s \subseteq B) \to B \in N (x)))$
14	4 13	mpd	$⊢ φ \to \forall x \in B \forall s \in 𝒫 B ((s \in N (x) \land s \subseteq B) \to B \in N (x))$
15		r19.23v	$⊢ \forall s \in 𝒫 B ((s \in N (x) \land s \subseteq B) \to B \in N (x)) \leftrightarrow (\exists s \in 𝒫 B (s \in N (x) \land s \subseteq B) \to B \in N (x))$
16	15	biimpi	$⊢ \forall s \in 𝒫 B ((s \in N (x) \land s \subseteq B) \to B \in N (x)) \to (\exists s \in 𝒫 B (s \in N (x) \land s \subseteq B) \to B \in N (x))$
17	16	a1i	$⊢ φ \to (\forall s \in 𝒫 B ((s \in N (x) \land s \subseteq B) \to B \in N (x)) \to (\exists s \in 𝒫 B (s \in N (x) \land s \subseteq B) \to B \in N (x)))$
18	17	ralimdv	$⊢ φ \to (\forall x \in B \forall s \in 𝒫 B ((s \in N (x) \land s \subseteq B) \to B \in N (x)) \to \forall x \in B (\exists s \in 𝒫 B (s \in N (x) \land s \subseteq B) \to B \in N (x)))$
19	14 18	mpd	$⊢ φ \to \forall x \in B (\exists s \in 𝒫 B (s \in N (x) \land s \subseteq B) \to B \in N (x))$
20		elmapi	$⊢ N \in ({𝒫 𝒫 B}^{B}) \to N : B ⟶ 𝒫 𝒫 B$
21	2 20	syl	$⊢ φ \to N : B ⟶ 𝒫 𝒫 B$
22	21	ffvelrnda	$⊢ (φ \land x \in B) \to N (x) \in 𝒫 𝒫 B$
23	22	elpwid	$⊢ (φ \land x \in B) \to N (x) \subseteq 𝒫 B$
24	23	sseld	$⊢ (φ \land x \in B) \to (s \in N (x) \to s \in 𝒫 B)$
25	24	ancrd	$⊢ (φ \land x \in B) \to (s \in N (x) \to (s \in 𝒫 B \land s \in N (x)))$
26	25	eximdv	$⊢ (φ \land x \in B) \to (\exists s s \in N (x) \to \exists s (s \in 𝒫 B \land s \in N (x)))$
27		n0	$⊢ N (x) \neq \emptyset \leftrightarrow \exists s s \in N (x)$
28		df-rex	$⊢ \exists s \in 𝒫 B s \in N (x) \leftrightarrow \exists s (s \in 𝒫 B \land s \in N (x))$
29	26 27 28	3imtr4g	$⊢ (φ \land x \in B) \to (N (x) \neq \emptyset \to \exists s \in 𝒫 B s \in N (x))$
30	29	imp	$⊢ ((φ \land x \in B) \land N (x) \neq \emptyset) \to \exists s \in 𝒫 B s \in N (x)$
31		elpwi	$⊢ s \in 𝒫 B \to s \subseteq B$
32	24 31	syl6	$⊢ (φ \land x \in B) \to (s \in N (x) \to s \subseteq B)$
33	32	ralrimivw	$⊢ (φ \land x \in B) \to \forall s \in 𝒫 B (s \in N (x) \to s \subseteq B)$
34	33	adantr	$⊢ ((φ \land x \in B) \land N (x) \neq \emptyset) \to \forall s \in 𝒫 B (s \in N (x) \to s \subseteq B)$
35	30 34	r19.29imd	$⊢ ((φ \land x \in B) \land N (x) \neq \emptyset) \to \exists s \in 𝒫 B (s \in N (x) \land s \subseteq B)$
36	35	ex	$⊢ (φ \land x \in B) \to (N (x) \neq \emptyset \to \exists s \in 𝒫 B (s \in N (x) \land s \subseteq B))$
37	36	ralimdva	$⊢ φ \to (\forall x \in B N (x) \neq \emptyset \to \forall x \in B \exists s \in 𝒫 B (s \in N (x) \land s \subseteq B))$
38	3 37	mpd	$⊢ φ \to \forall x \in B \exists s \in 𝒫 B (s \in N (x) \land s \subseteq B)$
39		ralim	$⊢ \forall x \in B (\exists s \in 𝒫 B (s \in N (x) \land s \subseteq B) \to B \in N (x)) \to (\forall x \in B \exists s \in 𝒫 B (s \in N (x) \land s \subseteq B) \to \forall x \in B B \in N (x))$
40	19 38 39	sylc	$⊢ φ \to \forall x \in B B \in N (x)$

Metamath Proof Explorer

Theorem neik0pk1imk0

Proof