Step | Hyp | Ref
| Expression |
1 | | 0ex 5175 |
. . 3
⊢ ∅
∈ V |
2 | | eqid 2738 |
. . . 4
⊢
(glb‘∅) = (glb‘∅) |
3 | | eqid 2738 |
. . . 4
⊢
(meet‘∅) = (meet‘∅) |
4 | 2, 3 | meetfval 17741 |
. . 3
⊢ (∅
∈ V → (meet‘∅) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘∅)𝑧}) |
5 | 1, 4 | ax-mp 5 |
. 2
⊢
(meet‘∅) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘∅)𝑧} |
6 | | df-oprab 7174 |
. . 3
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘∅)𝑧} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧)} |
7 | | br0 5079 |
. . . . . . . . 9
⊢ ¬
{𝑥, 𝑦}∅𝑧 |
8 | | base0 16639 |
. . . . . . . . . . . . 13
⊢ ∅ =
(Base‘∅) |
9 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(le‘∅) = (le‘∅) |
10 | | biid 264 |
. . . . . . . . . . . . 13
⊢
((∀𝑧 ∈
𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)) ↔ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))) |
11 | | id 22 |
. . . . . . . . . . . . 13
⊢ (∅
∈ V → ∅ ∈ V) |
12 | 8, 9, 2, 10, 11 | glbfval 17717 |
. . . . . . . . . . . 12
⊢ (∅
∈ V → (glb‘∅) = ((𝑥 ∈ 𝒫 ∅ ↦
(℩𝑦 ∈
∅ (∀𝑧 ∈
𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))})) |
13 | 1, 12 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(glb‘∅) = ((𝑥 ∈ 𝒫 ∅ ↦
(℩𝑦 ∈
∅ (∀𝑧 ∈
𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))}) |
14 | | reu0 4247 |
. . . . . . . . . . . . . 14
⊢ ¬
∃!𝑦 ∈ ∅
(∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)) |
15 | 14 | abf 4291 |
. . . . . . . . . . . . 13
⊢ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))} = ∅ |
16 | 15 | reseq2i 5822 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 ∅
↦ (℩𝑦
∈ ∅ (∀𝑧
∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))}) = ((𝑥 ∈ 𝒫 ∅ ↦
(℩𝑦 ∈
∅ (∀𝑧 ∈
𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ ∅) |
17 | | res0 5829 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 ∅
↦ (℩𝑦
∈ ∅ (∀𝑧
∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ ∅) =
∅ |
18 | 16, 17 | eqtri 2761 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 ∅
↦ (℩𝑦
∈ ∅ (∀𝑧
∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))}) = ∅ |
19 | 13, 18 | eqtri 2761 |
. . . . . . . . . 10
⊢
(glb‘∅) = ∅ |
20 | 19 | breqi 5036 |
. . . . . . . . 9
⊢ ({𝑥, 𝑦} (glb‘∅)𝑧 ↔ {𝑥, 𝑦}∅𝑧) |
21 | 7, 20 | mtbir 326 |
. . . . . . . 8
⊢ ¬
{𝑥, 𝑦} (glb‘∅)𝑧 |
22 | 21 | intnan 490 |
. . . . . . 7
⊢ ¬
(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧) |
23 | 22 | nex 1807 |
. . . . . 6
⊢ ¬
∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧) |
24 | 23 | nex 1807 |
. . . . 5
⊢ ¬
∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧) |
25 | 24 | nex 1807 |
. . . 4
⊢ ¬
∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧) |
26 | 25 | abf 4291 |
. . 3
⊢ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧)} = ∅ |
27 | 6, 26 | eqtri 2761 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘∅)𝑧} = ∅ |
28 | 5, 27 | eqtri 2761 |
1
⊢
(meet‘∅) = ∅ |