Step | Hyp | Ref
| Expression |
1 | | 0ex 5014 |
. . 3
⊢ ∅
∈ V |
2 | | base0 16275 |
. . . 4
⊢ ∅ =
(Base‘∅) |
3 | | 00lss 19298 |
. . . 4
⊢ ∅ =
(LSubSp‘∅) |
4 | | eqid 2825 |
. . . 4
⊢
(LSpan‘∅) = (LSpan‘∅) |
5 | 2, 3, 4 | lspfval 19332 |
. . 3
⊢ (∅
∈ V → (LSpan‘∅) = (𝑎 ∈ 𝒫 ∅ ↦ ∩ {𝑏
∈ ∅ ∣ 𝑎
⊆ 𝑏})) |
6 | 1, 5 | ax-mp 5 |
. 2
⊢
(LSpan‘∅) = (𝑎 ∈ 𝒫 ∅ ↦ ∩ {𝑏
∈ ∅ ∣ 𝑎
⊆ 𝑏}) |
7 | | eqid 2825 |
. . . . 5
⊢ (𝑎 ∈ 𝒫 ∅
↦ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏}) = (𝑎 ∈ 𝒫 ∅ ↦ ∩ {𝑏
∈ ∅ ∣ 𝑎
⊆ 𝑏}) |
8 | 7 | dmmpt 5871 |
. . . 4
⊢ dom
(𝑎 ∈ 𝒫 ∅
↦ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏}) = {𝑎 ∈ 𝒫 ∅ ∣ ∩ {𝑏
∈ ∅ ∣ 𝑎
⊆ 𝑏} ∈
V} |
9 | | vprc 5022 |
. . . . . . 7
⊢ ¬ V
∈ V |
10 | | rab0 4185 |
. . . . . . . . . 10
⊢ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏} = ∅ |
11 | 10 | inteqi 4701 |
. . . . . . . . 9
⊢ ∩ {𝑏
∈ ∅ ∣ 𝑎
⊆ 𝑏} = ∩ ∅ |
12 | | int0 4711 |
. . . . . . . . 9
⊢ ∩ ∅ = V |
13 | 11, 12 | eqtri 2849 |
. . . . . . . 8
⊢ ∩ {𝑏
∈ ∅ ∣ 𝑎
⊆ 𝑏} =
V |
14 | 13 | eleq1i 2897 |
. . . . . . 7
⊢ (∩ {𝑏
∈ ∅ ∣ 𝑎
⊆ 𝑏} ∈ V ↔
V ∈ V) |
15 | 9, 14 | mtbir 315 |
. . . . . 6
⊢ ¬
∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏} ∈ V |
16 | 15 | rgenw 3133 |
. . . . 5
⊢
∀𝑎 ∈
𝒫 ∅ ¬ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏} ∈ V |
17 | | rabeq0 4186 |
. . . . 5
⊢ ({𝑎 ∈ 𝒫 ∅
∣ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏} ∈ V} = ∅ ↔ ∀𝑎 ∈ 𝒫 ∅ ¬
∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏} ∈ V) |
18 | 16, 17 | mpbir 223 |
. . . 4
⊢ {𝑎 ∈ 𝒫 ∅
∣ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏} ∈ V} = ∅ |
19 | 8, 18 | eqtri 2849 |
. . 3
⊢ dom
(𝑎 ∈ 𝒫 ∅
↦ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏}) = ∅ |
20 | | funmpt 6161 |
. . . . 5
⊢ Fun
(𝑎 ∈ 𝒫 ∅
↦ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏}) |
21 | | funrel 6140 |
. . . . 5
⊢ (Fun
(𝑎 ∈ 𝒫 ∅
↦ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏}) → Rel (𝑎 ∈ 𝒫 ∅ ↦ ∩ {𝑏
∈ ∅ ∣ 𝑎
⊆ 𝑏})) |
22 | 20, 21 | ax-mp 5 |
. . . 4
⊢ Rel
(𝑎 ∈ 𝒫 ∅
↦ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏}) |
23 | | reldm0 5575 |
. . . 4
⊢ (Rel
(𝑎 ∈ 𝒫 ∅
↦ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏}) → ((𝑎 ∈ 𝒫 ∅ ↦ ∩ {𝑏
∈ ∅ ∣ 𝑎
⊆ 𝑏}) = ∅
↔ dom (𝑎 ∈
𝒫 ∅ ↦ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏}) = ∅)) |
24 | 22, 23 | ax-mp 5 |
. . 3
⊢ ((𝑎 ∈ 𝒫 ∅
↦ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏}) = ∅ ↔ dom (𝑎 ∈ 𝒫 ∅ ↦ ∩ {𝑏
∈ ∅ ∣ 𝑎
⊆ 𝑏}) =
∅) |
25 | 19, 24 | mpbir 223 |
. 2
⊢ (𝑎 ∈ 𝒫 ∅
↦ ∩ {𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏}) = ∅ |
26 | 6, 25 | eqtr2i 2850 |
1
⊢ ∅ =
(LSpan‘∅) |