Step | Hyp | Ref
| Expression |
1 | | gneispace.a |
. . 3
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖
{∅}) ∧ ∀𝑝
∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} |
2 | 1 | gneispace3 38431 |
. 2
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) ∧ ∀𝑝
∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))) |
3 | | simpll 790 |
. . . 4
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → Fun 𝐹) |
4 | | simplr 792 |
. . . . 5
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) |
5 | | difss 3737 |
. . . . . 6
⊢
(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})
⊆ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) |
6 | | difss 3737 |
. . . . . . 7
⊢
(𝒫 dom 𝐹
∖ {∅}) ⊆ 𝒫 dom 𝐹 |
7 | | sspwb 4917 |
. . . . . . 7
⊢
((𝒫 dom 𝐹
∖ {∅}) ⊆ 𝒫 dom 𝐹 ↔ 𝒫 (𝒫 dom 𝐹 ∖ {∅}) ⊆
𝒫 𝒫 dom 𝐹) |
8 | 6, 7 | mpbi 220 |
. . . . . 6
⊢ 𝒫
(𝒫 dom 𝐹 ∖
{∅}) ⊆ 𝒫 𝒫 dom 𝐹 |
9 | 5, 8 | sstri 3612 |
. . . . 5
⊢
(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖ {∅})
⊆ 𝒫 𝒫 dom 𝐹 |
10 | 4, 9 | syl6ss 3615 |
. . . 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 6352 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑝 ∈ dom 𝐹) → (𝐹‘𝑝) ∈ ran 𝐹) |
14 | 12, 13 | sylan 488 |
. . . . . . 7
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ 𝑝
∈ dom 𝐹) → (𝐹‘𝑝) ∈ ran 𝐹) |
15 | | ssel2 3598 |
. . . . . . . 8
⊢ ((ran
𝐹 ⊆ (𝒫
(𝒫 dom 𝐹 ∖
{∅}) ∖ {∅}) ∧ (𝐹‘𝑝) ∈ ran 𝐹) → (𝐹‘𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) |
16 | | eldifsni 4320 |
. . . . . . . 8
⊢ ((𝐹‘𝑝) ∈ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅}) → (𝐹‘𝑝) ≠ ∅) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ ((ran
𝐹 ⊆ (𝒫
(𝒫 dom 𝐹 ∖
{∅}) ∖ {∅}) ∧ (𝐹‘𝑝) ∈ ran 𝐹) → (𝐹‘𝑝) ≠ ∅) |
18 | 11, 14, 17 | syl2an2r 876 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ 𝑝
∈ dom 𝐹) → (𝐹‘𝑝) ≠ ∅) |
19 | 18 | ralrimiva 2966 |
. . . . 5
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) |
20 | | r19.26 3064 |
. . . . . 6
⊢
(∀𝑝 ∈
dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) ↔ (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
21 | 20 | biimpri 218 |
. . . . 5
⊢
((∀𝑝 ∈
dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
22 | 19, 21 | sylan 488 |
. . . 4
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
23 | 3, 10, 22 | 3jca 1242 |
. . 3
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))) |
24 | | simp1 1061 |
. . . . 5
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → Fun 𝐹) |
25 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑝Fun 𝐹 |
26 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑝ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 |
27 | | nfra1 2941 |
. . . . . . . . . 10
⊢
Ⅎ𝑝∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) |
28 | 25, 26, 27 | nf3an 1831 |
. . . . . . . . 9
⊢
Ⅎ𝑝(Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
29 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) |
30 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) → 𝑝 ∈ 𝑛) |
31 | | 19.8a 2052 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ 𝑛 → ∃𝑝 𝑝 ∈ 𝑛) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) → ∃𝑝 𝑝 ∈ 𝑛) |
33 | 32 | ralimi 2952 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
(𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛) |
34 | 29, 33 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛) |
35 | 34 | ralimi 2952 |
. . . . . . . . . . . . . 14
⊢
(∀𝑝 ∈
dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛) |
36 | 35 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛) |
37 | | rsp 2929 |
. . . . . . . . . . . . 13
⊢
(∀𝑝 ∈
dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛)) |
39 | | df-ex 1705 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∀𝑝 ¬ 𝑝 ∈ 𝑛) |
40 | 39 | ralbii 2980 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 ↔ ∀𝑛 ∈ (𝐹‘𝑝) ¬ ∀𝑝 ¬ 𝑝 ∈ 𝑛) |
41 | | ralnex 2992 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
(𝐹‘𝑝) ¬ ∀𝑝 ¬ 𝑝 ∈ 𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹‘𝑝)∀𝑝 ¬ 𝑝 ∈ 𝑛) |
42 | 40, 41 | bitri 264 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∃𝑛 ∈ (𝐹‘𝑝)∀𝑝 ¬ 𝑝 ∈ 𝑛) |
43 | | 0el 3939 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∈ (𝐹‘𝑝) ↔ ∃𝑛 ∈ (𝐹‘𝑝)∀𝑝 ¬ 𝑝 ∈ 𝑛) |
44 | 42, 43 | xchbinxr 325 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 ↔ ¬ ∅ ∈ (𝐹‘𝑝)) |
45 | 44 | biimpi 206 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → ¬ ∅ ∈ (𝐹‘𝑝)) |
46 | | elinel1 3799 |
. . . . . . . . . . . . . . 15
⊢ (∅
∈ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) → ∅ ∈ (𝐹‘𝑝)) |
47 | 45, 46 | nsyl 135 |
. . . . . . . . . . . . . 14
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → ¬ ∅ ∈ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹)) |
48 | | disjsn 4246 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ ↔ ¬
∅ ∈ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹)) |
49 | 47, 48 | sylibr 224 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) =
∅) |
50 | | disjdif2 4047 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∩ {∅}) = ∅ → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
(𝐹‘𝑝)∃𝑝 𝑝 ∈ 𝑛 → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹)) |
52 | 38, 51 | syl6 35 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹))) |
53 | | simp2 1062 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹) |
54 | 13 | ex 450 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → (𝑝 ∈ dom 𝐹 → (𝐹‘𝑝) ∈ ran 𝐹)) |
55 | 24, 54 | syl 17 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹‘𝑝) ∈ ran 𝐹)) |
56 | | ssel2 3598 |
. . . . . . . . . . . . 13
⊢ ((ran
𝐹 ⊆ 𝒫
𝒫 dom 𝐹 ∧
(𝐹‘𝑝) ∈ ran 𝐹) → (𝐹‘𝑝) ∈ 𝒫 𝒫 dom 𝐹) |
57 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑝) ∈ V |
58 | 57 | elpw 4164 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑝) ∈ 𝒫 𝒫 dom 𝐹 ↔ (𝐹‘𝑝) ⊆ 𝒫 dom 𝐹) |
59 | | df-ss 3588 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑝) ⊆ 𝒫 dom 𝐹 ↔ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) |
60 | 58, 59 | sylbb 209 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑝) ∈ 𝒫 𝒫 dom 𝐹 → ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) |
61 | 56, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ ((ran
𝐹 ⊆ 𝒫
𝒫 dom 𝐹 ∧
(𝐹‘𝑝) ∈ ran 𝐹) → ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) |
62 | 53, 55, 61 | syl6an 568 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝))) |
63 | 52, 62 | jcad 555 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → ((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)))) |
64 | | eqtr 2641 |
. . . . . . . . . . 11
⊢
(((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) → (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹‘𝑝)) |
65 | | df-ss 3588 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ((𝐹‘𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹‘𝑝)) |
66 | | indif2 3870 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) |
67 | 66 | eqeq1i 2627 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑝) ∩ (𝒫 dom 𝐹 ∖ {∅})) = (𝐹‘𝑝) ↔ (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹‘𝑝)) |
68 | 65, 67 | bitri 264 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = (𝐹‘𝑝)) |
69 | 64, 68 | sylibr 224 |
. . . . . . . . . 10
⊢
(((((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∖ {∅}) = ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) ∧ ((𝐹‘𝑝) ∩ 𝒫 dom 𝐹) = (𝐹‘𝑝)) → (𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})) |
70 | 63, 69 | syl6 35 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (𝑝 ∈ dom 𝐹 → (𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))) |
71 | 28, 70 | ralrimi 2957 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅})) |
72 | | funfn 5918 |
. . . . . . . . . . 11
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
73 | 72 | biimpi 206 |
. . . . . . . . . 10
⊢ (Fun
𝐹 → 𝐹 Fn dom 𝐹) |
74 | 24, 73 | syl 17 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → 𝐹 Fn dom 𝐹) |
75 | | sseq1 3626 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐹‘𝑝) → (𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ (𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))) |
76 | 75 | ralrn 6362 |
. . . . . . . . 9
⊢ (𝐹 Fn dom 𝐹 → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))) |
77 | 74, 76 | syl 17 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅}) ↔ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ⊆ (𝒫 dom 𝐹 ∖ {∅}))) |
78 | 71, 77 | mpbird 247 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑥 ∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖ {∅})) |
79 | | pwssb 4612 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ 𝒫
(𝒫 dom 𝐹 ∖
{∅}) ↔ ∀𝑥
∈ ran 𝐹 𝑥 ⊆ (𝒫 dom 𝐹 ∖
{∅})) |
80 | 78, 79 | sylibr 224 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ran 𝐹 ⊆ 𝒫 (𝒫 dom 𝐹 ∖
{∅})) |
81 | | simpl 473 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → (𝐹‘𝑝) ≠ ∅) |
82 | 81 | ralimi 2952 |
. . . . . . . . 9
⊢
(∀𝑝 ∈
dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) |
83 | 82 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) |
84 | 24, 83 | jca 554 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (Fun 𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅)) |
85 | | elrnrexdm 6363 |
. . . . . . . . . 10
⊢ (Fun
𝐹 → (∅ ∈
ran 𝐹 → ∃𝑝 ∈ dom 𝐹∅ = (𝐹‘𝑝))) |
86 | | nesym 2850 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑝) ≠ ∅ ↔ ¬ ∅ = (𝐹‘𝑝)) |
87 | 86 | ralbii 2980 |
. . . . . . . . . . 11
⊢
(∀𝑝 ∈
dom 𝐹(𝐹‘𝑝) ≠ ∅ ↔ ∀𝑝 ∈ dom 𝐹 ¬ ∅ = (𝐹‘𝑝)) |
88 | | ralnex 2992 |
. . . . . . . . . . 11
⊢
(∀𝑝 ∈
dom 𝐹 ¬ ∅ =
(𝐹‘𝑝) ↔ ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹‘𝑝)) |
89 | 87, 88 | sylbb 209 |
. . . . . . . . . 10
⊢
(∀𝑝 ∈
dom 𝐹(𝐹‘𝑝) ≠ ∅ → ¬ ∃𝑝 ∈ dom 𝐹∅ = (𝐹‘𝑝)) |
90 | 85, 89 | nsyli 155 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ → ¬ ∅ ∈
ran 𝐹)) |
91 | 90 | imp 445 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) → ¬ ∅ ∈
ran 𝐹) |
92 | | disjsn 4246 |
. . . . . . . 8
⊢ ((ran
𝐹 ∩ {∅}) =
∅ ↔ ¬ ∅ ∈ ran 𝐹) |
93 | 91, 92 | sylibr 224 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ ∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅) → (ran 𝐹 ∩ {∅}) =
∅) |
94 | 84, 93 | syl 17 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (ran 𝐹 ∩ {∅}) =
∅) |
95 | | reldisj 4020 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ 𝒫
(𝒫 dom 𝐹 ∖
{∅}) → ((ran 𝐹
∩ {∅}) = ∅ ↔ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅}))) |
96 | 95 | biimpd 219 |
. . . . . 6
⊢ (ran
𝐹 ⊆ 𝒫
(𝒫 dom 𝐹 ∖
{∅}) → ((ran 𝐹
∩ {∅}) = ∅ → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅}))) |
97 | 80, 94, 96 | sylc 65 |
. . . . 5
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) |
98 | 24, 97 | jca 554 |
. . . 4
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅}))) |
99 | 20 | biimpi 206 |
. . . . . 6
⊢
(∀𝑝 ∈
dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
100 | 99 | 3ad2ant3 1084 |
. . . . 5
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → (∀𝑝 ∈ dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
101 | | simpr 477 |
. . . . 5
⊢
((∀𝑝 ∈
dom 𝐹(𝐹‘𝑝) ≠ ∅ ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) |
102 | 100, 101 | syl 17 |
. . . 4
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) |
103 | 98, 102 | jca 554 |
. . 3
⊢ ((Fun
𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom
𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) → ((Fun 𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) ∧ ∀𝑝
∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
104 | 23, 103 | impbii 199 |
. 2
⊢ (((Fun
𝐹 ∧ ran 𝐹 ⊆ (𝒫 (𝒫
dom 𝐹 ∖ {∅})
∖ {∅})) ∧ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))) |
105 | 2, 104 | syl6bb 276 |
1
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ (Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀𝑝 ∈ dom 𝐹((𝐹‘𝑝) ≠ ∅ ∧ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))))) |