gneispace - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > gneispace		Structured version Visualization version GIF version

Theorem gneispace 37452

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

**Hypothesis**
Ref	Expression
gneispace.a	⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}

**Assertion**
Ref	Expression
gneispace	⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))))

Distinct variable groups: 𝑛,𝐹,𝑝,𝑓 𝐹,𝑠,𝑓 𝑓,𝑛,𝑝 𝑉,𝑝 Allowed substitution hints: 𝐴(𝑓,𝑛,𝑠,𝑝) 𝑉(𝑓,𝑛,𝑠)

Proof of Theorem gneispace Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		gneispace.a	. . 3 ⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))}
2	1	gneispace3 37451	. 2 ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))))
3		simpll 786	. . . 4 ⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → Fun 𝐹)
4		simplr 788	. . . . 5 ⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
5		difss 3699	. . . . . 6 ⊢ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅})
6		difss 3699	. . . . . . 7 ⊢ (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 dom 𝐹
7		sspwb 4844	. . . . . . 7 ⊢ ((𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 dom 𝐹 ↔ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹)
8	6, 7	mpbi 219	. . . . . 6 ⊢ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
9	5, 8	sstri 3577	. . . . 5 ⊢ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
10	4, 9	syl6ss 3580	. . . 4 ⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
11		simpr 476	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
12		simpl 472	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → Fun 𝐹)
13		fvelrn 6260	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝑝 ∈ dom 𝐹) → (𝐹‘𝑝) ∈ ran 𝐹)
14	12, 13	sylan 487	. . . . . . 7 ⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹‘𝑝) ∈ ran 𝐹)
15		ssel2 3563	. . . . . . . 8 ⊢ ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹‘𝑝) ∈ ran 𝐹) → (𝐹‘𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
16		eldifsni 4261	. . . . . . . 8 ⊢ ((𝐹‘𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) → (𝐹‘𝑝) ≠ ∅)
17	15, 16	syl 17	. . . . . . 7 ⊢ ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹‘𝑝) ∈ ran 𝐹) → (𝐹‘𝑝) ≠ ∅)
18	11, 14, 17	syl2an2r 872	. . . . . 6 ⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹‘𝑝) ≠ ∅)
19	18	ralrimiva 2949	. . . . 5 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅)
20		r19.26 3046	. . . . . 6 ⊢ (∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) ↔ (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))
21	20	biimpri 217	. . . . 5 ⊢ ((∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))
22	19, 21	sylan 487	. . . 4 ⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))
23	3, 10, 22	3jca 1235	. . 3 ⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))))
24		simp1 1054	. . . . 5 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → Fun 𝐹)
25		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑝Fun 𝐹
26		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑝ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹
27		nfra1 2925	. . . . . . . . . 10 ⊢ Ⅎ𝑝∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))
28	25, 26, 27	nf3an 1819	. . . . . . . . 9 ⊢ Ⅎ𝑝(Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))
29		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))
30		simpl 472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) → 𝑝 ∈ 𝑛)
31		19.8a 2039	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ 𝑛 → ∃𝑝 𝑝 ∈ 𝑛)
32	30, 31	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) → ∃𝑝 𝑝 ∈ 𝑛)
33	32	ralimi 2936	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛)
34	29, 33	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛)
35	34	ralimi 2936	. . . . . . . . . . . . . 14 ⊢ (∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛)
36	35	3ad2ant3 1077	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛)
37		rsp 2913	. . . . . . . . . . . . 13 ⊢ (∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛))
38	36, 37	syl 17	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛))
39		df-ex 1696	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∀𝑝 ¬ 𝑝 ∈ 𝑛)
40	39	ralbii 2963	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 ↔ ∀𝑛 ∈ (𝐹‘𝑝) ¬ ∀𝑝 ¬ 𝑝 ∈ 𝑛)
41		ralnex 2975	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑛 ∈ (𝐹‘𝑝) ¬ ∀𝑝 ¬ 𝑝 ∈ 𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹‘𝑝)∀𝑝 ¬ 𝑝 ∈ 𝑛)
42	40, 41	bitri 263	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹‘𝑝)∀𝑝 ¬ 𝑝 ∈ 𝑛)
43		0el 3895	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ (𝐹‘𝑝) ↔ ∃𝑛 ∈ (𝐹‘𝑝)∀𝑝 ¬ 𝑝 ∈ 𝑛)
44	42, 43	xchbinxr 324	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∅ ∈ (𝐹‘𝑝))
45	44	biimpi 205	. . . . . . . . . . . . . . 15 ⊢ (∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → ¬ ∅ ∈ (𝐹‘𝑝))
46		elinel1 3761	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) → ∅ ∈ (𝐹‘𝑝))
47	45, 46	nsyl 134	. . . . . . . . . . . . . 14 ⊢ (∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → ¬ ∅ ∈ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹))
48		disjsn 4192	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹))
49	47, 48	sylibr 223	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅)
50		disjdif2 3999	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹))
51	49, 50	syl 17	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹))
52	38, 51	syl6 34	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹)))
53		simp2 1055	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
54	13	ex 449	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → (𝑝 ∈ dom 𝐹 → (𝐹‘𝑝) ∈ ran 𝐹))
55	24, 54	syl 17	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹‘𝑝) ∈ ran 𝐹))
56		ssel2 3563	. . . . . . . . . . . . 13 ⊢ ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹‘𝑝) ∈ ran 𝐹) → (𝐹‘𝑝) ∈ 𝒫 𝒫 dom 𝐹)
57		fvex 6113	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑝) ∈ V
58	57	elpw 4114	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑝) ∈ 𝒫 𝒫 dom 𝐹 ↔ (𝐹‘𝑝) ⊆ 𝒫 dom 𝐹)
59		df-ss 3554	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑝) ⊆ 𝒫 dom 𝐹 ↔ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝))
60	58, 59	sylbb 208	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑝) ∈ 𝒫 𝒫 dom 𝐹 → ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝))
61	56, 60	syl 17	. . . . . . . . . . . 12 ⊢ ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹‘𝑝) ∈ ran 𝐹) → ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝))
62	53, 55, 61	syl6an 566	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)))
63	52, 62	jcad 554	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → ((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝))))
64		eqtr 2629	. . . . . . . . . . 11 ⊢ (((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹‘𝑝))
65		df-ss 3554	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ((𝐹‘𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹‘𝑝))
66		indif2 3829	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅})
67	66	eqeq1i 2615	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹‘𝑝) ↔ (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹‘𝑝))
68	65, 67	bitri 263	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹‘𝑝))
69	64, 68	sylibr 223	. . . . . . . . . 10 ⊢ (((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) → (𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))
70	63, 69	syl6 34	. . . . . . . . 9 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
71	28, 70	ralrimi 2940	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))
72		funfn 5833	. . . . . . . . . . 11 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
73	72	biimpi 205	. . . . . . . . . 10 ⊢ (Fun 𝐹 → 𝐹 Fn dom 𝐹)
74	24, 73	syl 17	. . . . . . . . 9 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → 𝐹 Fn dom 𝐹)
75		sseq1 3589	. . . . . . . . . 10 ⊢ (𝑥 = (𝐹‘𝑝) → (𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
76	75	ralrn 6270	. . . . . . . . 9 ⊢ (𝐹 Fn dom 𝐹 → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
77	74, 76	syl 17	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
78	71, 77	mpbird 246	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}))
79		pwssb 4548	. . . . . . 7 ⊢ (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}))
80	78, 79	sylibr 223	. . . . . 6 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}))
81		simpl 472	. . . . . . . . . 10 ⊢ (((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → (𝐹‘𝑝) ≠ ∅)
82	81	ralimi 2936	. . . . . . . . 9 ⊢ (∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅)
83	82	3ad2ant3 1077	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅)
84	24, 83	jca 553	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅))
85		elrnrexdm 6271	. . . . . . . . . 10 ⊢ (Fun 𝐹 → (∅ ∈ ran 𝐹 → ∃𝑝 ∈ dom 𝐹∅ = (𝐹‘𝑝)))
86		nesym 2838	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑝) ≠ ∅ ↔ ¬ ∅ = (𝐹‘𝑝))
87	86	ralbii 2963	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ↔ ∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹‘𝑝))
88		ralnex 2975	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹‘𝑝) ↔ ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹‘𝑝))
89	87, 88	sylbb 208	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ → ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹‘𝑝))
90	85, 89	nsyli 154	. . . . . . . . 9 ⊢ (Fun 𝐹 → (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ → ¬ ∅ ∈ ran 𝐹))
91	90	imp 444	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) → ¬ ∅ ∈ ran 𝐹)
92		disjsn 4192	. . . . . . . 8 ⊢ ((ran 𝐹 ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ran 𝐹)
93	91, 92	sylibr 223	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) → (ran 𝐹 ∩ {∅}) = ∅)
94	84, 93	syl 17	. . . . . 6 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (ran 𝐹 ∩ {∅}) = ∅)
95		reldisj 3972	. . . . . . 7 ⊢ (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) → ((ran 𝐹 ∩ {∅}) = ∅ ↔ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
96	95	biimpd 218	. . . . . 6 ⊢ (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) → ((ran 𝐹 ∩ {∅}) = ∅ → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
97	80, 94, 96	sylc 63	. . . . 5 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
98	24, 97	jca 553	. . . 4 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
99	20	biimpi 205	. . . . . 6 ⊢ (∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))
100	99	3ad2ant3 1077	. . . . 5 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))
101		simpr 476	. . . . 5 ⊢ ((∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))
102	100, 101	syl 17	. . . 4 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))
103	98, 102	jca 553	. . 3 ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))
104	23, 103	impbii 198	. 2 ⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))))
105	2, 104	syl6bb 275	1 ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 ∀wal 1473 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 ∖ cdif 3537 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 {csn 4125 dom cdm 5038 ran crn 5039 Fun wfun 5798 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-fv 5812

This theorem is referenced by: gneispacef2 37454 gneispacern2 37457 gneispace0nelrn 37458

W3C validator