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 40771
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 40770 . 2 (𝐹𝑉 → (𝐹𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
3 simpll 766 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → Fun 𝐹)
4 simplr 768 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
5 difss 4083 . . . . . 6 (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅})
6 difss 4083 . . . . . . 7 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 dom 𝐹
76sspwi 4525 . . . . . 6 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
85, 7sstri 3951 . . . . 5 (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
94, 8sstrdi 3954 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
10 simpr 488 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
11 simpl 486 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → Fun 𝐹)
12 fvelrn 6826 . . . . . . . 8 ((Fun 𝐹𝑝 ∈ dom 𝐹) → (𝐹𝑝) ∈ ran 𝐹)
1311, 12sylan 583 . . . . . . 7 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹𝑝) ∈ ran 𝐹)
14 ssel2 3937 . . . . . . . 8 ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
15 eldifsni 4696 . . . . . . . 8 ((𝐹𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) → (𝐹𝑝) ≠ ∅)
1614, 15syl 17 . . . . . . 7 ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ≠ ∅)
1710, 13, 16syl2an2r 684 . . . . . 6 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹𝑝) ≠ ∅)
1817ralrimiva 3174 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
19 r19.26 3162 . . . . . 6 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) ↔ (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
2019biimpri 231 . . . . 5 ((∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
2118, 20sylan 583 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
223, 9, 213jca 1125 . . 3 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
23 simp1 1133 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → Fun 𝐹)
24 nfv 1915 . . . . . . . . . 10 𝑝Fun 𝐹
25 nfv 1915 . . . . . . . . . 10 𝑝ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹
26 nfra1 3208 . . . . . . . . . 10 𝑝𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
2724, 25, 26nf3an 1902 . . . . . . . . 9 𝑝(Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
28 simpr 488 . . . . . . . . . . . . . . . 16 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
29 simpl 486 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → 𝑝𝑛)
302919.8ad 2182 . . . . . . . . . . . . . . . . 17 ((𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → ∃𝑝 𝑝𝑛)
3130ralimi 3152 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
3228, 31syl 17 . . . . . . . . . . . . . . 15 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
3332ralimi 3152 . . . . . . . . . . . . . 14 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
34333ad2ant3 1132 . . . . . . . . . . . . 13 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
35 rsp 3195 . . . . . . . . . . . . 13 (∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛))
3634, 35syl 17 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛))
37 df-ex 1782 . . . . . . . . . . . . . . . . . . 19 (∃𝑝 𝑝𝑛 ↔ ¬ ∀𝑝 ¬ 𝑝𝑛)
3837ralbii 3157 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ∀𝑛 ∈ (𝐹𝑝) ¬ ∀𝑝 ¬ 𝑝𝑛)
39 ralnex 3224 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝐹𝑝) ¬ ∀𝑝 ¬ 𝑝𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
4038, 39bitri 278 . . . . . . . . . . . . . . . . 17 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
41 0el 4292 . . . . . . . . . . . . . . . . 17 (∅ ∈ (𝐹𝑝) ↔ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
4240, 41xchbinxr 338 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ¬ ∅ ∈ (𝐹𝑝))
4342biimpi 219 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → ¬ ∅ ∈ (𝐹𝑝))
44 elinel1 4146 . . . . . . . . . . . . . . 15 (∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) → ∅ ∈ (𝐹𝑝))
4543, 44nsyl 142 . . . . . . . . . . . . . 14 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → ¬ ∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
46 disjsn 4621 . . . . . . . . . . . . . 14 ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
4745, 46sylibr 237 . . . . . . . . . . . . 13 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅)
48 disjdif2 4400 . . . . . . . . . . . . 13 ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
4947, 48syl 17 . . . . . . . . . . . 12 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
5036, 49syl6 35 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹)))
51 simp2 1134 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
5212ex 416 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ∈ ran 𝐹))
5323, 52syl 17 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ∈ ran 𝐹))
54 ssel2 3937 . . . . . . . . . . . . 13 ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹)
55 fvex 6665 . . . . . . . . . . . . . . 15 (𝐹𝑝) ∈ V
5655elpw 4515 . . . . . . . . . . . . . 14 ((𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹 ↔ (𝐹𝑝) ⊆ 𝒫 dom 𝐹)
57 df-ss 3925 . . . . . . . . . . . . . 14 ((𝐹𝑝) ⊆ 𝒫 dom 𝐹 ↔ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
5856, 57sylbb 222 . . . . . . . . . . . . 13 ((𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹 → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
5954, 58syl 17 . . . . . . . . . . . 12 ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹𝑝) ∈ ran 𝐹) → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6051, 53, 59syl6an 683 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)))
6150, 60jcad 516 . . . . . . . . . 10 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))))
62 eqtr 2842 . . . . . . . . . . 11 (((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)) → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
63 df-ss 3925 . . . . . . . . . . . 12 ((𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹𝑝))
64 indif2 4221 . . . . . . . . . . . . 13 ((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅})
6564eqeq1i 2827 . . . . . . . . . . . 12 (((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹𝑝) ↔ (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
6663, 65bitri 278 . . . . . . . . . . 11 ((𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
6762, 66sylibr 237 . . . . . . . . . 10 (((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)) → (𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))
6861, 67syl6 35 . . . . . . . . 9 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
6927, 68ralrimi 3205 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))
7023funfnd 6365 . . . . . . . . 9 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → 𝐹 Fn dom 𝐹)
71 sseq1 3967 . . . . . . . . . 10 (𝑥 = (𝐹𝑝) → (𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7271ralrn 6836 . . . . . . . . 9 (𝐹 Fn dom 𝐹 → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7370, 72syl 17 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7469, 73mpbird 260 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}))
75 pwssb 4998 . . . . . . 7 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}))
7674, 75sylibr 237 . . . . . 6 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}))
77 simpl 486 . . . . . . . . . 10 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (𝐹𝑝) ≠ ∅)
7877ralimi 3152 . . . . . . . . 9 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
79783ad2ant3 1132 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
8023, 79jca 515 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅))
81 elrnrexdm 6837 . . . . . . . . . 10 (Fun 𝐹 → (∅ ∈ ran 𝐹 → ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝)))
82 nesym 3067 . . . . . . . . . . . 12 ((𝐹𝑝) ≠ ∅ ↔ ¬ ∅ = (𝐹𝑝))
8382ralbii 3157 . . . . . . . . . . 11 (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ↔ ∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹𝑝))
84 ralnex 3224 . . . . . . . . . . 11 (∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹𝑝) ↔ ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝))
8583, 84sylbb 222 . . . . . . . . . 10 (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ → ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝))
8681, 85nsyli 160 . . . . . . . . 9 (Fun 𝐹 → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ → ¬ ∅ ∈ ran 𝐹))
8786imp 410 . . . . . . . 8 ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅) → ¬ ∅ ∈ ran 𝐹)
88 disjsn 4621 . . . . . . . 8 ((ran 𝐹 ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ran 𝐹)
8987, 88sylibr 237 . . . . . . 7 ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅) → (ran 𝐹 ∩ {∅}) = ∅)
9080, 89syl 17 . . . . . 6 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (ran 𝐹 ∩ {∅}) = ∅)
91 reldisj 4374 . . . . . . 7 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) → ((ran 𝐹 ∩ {∅}) = ∅ ↔ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9291biimpd 232 . . . . . 6 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) → ((ran 𝐹 ∩ {∅}) = ∅ → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9376, 90, 92sylc 65 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
9423, 93jca 515 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9519biimpi 219 . . . . . 6 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
96953ad2ant3 1132 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
97 simpr 488 . . . . 5 ((∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
9896, 97syl 17 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
9994, 98jca 515 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
10022, 99impbii 212 . 2 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
1012, 100syl6bb 290 1 (𝐹𝑉 → (𝐹𝐴 ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084  wal 1536   = wceq 1538  wex 1781  wcel 2114  {cab 2800  wne 3011  wral 3130  wrex 3131  cdif 3905  cin 3907  wss 3908  c0 4265  𝒫 cpw 4511  {csn 4539  dom cdm 5532  ran crn 5533  Fun wfun 6328   Fn wfn 6329  wf 6330  cfv 6334
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-fv 6342
This theorem is referenced by:  gneispacef2  40773  gneispacern2  40776  gneispace0nelrn  40777
  Copyright terms: Public domain W3C validator