Step | Hyp | Ref
| Expression |
1 | | gneispace.a |
. . 3
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖
{∅}) ∧ ∀𝑝
∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} |
2 | 1 | gneispace3 39791 |
. 2
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) ∧ ∀𝑝
∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))) |
3 | | simpll 754 |
. . . 4
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → Fun 𝐹) |
4 | | simplr 756 |
. . . . 5
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) |
5 | | difss 3994 |
. . . . . 6
⊢
(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})
⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) |
6 | | difss 3994 |
. . . . . . 7
⊢
(𝒫 dom 𝐹
∖ {∅}) ⊆ 𝒫 dom 𝐹 |
7 | | sspwb 5191 |
. . . . . . 7
⊢
((𝒫 dom 𝐹
∖ {∅}) ⊆ 𝒫 dom 𝐹 ↔ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆
𝒫 𝒫 dom 𝐹) |
8 | 6, 7 | mpbi 222 |
. . . . . 6
⊢ 𝒫
(𝒫 dom 𝐹 ∖
{∅}) ⊆ 𝒫 𝒫 dom 𝐹 |
9 | 5, 8 | sstri 3863 |
. . . . 5
⊢
(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})
⊆ 𝒫 𝒫 dom 𝐹 |
10 | 4, 9 | syl6ss 3866 |
. . . 4
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹) |
11 | | simpr 477 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) |
12 | | simpl 475 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) → Fun 𝐹) |
13 | | fvelrn 6663 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑝 ∈ dom 𝐹) → (𝐹‘𝑝) ∈ ran 𝐹) |
14 | 12, 13 | sylan 572 |
. . . . . . 7
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ 𝑝
∈ dom 𝐹) → (𝐹‘𝑝) ∈ ran 𝐹) |
15 | | ssel2 3849 |
. . . . . . . 8
⊢ ((ran
𝐹 ⊆ (𝒫
(𝒫 dom 𝐹 ∖
{∅}) ∖ {∅}) ∧ (𝐹‘𝑝) ∈ ran 𝐹) → (𝐹‘𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) |
16 | | eldifsni 4590 |
. . . . . . . 8
⊢ ((𝐹‘𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅}) → (𝐹‘𝑝) ≠ ∅) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ ((ran
𝐹 ⊆ (𝒫
(𝒫 dom 𝐹 ∖
{∅}) ∖ {∅}) ∧ (𝐹‘𝑝) ∈ ran 𝐹) → (𝐹‘𝑝) ≠ ∅) |
18 | 11, 14, 17 | syl2an2r 672 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ 𝑝
∈ dom 𝐹) → (𝐹‘𝑝) ≠ ∅) |
19 | 18 | ralrimiva 3126 |
. . . . 5
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) |
20 | | r19.26 3114 |
. . . . . 6
⊢
(∀𝑝 ∈
dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) ↔ (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
21 | 20 | biimpri 220 |
. . . . 5
⊢
((∀𝑝 ∈
dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
22 | 19, 21 | sylan 572 |
. . . 4
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
23 | 3, 10, 22 | 3jca 1108 |
. . 3
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))) |
24 | | simp1 1116 |
. . . . 5
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → Fun 𝐹) |
25 | | nfv 1873 |
. . . . . . . . . 10
⊢
Ⅎ𝑝Fun 𝐹 |
26 | | nfv 1873 |
. . . . . . . . . 10
⊢
Ⅎ𝑝ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 |
27 | | nfra1 3163 |
. . . . . . . . . 10
⊢
Ⅎ𝑝∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) |
28 | 25, 26, 27 | nf3an 1864 |
. . . . . . . . 9
⊢
Ⅎ𝑝(Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
29 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) |
30 | | simpl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) → 𝑝 ∈ 𝑛) |
31 | 30 | 19.8ad 2108 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) → ∃𝑝 𝑝 ∈ 𝑛) |
32 | 31 | ralimi 3104 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
(𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛) |
33 | 29, 32 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛) |
34 | 33 | ralimi 3104 |
. . . . . . . . . . . . . 14
⊢
(∀𝑝 ∈
dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛) |
35 | 34 | 3ad2ant3 1115 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛) |
36 | | rsp 3149 |
. . . . . . . . . . . . 13
⊢
(∀𝑝 ∈
dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛)) |
38 | | df-ex 1743 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∀𝑝 ¬ 𝑝 ∈ 𝑛) |
39 | 38 | ralbii 3109 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 ↔ ∀𝑛 ∈ (𝐹‘𝑝) ¬ ∀𝑝 ¬ 𝑝 ∈ 𝑛) |
40 | | ralnex 3177 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
(𝐹‘𝑝) ¬ ∀𝑝 ¬ 𝑝 ∈ 𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹‘𝑝)∀𝑝 ¬ 𝑝 ∈ 𝑛) |
41 | 39, 40 | bitri 267 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹‘𝑝)∀𝑝 ¬ 𝑝 ∈ 𝑛) |
42 | | 0el 4201 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∈ (𝐹‘𝑝) ↔ ∃𝑛 ∈ (𝐹‘𝑝)∀𝑝 ¬ 𝑝 ∈ 𝑛) |
43 | 41, 42 | xchbinxr 327 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∅ ∈ (𝐹‘𝑝)) |
44 | 43 | biimpi 208 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → ¬ ∅ ∈ (𝐹‘𝑝)) |
45 | | elinel1 4056 |
. . . . . . . . . . . . . . 15
⊢ (∅
∈ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) → ∅ ∈ (𝐹‘𝑝)) |
46 | 44, 45 | nsyl 138 |
. . . . . . . . . . . . . 14
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → ¬ ∅ ∈ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹)) |
47 | | disjsn 4515 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ ↔ ¬
∅ ∈ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹)) |
48 | 46, 47 | sylibr 226 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) =
∅) |
49 | | disjdif2 4305 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹)) |
51 | 37, 50 | syl6 35 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹))) |
52 | | simp2 1117 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹) |
53 | 13 | ex 405 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → (𝑝 ∈ dom 𝐹 → (𝐹‘𝑝) ∈ ran 𝐹)) |
54 | 24, 53 | syl 17 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹‘𝑝) ∈ ran 𝐹)) |
55 | | ssel2 3849 |
. . . . . . . . . . . . 13
⊢ ((ran
𝐹 ⊆ 𝒫
𝒫 dom 𝐹 ∧
(𝐹‘𝑝) ∈ ran 𝐹) → (𝐹‘𝑝) ∈ 𝒫 𝒫 dom 𝐹) |
56 | | fvex 6506 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑝) ∈ V |
57 | 56 | elpw 4422 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑝) ∈ 𝒫 𝒫 dom 𝐹 ↔ (𝐹‘𝑝) ⊆ 𝒫 dom 𝐹) |
58 | | df-ss 3839 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑝) ⊆ 𝒫 dom 𝐹 ↔ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) |
59 | 57, 58 | sylbb 211 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑝) ∈ 𝒫 𝒫 dom 𝐹 → ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) |
60 | 55, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ ((ran
𝐹 ⊆ 𝒫
𝒫 dom 𝐹 ∧
(𝐹‘𝑝) ∈ ran 𝐹) → ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) |
61 | 52, 54, 60 | syl6an 671 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝))) |
62 | 51, 61 | jcad 505 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → ((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)))) |
63 | | eqtr 2793 |
. . . . . . . . . . 11
⊢
(((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹‘𝑝)) |
64 | | df-ss 3839 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ((𝐹‘𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹‘𝑝)) |
65 | | indif2 4129 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) |
66 | 65 | eqeq1i 2777 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹‘𝑝) ↔ (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹‘𝑝)) |
67 | 64, 66 | bitri 267 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹‘𝑝)) |
68 | 63, 67 | sylibr 226 |
. . . . . . . . . 10
⊢
(((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) → (𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})) |
69 | 62, 68 | syl6 35 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))) |
70 | 28, 69 | ralrimi 3160 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})) |
71 | 24 | funfnd 6213 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → 𝐹 Fn dom 𝐹) |
72 | | sseq1 3878 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐹‘𝑝) → (𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))) |
73 | 72 | ralrn 6673 |
. . . . . . . . 9
⊢ (𝐹 Fn dom 𝐹 → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))) |
74 | 71, 73 | syl 17 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))) |
75 | 70, 74 | mpbird 249 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅})) |
76 | | pwssb 4883 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ 𝒫
(𝒫 dom 𝐹 ∖
{∅}) ↔ ∀𝑥
∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖
{∅})) |
77 | 75, 76 | sylibr 226 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖
{∅})) |
78 | | simpl 475 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → (𝐹‘𝑝) ≠ ∅) |
79 | 78 | ralimi 3104 |
. . . . . . . . 9
⊢
(∀𝑝 ∈
dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) |
80 | 79 | 3ad2ant3 1115 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) |
81 | 24, 80 | jca 504 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅)) |
82 | | elrnrexdm 6674 |
. . . . . . . . . 10
⊢ (Fun
𝐹 → (∅ ∈
ran 𝐹 → ∃𝑝 ∈ dom 𝐹∅ = (𝐹‘𝑝))) |
83 | | nesym 3017 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑝) ≠ ∅ ↔ ¬ ∅ = (𝐹‘𝑝)) |
84 | 83 | ralbii 3109 |
. . . . . . . . . . 11
⊢
(∀𝑝 ∈
dom 𝐹(𝐹‘𝑝) ≠ ∅ ↔ ∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹‘𝑝)) |
85 | | ralnex 3177 |
. . . . . . . . . . 11
⊢
(∀𝑝 ∈
dom 𝐹 ¬ ∅ =
(𝐹‘𝑝) ↔ ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹‘𝑝)) |
86 | 84, 85 | sylbb 211 |
. . . . . . . . . 10
⊢
(∀𝑝 ∈
dom 𝐹(𝐹‘𝑝) ≠ ∅ → ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹‘𝑝)) |
87 | 82, 86 | nsyli 157 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ → ¬ ∅ ∈
ran 𝐹)) |
88 | 87 | imp 398 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) → ¬ ∅ ∈
ran 𝐹) |
89 | | disjsn 4515 |
. . . . . . . 8
⊢ ((ran
𝐹 ∩ {∅}) =
∅ ↔ ¬ ∅ ∈ ran 𝐹) |
90 | 88, 89 | sylibr 226 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) → (ran 𝐹 ∩ {∅}) =
∅) |
91 | 81, 90 | syl 17 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (ran 𝐹 ∩ {∅}) =
∅) |
92 | | reldisj 4279 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ 𝒫
(𝒫 dom 𝐹 ∖
{∅}) → ((ran 𝐹
∩ {∅}) = ∅ ↔ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅}))) |
93 | 92 | biimpd 221 |
. . . . . 6
⊢ (ran
𝐹 ⊆ 𝒫
(𝒫 dom 𝐹 ∖
{∅}) → ((ran 𝐹
∩ {∅}) = ∅ → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅}))) |
94 | 77, 91, 93 | sylc 65 |
. . . . 5
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) |
95 | 24, 94 | jca 504 |
. . . 4
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅}))) |
96 | 20 | biimpi 208 |
. . . . . 6
⊢
(∀𝑝 ∈
dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
97 | 96 | 3ad2ant3 1115 |
. . . . 5
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
98 | | simpr 477 |
. . . . 5
⊢
((∀𝑝 ∈
dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) |
99 | 97, 98 | syl 17 |
. . . 4
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) |
100 | 95, 99 | jca 504 |
. . 3
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) ∧ ∀𝑝
∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
101 | 23, 100 | impbii 201 |
. 2
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))) |
102 | 2, 101 | syl6bb 279 |
1
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))))) |