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 38951
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 38950 . 2 (𝐹𝑉 → (𝐹𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
3 simpll 742 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → Fun 𝐹)
4 simplr 744 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
5 difss 3886 . . . . . 6 (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅})
6 difss 3886 . . . . . . 7 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 dom 𝐹
7 sspwb 5045 . . . . . . 7 ((𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 dom 𝐹 ↔ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹)
86, 7mpbi 220 . . . . . 6 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
95, 8sstri 3759 . . . . 5 (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ⊆ 𝒫 𝒫 dom 𝐹
104, 9syl6ss 3762 . . . 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 561 . . . . . . 7 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹𝑝) ∈ ran 𝐹)
15 ssel2 3745 . . . . . . . 8 ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}))
16 eldifsni 4455 . . . . . . . 8 ((𝐹𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) → (𝐹𝑝) ≠ ∅)
1715, 16syl 17 . . . . . . 7 ((ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅}) ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ≠ ∅)
1811, 14, 17syl2an2r 656 . . . . . 6 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ 𝑝 ∈ dom 𝐹) → (𝐹𝑝) ≠ ∅)
1918ralrimiva 3114 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
20 r19.26 3211 . . . . . 6 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) ↔ (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
2120biimpri 218 . . . . 5 ((∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
2219, 21sylan 561 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
233, 10, 223jca 1121 . . 3 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))))
24 simp1 1129 . . . . 5 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → Fun 𝐹)
25 nfv 1994 . . . . . . . . . 10 𝑝Fun 𝐹
26 nfv 1994 . . . . . . . . . 10 𝑝ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹
27 nfra1 3089 . . . . . . . . . 10 𝑝𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
2825, 26, 27nf3an 1982 . . . . . . . . 9 𝑝(Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
29 simpr 471 . . . . . . . . . . . . . . . 16 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))
30 simpl 468 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → 𝑝𝑛)
31 19.8a 2205 . . . . . . . . . . . . . . . . . 18 (𝑝𝑛 → ∃𝑝 𝑝𝑛)
3230, 31syl 17 . . . . . . . . . . . . . . . . 17 ((𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → ∃𝑝 𝑝𝑛)
3332ralimi 3100 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))) → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
3429, 33syl 17 . . . . . . . . . . . . . . 15 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
3534ralimi 3100 . . . . . . . . . . . . . 14 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
36353ad2ant3 1128 . . . . . . . . . . . . 13 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛)
37 rsp 3077 . . . . . . . . . . . . 13 (∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛))
3836, 37syl 17 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛))
39 df-ex 1852 . . . . . . . . . . . . . . . . . . 19 (∃𝑝 𝑝𝑛 ↔ ¬ ∀𝑝 ¬ 𝑝𝑛)
4039ralbii 3128 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ∀𝑛 ∈ (𝐹𝑝) ¬ ∀𝑝 ¬ 𝑝𝑛)
41 ralnex 3140 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝐹𝑝) ¬ ∀𝑝 ¬ 𝑝𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
4240, 41bitri 264 . . . . . . . . . . . . . . . . 17 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
43 0el 4084 . . . . . . . . . . . . . . . . 17 (∅ ∈ (𝐹𝑝) ↔ ∃𝑛 ∈ (𝐹𝑝)∀𝑝 ¬ 𝑝𝑛)
4442, 43xchbinxr 324 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 ↔ ¬ ∅ ∈ (𝐹𝑝))
4544biimpi 206 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → ¬ ∅ ∈ (𝐹𝑝))
46 elinel1 3948 . . . . . . . . . . . . . . 15 (∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) → ∅ ∈ (𝐹𝑝))
4745, 46nsyl 137 . . . . . . . . . . . . . 14 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → ¬ ∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
48 disjsn 4381 . . . . . . . . . . . . . 14 ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
4947, 48sylibr 224 . . . . . . . . . . . . 13 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅)
50 disjdif2 4187 . . . . . . . . . . . . 13 ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
5149, 50syl 17 . . . . . . . . . . . 12 (∀𝑛 ∈ (𝐹𝑝)∃𝑝 𝑝𝑛 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹))
5238, 51syl6 35 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹)))
53 simp2 1130 . . . . . . . . . . . 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 3745 . . . . . . . . . . . . 13 ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹𝑝) ∈ ran 𝐹) → (𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹)
57 fvex 6342 . . . . . . . . . . . . . . 15 (𝐹𝑝) ∈ V
5857elpw 4301 . . . . . . . . . . . . . 14 ((𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹 ↔ (𝐹𝑝) ⊆ 𝒫 dom 𝐹)
59 df-ss 3735 . . . . . . . . . . . . . 14 ((𝐹𝑝) ⊆ 𝒫 dom 𝐹 ↔ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6058, 59sylbb 209 . . . . . . . . . . . . 13 ((𝐹𝑝) ∈ 𝒫 𝒫 dom 𝐹 → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6156, 60syl 17 . . . . . . . . . . . 12 ((ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ (𝐹𝑝) ∈ ran 𝐹) → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))
6253, 55, 61syl6an 655 . . . . . . . . . . 11 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)))
6352, 62jcad 496 . . . . . . . . . 10 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (𝑝 ∈ dom 𝐹 → ((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝))))
64 eqtr 2789 . . . . . . . . . . 11 (((((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹𝑝) ∩ 𝒫 dom 𝐹) = (𝐹𝑝)) → (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹𝑝))
65 df-ss 3735 . . . . . . . . . . . 12 ((𝐹𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹𝑝))
66 indif2 4017 . . . . . . . . . . . . 13 ((𝐹𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (((𝐹𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅})
6766eqeq1i 2775 . . . . . . . . . . . 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 3105 . . . . . . . 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 3773 . . . . . . . . . 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 4744 . . . . . . 7 (ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}))
8078, 79sylibr 224 . . . . . 6 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}))
81 simpl 468 . . . . . . . . . 10 (((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (𝐹𝑝) ≠ ∅)
8281ralimi 3100 . . . . . . . . 9 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
83823ad2ant3 1128 . . . . . . . 8 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅)
8424, 83jca 495 . . . . . . 7 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅))
85 elrnrexdm 6506 . . . . . . . . . 10 (Fun 𝐹 → (∅ ∈ ran 𝐹 → ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝)))
86 nesym 2998 . . . . . . . . . . . 12 ((𝐹𝑝) ≠ ∅ ↔ ¬ ∅ = (𝐹𝑝))
8786ralbii 3128 . . . . . . . . . . 11 (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ↔ ∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹𝑝))
88 ralnex 3140 . . . . . . . . . . 11 (∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹𝑝) ↔ ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝))
8987, 88sylbb 209 . . . . . . . . . 10 (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ → ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹𝑝))
9085, 89nsyli 156 . . . . . . . . 9 (Fun 𝐹 → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ → ¬ ∅ ∈ ran 𝐹))
9190imp 393 . . . . . . . 8 ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅) → ¬ ∅ ∈ ran 𝐹)
92 disjsn 4381 . . . . . . . 8 ((ran 𝐹 ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ran 𝐹)
9391, 92sylibr 224 . . . . . . 7 ((Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅) → (ran 𝐹 ∩ {∅}) = ∅)
9484, 93syl 17 . . . . . 6 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (ran 𝐹 ∩ {∅}) = ∅)
95 reldisj 4161 . . . . . . 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 495 . . . 4 ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝))))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})))
9920biimpi 206 . . . . . 6 (∀𝑝 ∈ dom 𝐹((𝐹𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))) → (∀𝑝 ∈ dom 𝐹(𝐹𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹𝑛 ∈ (𝐹𝑝)(𝑝𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛𝑠𝑠 ∈ (𝐹𝑝)))))
100993ad2ant3 1128 . . . . 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 495 . . 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 1070  wal 1628   = wceq 1630  wex 1851  wcel 2144  {cab 2756  wne 2942  wral 3060  wrex 3061  cdif 3718  cin 3720  wss 3721  c0 4061  𝒫 cpw 4295  {csn 4314  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 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-mpt 4862  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  38953  gneispacern2  38956  gneispace0nelrn  38957
  Copyright terms: Public domain W3C validator