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 38958
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 38957 . 2 (𝐹𝑉 → (𝐹𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
3 simpll 750 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → Fun 𝐹)
4 simplr 752 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
5 difss 3888 . . . . . 6 (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅})
6 difss 3888 . . . . . . 7 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 dom 𝐹
7 sspwb 5045 . . . . . . 7 ((𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 dom 𝐹 ↔ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹)
86, 7mpbi 220 . . . . . 6 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
95, 8sstri 3761 . . . . 5 (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
104, 9syl6ss 3764 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
11 simpr 471 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
12 simpl 468 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → Fun 𝐹)
13 fvelrn 6495 . . . . . . . 8 ((Fun 𝐹𝑝 ∈ dom 𝐹) → (𝐹𝑝) ∈ ran 𝐹)
1412, 13sylan 569 . . . . . . 7 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹𝑝) ∈ ran 𝐹)
15 ssel2 3747 . . . . . . . 8 ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
16 eldifsni 4457 . . . . . . . 8 ((𝐹𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) → (𝐹𝑝) ≠ ∅)
1715, 16syl 17 . . . . . . 7 ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ≠ ∅)
1811, 14, 17syl2an2r 664 . . . . . 6 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹𝑝) ≠ ∅)
1918ralrimiva 3115 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
20 r19.26 3212 . . . . . 6 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) ↔ (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
2120biimpri 218 . . . . 5 ((∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
2219, 21sylan 569 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
233, 10, 223jca 1122 . . 3 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
24 simp1 1130 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → Fun 𝐹)
25 nfv 1995 . . . . . . . . . 10 𝑝Fun 𝐹
26 nfv 1995 . . . . . . . . . 10 𝑝ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹
27 nfra1 3090 . . . . . . . . . 10 𝑝𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
2825, 26, 27nf3an 1983 . . . . . . . . 9 𝑝(Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
29 simpr 471 . . . . . . . . . . . . . . . 16 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
30 simpl 468 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → 𝑝𝑛)
31 19.8a 2206 . . . . . . . . . . . . . . . . . 18 (𝑝𝑛 → ∃𝑝 𝑝𝑛)
3230, 31syl 17 . . . . . . . . . . . . . . . . 17 ((𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → ∃𝑝 𝑝𝑛)
3332ralimi 3101 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
3429, 33syl 17 . . . . . . . . . . . . . . 15 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
3534ralimi 3101 . . . . . . . . . . . . . 14 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
36353ad2ant3 1129 . . . . . . . . . . . . 13 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
37 rsp 3078 . . . . . . . . . . . . 13 (∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛))
3836, 37syl 17 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛))
39 df-ex 1853 . . . . . . . . . . . . . . . . . . 19 (∃𝑝 𝑝𝑛 ↔ ¬ ∀𝑝 ¬ 𝑝𝑛)
4039ralbii 3129 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ∀𝑛 ∈ (𝐹𝑝) ¬ ∀𝑝 ¬ 𝑝𝑛)
41 ralnex 3141 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝐹𝑝) ¬ ∀𝑝 ¬ 𝑝𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
4240, 41bitri 264 . . . . . . . . . . . . . . . . 17 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
43 0el 4086 . . . . . . . . . . . . . . . . 17 (∅ ∈ (𝐹𝑝) ↔ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
4442, 43xchbinxr 324 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ¬ ∅ ∈ (𝐹𝑝))
4544biimpi 206 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → ¬ ∅ ∈ (𝐹𝑝))
46 elinel1 3950 . . . . . . . . . . . . . . 15 (∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) → ∅ ∈ (𝐹𝑝))
4745, 46nsyl 137 . . . . . . . . . . . . . 14 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → ¬ ∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
48 disjsn 4383 . . . . . . . . . . . . . 14 ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
4947, 48sylibr 224 . . . . . . . . . . . . 13 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅)
50 disjdif2 4189 . . . . . . . . . . . . 13 ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
5149, 50syl 17 . . . . . . . . . . . 12 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
5238, 51syl6 35 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹)))
53 simp2 1131 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹)
5413ex 397 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ∈ ran 𝐹))
5524, 54syl 17 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹𝑝) ∈ ran 𝐹))
56 ssel2 3747 . . . . . . . . . . . . 13 ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹)
57 fvex 6342 . . . . . . . . . . . . . . 15 (𝐹𝑝) ∈ V
5857elpw 4303 . . . . . . . . . . . . . 14 ((𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹 ↔ (𝐹𝑝) ⊆ 𝒫 dom 𝐹)
59 df-ss 3737 . . . . . . . . . . . . . 14 ((𝐹𝑝) ⊆ 𝒫 dom 𝐹 ↔ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6058, 59sylbb 209 . . . . . . . . . . . . 13 ((𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹 → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6156, 60syl 17 . . . . . . . . . . . 12 ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹𝑝) ∈ ran 𝐹) → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6253, 55, 61syl6an 663 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)))
6352, 62jcad 502 . . . . . . . . . 10 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))))
64 eqtr 2790 . . . . . . . . . . 11 (((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)) → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
65 df-ss 3737 . . . . . . . . . . . 12 ((𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹𝑝))
66 indif2 4019 . . . . . . . . . . . . 13 ((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅})
6766eqeq1i 2776 . . . . . . . . . . . 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 3106 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))
72 funfn 6061 . . . . . . . . . . 11 (Fun 𝐹𝐹 Fn dom 𝐹)
7372biimpi 206 . . . . . . . . . 10 (Fun 𝐹𝐹 Fn dom 𝐹)
7424, 73syl 17 . . . . . . . . 9 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → 𝐹 Fn dom 𝐹)
75 sseq1 3775 . . . . . . . . . 10 (𝑥 = (𝐹𝑝) → (𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})))
7675ralrn 6505 . . . . . . . . 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 4746 . . . . . . 7 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}))
8078, 79sylibr 224 . . . . . 6 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}))
81 simpl 468 . . . . . . . . . 10 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (𝐹𝑝) ≠ ∅)
8281ralimi 3101 . . . . . . . . 9 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
83823ad2ant3 1129 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
8424, 83jca 501 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅))
85 elrnrexdm 6506 . . . . . . . . . 10 (Fun 𝐹 → (∅ ∈ ran 𝐹 → ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝)))
86 nesym 2999 . . . . . . . . . . . 12 ((𝐹𝑝) ≠ ∅ ↔ ¬ ∅ = (𝐹𝑝))
8786ralbii 3129 . . . . . . . . . . 11 (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ↔ ∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹𝑝))
88 ralnex 3141 . . . . . . . . . . 11 (∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹𝑝) ↔ ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝))
8987, 88sylbb 209 . . . . . . . . . 10 (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ → ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝))
9085, 89nsyli 156 . . . . . . . . 9 (Fun 𝐹 → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ → ¬ ∅ ∈ ran 𝐹))
9190imp 393 . . . . . . . 8 ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅) → ¬ ∅ ∈ ran 𝐹)
92 disjsn 4383 . . . . . . . 8 ((ran 𝐹 ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ran 𝐹)
9391, 92sylibr 224 . . . . . . 7 ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅) → (ran 𝐹 ∩ {∅}) = ∅)
9484, 93syl 17 . . . . . 6 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (ran 𝐹 ∩ {∅}) = ∅)
95 reldisj 4163 . . . . . . 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 501 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9920biimpi 206 . . . . . 6 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
100993ad2ant3 1129 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
101 simpr 471 . . . . 5 ((∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
102100, 101syl 17 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
10398, 102jca 501 . . 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 382  w3a 1071  wal 1629   = wceq 1631  wex 1852  wcel 2145  {cab 2757  wne 2943  wral 3061  wrex 3062  cdif 3720  cin 3722  wss 3723  c0 4063  𝒫 cpw 4297  {csn 4316  dom cdm 5249  ran crn 5250  Fun wfun 6025   Fn wfn 6026  wf 6027  cfv 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fv 6039
This theorem is referenced by:  gneispacef2  38960  gneispacern2  38963  gneispace0nelrn  38964
  Copyright terms: Public domain W3C validator