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 ∖ \{\emptyset\}) ∖ \{\emptyset\} \land \forall p \in dom f \forall n \in f (p) (p \in n \land \forall s \in 𝒫 dom f (n \subseteq s \to s \in f (p))))\}$
	Assertion	gneispace	$⊢ F \in V \to (F \in A \leftrightarrow (Fun F \land ran F \subseteq 𝒫 𝒫 dom F \land \forall p \in dom F (F (p) \neq \emptyset \land \forall n \in F (p) (p \in n \land \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p))))))$

Proof

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

Metamath Proof Explorer

Theorem gneispace

Proof