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

Theorem gneispace 42875
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.
StepHypRef Expression
1 gneispace.a . . 3 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖ {∅}) ∧ ∀𝑝 ∈ dom 𝑓𝑛 ∈ (𝑓𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛𝑠𝑠 ∈ (𝑓𝑝))))}
21gneispace3 42874 . 2 (𝐹𝑉 → (𝐹𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
3 simpll 765 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → Fun 𝐹)
4 simplr 767 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
5 difss 4131 . . . . . 6 (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅})
6 difss 4131 . . . . . . 7 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 dom 𝐹
76sspwi 4614 . . . . . 6 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
85, 7sstri 3991 . . . . 5 (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
94, 8sstrdi 3994 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
10 simpr 485 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
11 simpl 483 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → Fun 𝐹)
12 fvelrn 7078 . . . . . . . 8 ((Fun 𝐹𝑝 ∈ dom 𝐹) → (𝐹𝑝) ∈ ran 𝐹)
1311, 12sylan 580 . . . . . . 7 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹𝑝) ∈ ran 𝐹)
14 ssel2 3977 . . . . . . . 8 ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
15 eldifsni 4793 . . . . . . . 8 ((𝐹𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) → (𝐹𝑝) ≠ ∅)
1614, 15syl 17 . . . . . . 7 ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ≠ ∅)
1710, 13, 16syl2an2r 683 . . . . . 6 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹𝑝) ≠ ∅)
1817ralrimiva 3146 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
19 r19.26 3111 . . . . . 6 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) ↔ (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
2019biimpri 227 . . . . 5 ((∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
2118, 20sylan 580 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
223, 9, 213jca 1128 . . 3 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
23 simp1 1136 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → Fun 𝐹)
24 nfv 1917 . . . . . . . . . 10 𝑝Fun 𝐹
25 nfv 1917 . . . . . . . . . 10 𝑝ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹
26 nfra1 3281 . . . . . . . . . 10 𝑝𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
2724, 25, 26nf3an 1904 . . . . . . . . 9 𝑝(Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
28 simpr 485 . . . . . . . . . . . . . . . 16 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
29 simpl 483 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → 𝑝𝑛)
302919.8ad 2175 . . . . . . . . . . . . . . . . 17 ((𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → ∃𝑝 𝑝𝑛)
3130ralimi 3083 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
3228, 31syl 17 . . . . . . . . . . . . . . 15 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
3332ralimi 3083 . . . . . . . . . . . . . 14 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
34333ad2ant3 1135 . . . . . . . . . . . . 13 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
35 rsp 3244 . . . . . . . . . . . . 13 (∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛))
3634, 35syl 17 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛))
37 df-ex 1782 . . . . . . . . . . . . . . . . . . 19 (∃𝑝 𝑝𝑛 ↔ ¬ ∀𝑝 ¬ 𝑝𝑛)
3837ralbii 3093 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ∀𝑛 ∈ (𝐹𝑝) ¬ ∀𝑝 ¬ 𝑝𝑛)
39 ralnex 3072 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝐹𝑝) ¬ ∀𝑝 ¬ 𝑝𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
4038, 39bitri 274 . . . . . . . . . . . . . . . . 17 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
41 0el 4360 . . . . . . . . . . . . . . . . 17 (∅ ∈ (𝐹𝑝) ↔ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
4240, 41xchbinxr 334 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ¬ ∅ ∈ (𝐹𝑝))
4342biimpi 215 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → ¬ ∅ ∈ (𝐹𝑝))
44 elinel1 4195 . . . . . . . . . . . . . . 15 (∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) → ∅ ∈ (𝐹𝑝))
4543, 44nsyl 140 . . . . . . . . . . . . . 14 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → ¬ ∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
46 disjsn 4715 . . . . . . . . . . . . . 14 ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
4745, 46sylibr 233 . . . . . . . . . . . . 13 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅)
48 disjdif2 4479 . . . . . . . . . . . . 13 ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
4947, 48syl 17 . . . . . . . . . . . 12 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
5036, 49syl6 35 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹)))
51 simp2 1137 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
5212ex 413 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ∈ ran 𝐹))
5323, 52syl 17 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ∈ ran 𝐹))
54 ssel2 3977 . . . . . . . . . . . . 13 ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹)
55 fvex 6904 . . . . . . . . . . . . . . 15 (𝐹𝑝) ∈ V
5655elpw 4606 . . . . . . . . . . . . . 14 ((𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹 ↔ (𝐹𝑝) ⊆ 𝒫 dom 𝐹)
57 df-ss 3965 . . . . . . . . . . . . . 14 ((𝐹𝑝) ⊆ 𝒫 dom 𝐹 ↔ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
5856, 57sylbb 218 . . . . . . . . . . . . 13 ((𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹 → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
5954, 58syl 17 . . . . . . . . . . . 12 ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹𝑝) ∈ ran 𝐹) → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6051, 53, 59syl6an 682 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)))
6150, 60jcad 513 . . . . . . . . . 10 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))))
62 eqtr 2755 . . . . . . . . . . 11 (((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)) → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
63 df-ss 3965 . . . . . . . . . . . 12 ((𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹𝑝))
64 indif2 4270 . . . . . . . . . . . . 13 ((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅})
6564eqeq1i 2737 . . . . . . . . . . . 12 (((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹𝑝) ↔ (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
6663, 65bitri 274 . . . . . . . . . . 11 ((𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
6762, 66sylibr 233 . . . . . . . . . 10 (((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)) → (𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))
6861, 67syl6 35 . . . . . . . . 9 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
6927, 68ralrimi 3254 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))
7023funfnd 6579 . . . . . . . . 9 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → 𝐹 Fn dom 𝐹)
71 sseq1 4007 . . . . . . . . . 10 (𝑥 = (𝐹𝑝) → (𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7271ralrn 7089 . . . . . . . . 9 (𝐹 Fn dom 𝐹 → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7370, 72syl 17 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7469, 73mpbird 256 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}))
75 pwssb 5104 . . . . . . 7 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}))
7674, 75sylibr 233 . . . . . 6 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}))
77 simpl 483 . . . . . . . . . 10 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (𝐹𝑝) ≠ ∅)
7877ralimi 3083 . . . . . . . . 9 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
79783ad2ant3 1135 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
8023, 79jca 512 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅))
81 elrnrexdm 7090 . . . . . . . . . 10 (Fun 𝐹 → (∅ ∈ ran 𝐹 → ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝)))
82 nesym 2997 . . . . . . . . . . . 12 ((𝐹𝑝) ≠ ∅ ↔ ¬ ∅ = (𝐹𝑝))
8382ralbii 3093 . . . . . . . . . . 11 (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ↔ ∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹𝑝))
84 ralnex 3072 . . . . . . . . . . 11 (∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹𝑝) ↔ ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝))
8583, 84sylbb 218 . . . . . . . . . 10 (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ → ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝))
8681, 85nsyli 157 . . . . . . . . 9 (Fun 𝐹 → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ → ¬ ∅ ∈ ran 𝐹))
8786imp 407 . . . . . . . 8 ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅) → ¬ ∅ ∈ ran 𝐹)
88 disjsn 4715 . . . . . . . 8 ((ran 𝐹 ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ran 𝐹)
8987, 88sylibr 233 . . . . . . 7 ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅) → (ran 𝐹 ∩ {∅}) = ∅)
9080, 89syl 17 . . . . . 6 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (ran 𝐹 ∩ {∅}) = ∅)
91 reldisj 4451 . . . . . . 7 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) → ((ran 𝐹 ∩ {∅}) = ∅ ↔ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9291biimpd 228 . . . . . 6 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) → ((ran 𝐹 ∩ {∅}) = ∅ → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9376, 90, 92sylc 65 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
9423, 93jca 512 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9519biimpi 215 . . . . . 6 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
96953ad2ant3 1135 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
97 simpr 485 . . . . 5 ((∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
9896, 97syl 17 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
9994, 98jca 512 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
10022, 99impbii 208 . 2 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
1012, 100bitrdi 286 1 (𝐹𝑉 → (𝐹𝐴 ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087  wal 1539   = wceq 1541  wex 1781  wcel 2106  {cab 2709  wne 2940  wral 3061  wrex 3070  cdif 3945  cin 3947  wss 3948  c0 4322  𝒫 cpw 4602  {csn 4628  dom cdm 5676  ran crn 5677  Fun wfun 6537   Fn wfn 6538  wf 6539  cfv 6543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551
This theorem is referenced by:  gneispacef2  42877  gneispacern2  42880  gneispace0nelrn  42881
  Copyright terms: Public domain W3C validator