Proof of Theorem gneispacess2
Step | Hyp | Ref
| Expression |
1 | | gneispace.a |
. . . . 5
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖
{∅}) ∧ ∀𝑝
∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} |
2 | 1 | gneispacess 41708 |
. . . 4
⊢ (𝐹 ∈ 𝐴 → ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))) |
3 | | fveq2 6768 |
. . . . . 6
⊢ (𝑝 = 𝑃 → (𝐹‘𝑝) = (𝐹‘𝑃)) |
4 | 3 | eleq2d 2825 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑠 ∈ (𝐹‘𝑝) ↔ 𝑠 ∈ (𝐹‘𝑃))) |
5 | 4 | imbi2d 340 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → ((𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)) ↔ (𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)))) |
6 | 5 | ralbidv 3122 |
. . . . . 6
⊢ (𝑝 = 𝑃 → (∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)) ↔ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)))) |
7 | 3, 6 | raleqbidv 3334 |
. . . . 5
⊢ (𝑝 = 𝑃 → (∀𝑛 ∈ (𝐹‘𝑝)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)) ↔ ∀𝑛 ∈ (𝐹‘𝑃)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)))) |
8 | 7 | rspccv 3557 |
. . . 4
⊢
(∀𝑝 ∈
dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)) → (𝑃 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹‘𝑃)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)))) |
9 | 2, 8 | syl 17 |
. . 3
⊢ (𝐹 ∈ 𝐴 → (𝑃 ∈ dom 𝐹 → ∀𝑛 ∈ (𝐹‘𝑃)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)))) |
10 | | sseq1 3950 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑛 ⊆ 𝑠 ↔ 𝑁 ⊆ 𝑠)) |
11 | 10 | imbi1d 341 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)) ↔ (𝑁 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)))) |
12 | 11 | ralbidv 3122 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)) ↔ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑁 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)))) |
13 | 12 | rspccv 3557 |
. . . . 5
⊢
(∀𝑛 ∈
(𝐹‘𝑃)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)) → (𝑁 ∈ (𝐹‘𝑃) → ∀𝑠 ∈ 𝒫 dom 𝐹(𝑁 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)))) |
14 | | sseq2 3951 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (𝑁 ⊆ 𝑠 ↔ 𝑁 ⊆ 𝑆)) |
15 | | eleq1 2827 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (𝑠 ∈ (𝐹‘𝑃) ↔ 𝑆 ∈ (𝐹‘𝑃))) |
16 | 14, 15 | imbi12d 344 |
. . . . . 6
⊢ (𝑠 = 𝑆 → ((𝑁 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)) ↔ (𝑁 ⊆ 𝑆 → 𝑆 ∈ (𝐹‘𝑃)))) |
17 | 16 | rspccv 3557 |
. . . . 5
⊢
(∀𝑠 ∈
𝒫 dom 𝐹(𝑁 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)) → (𝑆 ∈ 𝒫 dom 𝐹 → (𝑁 ⊆ 𝑆 → 𝑆 ∈ (𝐹‘𝑃)))) |
18 | 13, 17 | syl6 35 |
. . . 4
⊢
(∀𝑛 ∈
(𝐹‘𝑃)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)) → (𝑁 ∈ (𝐹‘𝑃) → (𝑆 ∈ 𝒫 dom 𝐹 → (𝑁 ⊆ 𝑆 → 𝑆 ∈ (𝐹‘𝑃))))) |
19 | 18 | 3impd 1346 |
. . 3
⊢
(∀𝑛 ∈
(𝐹‘𝑃)∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑃)) → ((𝑁 ∈ (𝐹‘𝑃) ∧ 𝑆 ∈ 𝒫 dom 𝐹 ∧ 𝑁 ⊆ 𝑆) → 𝑆 ∈ (𝐹‘𝑃))) |
20 | 9, 19 | syl6 35 |
. 2
⊢ (𝐹 ∈ 𝐴 → (𝑃 ∈ dom 𝐹 → ((𝑁 ∈ (𝐹‘𝑃) ∧ 𝑆 ∈ 𝒫 dom 𝐹 ∧ 𝑁 ⊆ 𝑆) → 𝑆 ∈ (𝐹‘𝑃)))) |
21 | 20 | imp31 417 |
1
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹) ∧ (𝑁 ∈ (𝐹‘𝑃) ∧ 𝑆 ∈ 𝒫 dom 𝐹 ∧ 𝑁 ⊆ 𝑆)) → 𝑆 ∈ (𝐹‘𝑃)) |