Proof of Theorem gneispace2
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
⊢ (𝑓 = 𝐹 → 𝑓 = 𝐹) |
2 | | dmeq 5781 |
. . . 4
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) |
3 | 2 | pweqd 4541 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → 𝒫 dom 𝑓 = 𝒫 dom 𝐹) |
4 | 3 | difeq1d 4045 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝒫 dom 𝑓 ∖ {∅}) = (𝒫 dom 𝐹 ∖
{∅})) |
5 | 4 | pweqd 4541 |
. . . . 5
⊢ (𝑓 = 𝐹 → 𝒫 (𝒫 dom 𝑓 ∖ {∅}) = 𝒫
(𝒫 dom 𝐹 ∖
{∅})) |
6 | 5 | difeq1d 4045 |
. . . 4
⊢ (𝑓 = 𝐹 → (𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖
{∅}) = (𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅})) |
7 | 1, 2, 6 | feq123d 6543 |
. . 3
⊢ (𝑓 = 𝐹 → (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖
{∅}) ↔ 𝐹:dom
𝐹⟶(𝒫
(𝒫 dom 𝐹 ∖
{∅}) ∖ {∅}))) |
8 | | fveq1 6725 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑓‘𝑝) = (𝐹‘𝑝)) |
9 | 8 | eleq2d 2824 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑠 ∈ (𝑓‘𝑝) ↔ 𝑠 ∈ (𝐹‘𝑝))) |
10 | 9 | imbi2d 344 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝)) ↔ (𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) |
11 | 3, 10 | raleqbidv 3320 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝)) ↔ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))) |
12 | 11 | anbi2d 632 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))) ↔ (𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
13 | 8, 12 | raleqbidv 3320 |
. . . 4
⊢ (𝑓 = 𝐹 → (∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))) ↔ ∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
14 | 2, 13 | raleqbidv 3320 |
. . 3
⊢ (𝑓 = 𝐹 → (∀𝑝 ∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))) ↔ ∀𝑝 ∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝))))) |
15 | 7, 14 | anbi12d 634 |
. 2
⊢ (𝑓 = 𝐹 → ((𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖
{∅}) ∧ ∀𝑝
∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝)))) ↔ (𝐹:dom 𝐹⟶(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅}) ∧ ∀𝑝
∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))) |
16 | | gneispace.a |
. 2
⊢ 𝐴 = {𝑓 ∣ (𝑓:dom 𝑓⟶(𝒫 (𝒫 dom 𝑓 ∖ {∅}) ∖
{∅}) ∧ ∀𝑝
∈ dom 𝑓∀𝑛 ∈ (𝑓‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝑓(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝑓‘𝑝))))} |
17 | 15, 16 | elab2g 3596 |
1
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐴 ↔ (𝐹:dom 𝐹⟶(𝒫 (𝒫 dom 𝐹 ∖ {∅}) ∖
{∅}) ∧ ∀𝑝
∈ dom 𝐹∀𝑛 ∈ (𝐹‘𝑝)(𝑝 ∈ 𝑛 ∧ ∀𝑠 ∈ 𝒫 dom 𝐹(𝑛 ⊆ 𝑠 → 𝑠 ∈ (𝐹‘𝑝)))))) |