Metamath Proof Explorer

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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑥 ) ∈ 𝒫 𝒫 𝐵 )
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 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝐵 ∈ ( 𝑁 ‘ 𝑥 ) )