Metamath Proof Explorer

Theorem gneispace

Description: The predicate that F is a (generic) Seifert and Threlfall neighborhood space. (Contributed by RP, 14-Apr-2021)

Ref Expression
Hypothesis gneispace.a ⊢A=f|f:dom⁡f⟶𝒫𝒫dom⁡f∖∅∖∅∧∀p∈dom⁡f∀n∈f⁡pp∈n∧∀s∈𝒫dom⁡fn⊆s→s∈f⁡p
Assertion gneispace ⊢F∈V→F∈A↔Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p

Proof

Step Hyp Ref Expression
1 gneispace.a ⊢A=f|f:dom⁡f⟶𝒫𝒫dom⁡f∖∅∖∅∧∀p∈dom⁡f∀n∈f⁡pp∈n∧∀s∈𝒫dom⁡fn⊆s→s∈f⁡p
2 1 gneispace3 ⊢F∈V→F∈A↔Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
3 simpll ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→Fun⁡F
4 simplr ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅
5 difss ⊢𝒫𝒫dom⁡F∖∅∖∅⊆𝒫𝒫dom⁡F∖∅
6 difss ⊢𝒫dom⁡F∖∅⊆𝒫dom⁡F
7 6 sspwi ⊢𝒫𝒫dom⁡F∖∅⊆𝒫𝒫dom⁡F
8 5 7 sstri ⊢𝒫𝒫dom⁡F∖∅∖∅⊆𝒫𝒫dom⁡F
9 4 8 sstrdi ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→ran⁡F⊆𝒫𝒫dom⁡F
10 simpr ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅→ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅
11 simpl ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅→Fun⁡F
12 fvelrn ⊢Fun⁡F∧p∈dom⁡F→F⁡p∈ran⁡F
13 11 12 sylan ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧p∈dom⁡F→F⁡p∈ran⁡F
14 ssel2 ⊢ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧F⁡p∈ran⁡F→F⁡p∈𝒫𝒫dom⁡F∖∅∖∅
15 eldifsni ⊢F⁡p∈𝒫𝒫dom⁡F∖∅∖∅→F⁡p≠∅
16 14 15 syl ⊢ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧F⁡p∈ran⁡F→F⁡p≠∅
17 10 13 16 syl2an2r ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧p∈dom⁡F→F⁡p≠∅
18 17 ralrimiva ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅→∀p∈dom⁡FF⁡p≠∅
19 r19.26 ⊢∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p↔∀p∈dom⁡FF⁡p≠∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
20 19 biimpri ⊢∀p∈dom⁡FF⁡p≠∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
21 18 20 sylan ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
22 3 9 21 3jca ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
23 simp1 ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→Fun⁡F
24 nfv ⊢ℲpFun⁡F
25 nfv ⊢Ⅎpran⁡F⊆𝒫𝒫dom⁡F
26 nfra1 ⊢Ⅎp∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
27 24 25 26 nf3an ⊢ℲpFun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
28 simpr ⊢F⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
29 simpl ⊢p∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→p∈n
30 29 19.8ad ⊢p∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∃pp∈n
31 30 ralimi ⊢∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀n∈F⁡p∃pp∈n
32 28 31 syl ⊢F⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀n∈F⁡p∃pp∈n
33 32 ralimi ⊢∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡F∀n∈F⁡p∃pp∈n
34 33 3ad2ant3 ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡F∀n∈F⁡p∃pp∈n
35 rsp ⊢∀p∈dom⁡F∀n∈F⁡p∃pp∈n→p∈dom⁡F→∀n∈F⁡p∃pp∈n
36 34 35 syl ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→p∈dom⁡F→∀n∈F⁡p∃pp∈n
37 df-ex ⊢∃pp∈n↔¬∀p¬p∈n
38 37 ralbii ⊢∀n∈F⁡p∃pp∈n↔∀n∈F⁡p¬∀p¬p∈n
39 ralnex ⊢∀n∈F⁡p¬∀p¬p∈n↔¬∃n∈F⁡p∀p¬p∈n
40 38 39 bitri ⊢∀n∈F⁡p∃pp∈n↔¬∃n∈F⁡p∀p¬p∈n
41 0el ⊢∅∈F⁡p↔∃n∈F⁡p∀p¬p∈n
42 40 41 xchbinxr ⊢∀n∈F⁡p∃pp∈n↔¬∅∈F⁡p
43 42 biimpi ⊢∀n∈F⁡p∃pp∈n→¬∅∈F⁡p
44 elinel1 ⊢∅∈F⁡p∩𝒫dom⁡F→∅∈F⁡p
45 43 44 nsyl ⊢∀n∈F⁡p∃pp∈n→¬∅∈F⁡p∩𝒫dom⁡F
46 disjsn ⊢F⁡p∩𝒫dom⁡F∩∅=∅↔¬∅∈F⁡p∩𝒫dom⁡F
47 45 46 sylibr ⊢∀n∈F⁡p∃pp∈n→F⁡p∩𝒫dom⁡F∩∅=∅
48 disjdif2 ⊢F⁡p∩𝒫dom⁡F∩∅=∅→F⁡p∩𝒫dom⁡F∖∅=F⁡p∩𝒫dom⁡F
49 47 48 syl ⊢∀n∈F⁡p∃pp∈n→F⁡p∩𝒫dom⁡F∖∅=F⁡p∩𝒫dom⁡F
50 36 49 syl6 ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→p∈dom⁡F→F⁡p∩𝒫dom⁡F∖∅=F⁡p∩𝒫dom⁡F
51 simp2 ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→ran⁡F⊆𝒫𝒫dom⁡F
52 12 ex ⊢Fun⁡F→p∈dom⁡F→F⁡p∈ran⁡F
53 23 52 syl ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→p∈dom⁡F→F⁡p∈ran⁡F
54 ssel2 ⊢ran⁡F⊆𝒫𝒫dom⁡F∧F⁡p∈ran⁡F→F⁡p∈𝒫𝒫dom⁡F
55 fvex ⊢F⁡p∈V
56 55 elpw ⊢F⁡p∈𝒫𝒫dom⁡F↔F⁡p⊆𝒫dom⁡F
57 df-ss ⊢F⁡p⊆𝒫dom⁡F↔F⁡p∩𝒫dom⁡F=F⁡p
58 56 57 sylbb ⊢F⁡p∈𝒫𝒫dom⁡F→F⁡p∩𝒫dom⁡F=F⁡p
59 54 58 syl ⊢ran⁡F⊆𝒫𝒫dom⁡F∧F⁡p∈ran⁡F→F⁡p∩𝒫dom⁡F=F⁡p
60 51 53 59 syl6an ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→p∈dom⁡F→F⁡p∩𝒫dom⁡F=F⁡p
61 50 60 jcad ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→p∈dom⁡F→F⁡p∩𝒫dom⁡F∖∅=F⁡p∩𝒫dom⁡F∧F⁡p∩𝒫dom⁡F=F⁡p
62 eqtr ⊢F⁡p∩𝒫dom⁡F∖∅=F⁡p∩𝒫dom⁡F∧F⁡p∩𝒫dom⁡F=F⁡p→F⁡p∩𝒫dom⁡F∖∅=F⁡p
63 df-ss ⊢F⁡p⊆𝒫dom⁡F∖∅↔F⁡p∩𝒫dom⁡F∖∅=F⁡p
64 indif2 ⊢F⁡p∩𝒫dom⁡F∖∅=F⁡p∩𝒫dom⁡F∖∅
65 64 eqeq1i ⊢F⁡p∩𝒫dom⁡F∖∅=F⁡p↔F⁡p∩𝒫dom⁡F∖∅=F⁡p
66 63 65 bitri ⊢F⁡p⊆𝒫dom⁡F∖∅↔F⁡p∩𝒫dom⁡F∖∅=F⁡p
67 62 66 sylibr ⊢F⁡p∩𝒫dom⁡F∖∅=F⁡p∩𝒫dom⁡F∧F⁡p∩𝒫dom⁡F=F⁡p→F⁡p⊆𝒫dom⁡F∖∅
68 61 67 syl6 ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→p∈dom⁡F→F⁡p⊆𝒫dom⁡F∖∅
69 27 68 ralrimi ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡FF⁡p⊆𝒫dom⁡F∖∅
70 23 funfnd ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→FFndom⁡F
71 sseq1 ⊢x=F⁡p→x⊆𝒫dom⁡F∖∅↔F⁡p⊆𝒫dom⁡F∖∅
72 71 ralrn ⊢FFndom⁡F→∀x∈ran⁡Fx⊆𝒫dom⁡F∖∅↔∀p∈dom⁡FF⁡p⊆𝒫dom⁡F∖∅
73 70 72 syl ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀x∈ran⁡Fx⊆𝒫dom⁡F∖∅↔∀p∈dom⁡FF⁡p⊆𝒫dom⁡F∖∅
74 69 73 mpbird ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀x∈ran⁡Fx⊆𝒫dom⁡F∖∅
75 pwssb ⊢ran⁡F⊆𝒫𝒫dom⁡F∖∅↔∀x∈ran⁡Fx⊆𝒫dom⁡F∖∅
76 74 75 sylibr ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→ran⁡F⊆𝒫𝒫dom⁡F∖∅
77 simpl ⊢F⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→F⁡p≠∅
78 77 ralimi ⊢∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡FF⁡p≠∅
79 78 3ad2ant3 ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡FF⁡p≠∅
80 23 79 jca ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→Fun⁡F∧∀p∈dom⁡FF⁡p≠∅
81 elrnrexdm ⊢Fun⁡F→∅∈ran⁡F→∃p∈dom⁡F∅=F⁡p
82 nesym ⊢F⁡p≠∅↔¬∅=F⁡p
83 82 ralbii ⊢∀p∈dom⁡FF⁡p≠∅↔∀p∈dom⁡F¬∅=F⁡p
84 ralnex ⊢∀p∈dom⁡F¬∅=F⁡p↔¬∃p∈dom⁡F∅=F⁡p
85 83 84 sylbb ⊢∀p∈dom⁡FF⁡p≠∅→¬∃p∈dom⁡F∅=F⁡p
86 81 85 nsyli ⊢Fun⁡F→∀p∈dom⁡FF⁡p≠∅→¬∅∈ran⁡F
87 86 imp ⊢Fun⁡F∧∀p∈dom⁡FF⁡p≠∅→¬∅∈ran⁡F
88 disjsn ⊢ran⁡F∩∅=∅↔¬∅∈ran⁡F
89 87 88 sylibr ⊢Fun⁡F∧∀p∈dom⁡FF⁡p≠∅→ran⁡F∩∅=∅
90 80 89 syl ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→ran⁡F∩∅=∅
91 reldisj ⊢ran⁡F⊆𝒫𝒫dom⁡F∖∅→ran⁡F∩∅=∅↔ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅
92 91 biimpd ⊢ran⁡F⊆𝒫𝒫dom⁡F∖∅→ran⁡F∩∅=∅→ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅
93 76 90 92 sylc ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅
94 23 93 jca ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅
95 19 biimpi ⊢∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡FF⁡p≠∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
96 95 3ad2ant3 ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡FF⁡p≠∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
97 simpr ⊢∀p∈dom⁡FF⁡p≠∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
98 96 97 syl ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
99 94 98 jca ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p→Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
100 22 99 impbii ⊢Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∖∅∖∅∧∀p∈dom⁡F∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p↔Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p
101 2 100 bitrdi ⊢F∈V→F∈A↔Fun⁡F∧ran⁡F⊆𝒫𝒫dom⁡F∧∀p∈dom⁡FF⁡p≠∅∧∀n∈F⁡pp∈n∧∀s∈𝒫dom⁡Fn⊆s→s∈F⁡p