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 
|- ( ph -> B e. V )
neik0pk1imk0.n 
|- ( ph -> N e. ( ~P ~P B ^m B ) )
neik0pk1imk0.k0p 
|- ( ph -> A. x e. B ( N ` x ) =/= (/) )
neik0pk1imk0.k1 
|- ( ph -> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) )
Assertion neik0pk1imk0 
|- ( ph -> A. x e. B B e. ( N ` x ) )

Proof

Step Hyp Ref Expression
1 neik0pk1imk0.bex 
 |-  ( ph -> B e. V )
2 neik0pk1imk0.n 
 |-  ( ph -> N e. ( ~P ~P B ^m B ) )
3 neik0pk1imk0.k0p 
 |-  ( ph -> A. x e. B ( N ` x ) =/= (/) )
4 neik0pk1imk0.k1 
 |-  ( ph -> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) )
5 pwidg 
 |-  ( B e. V -> B e. ~P B )
6 sseq2 
 |-  ( t = B -> ( s C_ t <-> s C_ B ) )
7 6 anbi2d 
 |-  ( t = B -> ( ( s e. ( N ` x ) /\ s C_ t ) <-> ( s e. ( N ` x ) /\ s C_ B ) ) )
8 eleq1 
 |-  ( t = B -> ( t e. ( N ` x ) <-> B e. ( N ` x ) ) )
9 7 8 imbi12d 
 |-  ( t = B -> ( ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) <-> ( ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) ) )
10 9 rspcv 
 |-  ( B e. ~P B -> ( A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) -> ( ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) ) )
11 1 5 10 3syl 
 |-  ( ph -> ( A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) -> ( ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) ) )
12 11 ralimdv 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) -> A. s e. ~P B ( ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) ) )
13 12 ralimdv 
 |-  ( ph -> ( A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) -> A. x e. B A. s e. ~P B ( ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) ) )
14 4 13 mpd 
 |-  ( ph -> A. x e. B A. s e. ~P B ( ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) )
15 r19.23v 
 |-  ( A. s e. ~P B ( ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) <-> ( E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) )
16 15 biimpi 
 |-  ( A. s e. ~P B ( ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) -> ( E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) )
17 16 a1i 
 |-  ( ph -> ( A. s e. ~P B ( ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) -> ( E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) ) )
18 17 ralimdv 
 |-  ( ph -> ( A. x e. B A. s e. ~P B ( ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) -> A. x e. B ( E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) ) )
19 14 18 mpd 
 |-  ( ph -> A. x e. B ( E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) )
20 elmapi 
 |-  ( N e. ( ~P ~P B ^m B ) -> N : B --> ~P ~P B )
21 2 20 syl 
 |-  ( ph -> N : B --> ~P ~P B )
22 21 ffvelcdmda 
 |-  ( ( ph /\ x e. B ) -> ( N ` x ) e. ~P ~P B )
23 22 elpwid 
 |-  ( ( ph /\ x e. B ) -> ( N ` x ) C_ ~P B )
24 23 sseld 
 |-  ( ( ph /\ x e. B ) -> ( s e. ( N ` x ) -> s e. ~P B ) )
25 24 ancrd 
 |-  ( ( ph /\ x e. B ) -> ( s e. ( N ` x ) -> ( s e. ~P B /\ s e. ( N ` x ) ) ) )
26 25 eximdv 
 |-  ( ( ph /\ x e. B ) -> ( E. s s e. ( N ` x ) -> E. s ( s e. ~P B /\ s e. ( N ` x ) ) ) )
27 n0 
 |-  ( ( N ` x ) =/= (/) <-> E. s s e. ( N ` x ) )
28 df-rex 
 |-  ( E. s e. ~P B s e. ( N ` x ) <-> E. s ( s e. ~P B /\ s e. ( N ` x ) ) )
29 26 27 28 3imtr4g 
 |-  ( ( ph /\ x e. B ) -> ( ( N ` x ) =/= (/) -> E. s e. ~P B s e. ( N ` x ) ) )
30 29 imp 
 |-  ( ( ( ph /\ x e. B ) /\ ( N ` x ) =/= (/) ) -> E. s e. ~P B s e. ( N ` x ) )
31 elpwi 
 |-  ( s e. ~P B -> s C_ B )
32 24 31 syl6 
 |-  ( ( ph /\ x e. B ) -> ( s e. ( N ` x ) -> s C_ B ) )
33 32 ralrimivw 
 |-  ( ( ph /\ x e. B ) -> A. s e. ~P B ( s e. ( N ` x ) -> s C_ B ) )
34 33 adantr 
 |-  ( ( ( ph /\ x e. B ) /\ ( N ` x ) =/= (/) ) -> A. s e. ~P B ( s e. ( N ` x ) -> s C_ B ) )
35 30 34 r19.29imd 
 |-  ( ( ( ph /\ x e. B ) /\ ( N ` x ) =/= (/) ) -> E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) )
36 35 ex 
 |-  ( ( ph /\ x e. B ) -> ( ( N ` x ) =/= (/) -> E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) ) )
37 36 ralimdva 
 |-  ( ph -> ( A. x e. B ( N ` x ) =/= (/) -> A. x e. B E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) ) )
38 3 37 mpd 
 |-  ( ph -> A. x e. B E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) )
39 ralim 
 |-  ( A. x e. B ( E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) -> B e. ( N ` x ) ) -> ( A. x e. B E. s e. ~P B ( s e. ( N ` x ) /\ s C_ B ) -> A. x e. B B e. ( N ` x ) ) )
40 19 38 39 sylc 
 |-  ( ph -> A. x e. B B e. ( N ` x ) )