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 38252
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 38251 . 2 (𝐹𝑉 → (𝐹𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
3 simpll 789 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → Fun 𝐹)
4 simplr 791 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
5 difss 3729 . . . . . 6 (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅})
6 difss 3729 . . . . . . 7 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 dom 𝐹
7 sspwb 4908 . . . . . . 7 ((𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 dom 𝐹 ↔ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹)
86, 7mpbi 220 . . . . . 6 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
95, 8sstri 3604 . . . . 5 (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
104, 9syl6ss 3607 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
11 simpr 477 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
12 simpl 473 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → Fun 𝐹)
13 fvelrn 6338 . . . . . . . 8 ((Fun 𝐹𝑝 ∈ dom 𝐹) → (𝐹𝑝) ∈ ran 𝐹)
1412, 13sylan 488 . . . . . . 7 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹𝑝) ∈ ran 𝐹)
15 ssel2 3590 . . . . . . . 8 ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
16 eldifsni 4311 . . . . . . . 8 ((𝐹𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) → (𝐹𝑝) ≠ ∅)
1715, 16syl 17 . . . . . . 7 ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ≠ ∅)
1811, 14, 17syl2an2r 875 . . . . . 6 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹𝑝) ≠ ∅)
1918ralrimiva 2963 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
20 r19.26 3060 . . . . . 6 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) ↔ (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
2120biimpri 218 . . . . 5 ((∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
2219, 21sylan 488 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
233, 10, 223jca 1240 . . 3 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
24 simp1 1059 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → Fun 𝐹)
25 nfv 1841 . . . . . . . . . 10 𝑝Fun 𝐹
26 nfv 1841 . . . . . . . . . 10 𝑝ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹
27 nfra1 2938 . . . . . . . . . 10 𝑝𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
2825, 26, 27nf3an 1829 . . . . . . . . 9 𝑝(Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
29 simpr 477 . . . . . . . . . . . . . . . 16 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
30 simpl 473 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → 𝑝𝑛)
31 19.8a 2050 . . . . . . . . . . . . . . . . . 18 (𝑝𝑛 → ∃𝑝 𝑝𝑛)
3230, 31syl 17 . . . . . . . . . . . . . . . . 17 ((𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → ∃𝑝 𝑝𝑛)
3332ralimi 2949 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
3429, 33syl 17 . . . . . . . . . . . . . . 15 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
3534ralimi 2949 . . . . . . . . . . . . . 14 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
36353ad2ant3 1082 . . . . . . . . . . . . 13 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
37 rsp 2926 . . . . . . . . . . . . 13 (∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛))
3836, 37syl 17 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛))
39 df-ex 1703 . . . . . . . . . . . . . . . . . . 19 (∃𝑝 𝑝𝑛 ↔ ¬ ∀𝑝 ¬ 𝑝𝑛)
4039ralbii 2977 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ∀𝑛 ∈ (𝐹𝑝) ¬ ∀𝑝 ¬ 𝑝𝑛)
41 ralnex 2989 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝐹𝑝) ¬ ∀𝑝 ¬ 𝑝𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
4240, 41bitri 264 . . . . . . . . . . . . . . . . 17 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
43 0el 3931 . . . . . . . . . . . . . . . . 17 (∅ ∈ (𝐹𝑝) ↔ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
4442, 43xchbinxr 325 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ¬ ∅ ∈ (𝐹𝑝))
4544biimpi 206 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → ¬ ∅ ∈ (𝐹𝑝))
46 elinel1 3791 . . . . . . . . . . . . . . 15 (∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) → ∅ ∈ (𝐹𝑝))
4745, 46nsyl 135 . . . . . . . . . . . . . 14 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → ¬ ∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
48 disjsn 4237 . . . . . . . . . . . . . 14 ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
4947, 48sylibr 224 . . . . . . . . . . . . 13 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅)
50 disjdif2 4038 . . . . . . . . . . . . 13 ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
5149, 50syl 17 . . . . . . . . . . . 12 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
5238, 51syl6 35 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹)))
53 simp2 1060 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
5413ex 450 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ∈ ran 𝐹))
5524, 54syl 17 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ∈ ran 𝐹))
56 ssel2 3590 . . . . . . . . . . . . 13 ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹)
57 fvex 6188 . . . . . . . . . . . . . . 15 (𝐹𝑝) ∈ V
5857elpw 4155 . . . . . . . . . . . . . 14 ((𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹 ↔ (𝐹𝑝) ⊆ 𝒫 dom 𝐹)
59 df-ss 3581 . . . . . . . . . . . . . 14 ((𝐹𝑝) ⊆ 𝒫 dom 𝐹 ↔ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6058, 59sylbb 209 . . . . . . . . . . . . 13 ((𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹 → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6156, 60syl 17 . . . . . . . . . . . 12 ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹𝑝) ∈ ran 𝐹) → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6253, 55, 61syl6an 567 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)))
6352, 62jcad 555 . . . . . . . . . 10 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))))
64 eqtr 2639 . . . . . . . . . . 11 (((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)) → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
65 df-ss 3581 . . . . . . . . . . . 12 ((𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹𝑝))
66 indif2 3862 . . . . . . . . . . . . 13 ((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅})
6766eqeq1i 2625 . . . . . . . . . . . 12 (((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹𝑝) ↔ (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
6865, 67bitri 264 . . . . . . . . . . 11 ((𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
6964, 68sylibr 224 . . . . . . . . . 10 (((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)) → (𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))
7063, 69syl6 35 . . . . . . . . 9 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7128, 70ralrimi 2954 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))
72 funfn 5906 . . . . . . . . . . 11 (Fun 𝐹𝐹 Fn dom 𝐹)
7372biimpi 206 . . . . . . . . . 10 (Fun 𝐹𝐹 Fn dom 𝐹)
7424, 73syl 17 . . . . . . . . 9 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → 𝐹 Fn dom 𝐹)
75 sseq1 3618 . . . . . . . . . 10 (𝑥 = (𝐹𝑝) → (𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7675ralrn 6348 . . . . . . . . 9 (𝐹 Fn dom 𝐹 → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7774, 76syl 17 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7871, 77mpbird 247 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}))
79 pwssb 4603 . . . . . . 7 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}))
8078, 79sylibr 224 . . . . . 6 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}))
81 simpl 473 . . . . . . . . . 10 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (𝐹𝑝) ≠ ∅)
8281ralimi 2949 . . . . . . . . 9 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
83823ad2ant3 1082 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
8424, 83jca 554 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅))
85 elrnrexdm 6349 . . . . . . . . . 10 (Fun 𝐹 → (∅ ∈ ran 𝐹 → ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝)))
86 nesym 2847 . . . . . . . . . . . 12 ((𝐹𝑝) ≠ ∅ ↔ ¬ ∅ = (𝐹𝑝))
8786ralbii 2977 . . . . . . . . . . 11 (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ↔ ∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹𝑝))
88 ralnex 2989 . . . . . . . . . . 11 (∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹𝑝) ↔ ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝))
8987, 88sylbb 209 . . . . . . . . . 10 (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ → ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝))
9085, 89nsyli 155 . . . . . . . . 9 (Fun 𝐹 → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ → ¬ ∅ ∈ ran 𝐹))
9190imp 445 . . . . . . . 8 ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅) → ¬ ∅ ∈ ran 𝐹)
92 disjsn 4237 . . . . . . . 8 ((ran 𝐹 ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ran 𝐹)
9391, 92sylibr 224 . . . . . . 7 ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅) → (ran 𝐹 ∩ {∅}) = ∅)
9484, 93syl 17 . . . . . 6 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (ran 𝐹 ∩ {∅}) = ∅)
95 reldisj 4011 . . . . . . 7 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) → ((ran 𝐹 ∩ {∅}) = ∅ ↔ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9695biimpd 219 . . . . . 6 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) → ((ran 𝐹 ∩ {∅}) = ∅ → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9780, 94, 96sylc 65 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
9824, 97jca 554 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9920biimpi 206 . . . . . 6 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
100993ad2ant3 1082 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
101 simpr 477 . . . . 5 ((∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
102100, 101syl 17 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
10398, 102jca 554 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
10423, 103impbii 199 . 2 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
1052, 104syl6bb 276 1 (𝐹𝑉 → (𝐹𝐴 ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036  wal 1479   = wceq 1481  wex 1702  wcel 1988  {cab 2606  wne 2791  wral 2909  wrex 2910  cdif 3564  cin 3566  wss 3567  c0 3907  𝒫 cpw 4149  {csn 4168  dom cdm 5104  ran crn 5105  Fun wfun 5870   Fn wfn 5871  wf 5872  cfv 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-fv 5884
This theorem is referenced by:  gneispacef2  38254  gneispacern2  38257  gneispace0nelrn  38258
  Copyright terms: Public domain W3C validator