Step | Hyp | Ref
| Expression |
1 | | 0ex 4790 |
. . 3
⊢ ∅
∈ V |
2 | | eqid 2622 |
. . . 4
⊢
(glb‘∅) = (glb‘∅) |
3 | | eqid 2622 |
. . . 4
⊢
(meet‘∅) = (meet‘∅) |
4 | 2, 3 | meetfval 17015 |
. . 3
⊢ (∅
∈ V → (meet‘∅) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘∅)𝑧}) |
5 | 1, 4 | ax-mp 5 |
. 2
⊢
(meet‘∅) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘∅)𝑧} |
6 | | df-oprab 6654 |
. . 3
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘∅)𝑧} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧)} |
7 | | br0 4701 |
. . . . . . . . 9
⊢ ¬
{𝑥, 𝑦}∅𝑧 |
8 | | base0 15912 |
. . . . . . . . . . . . 13
⊢ ∅ =
(Base‘∅) |
9 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(le‘∅) = (le‘∅) |
10 | | biid 251 |
. . . . . . . . . . . . 13
⊢
((∀𝑧 ∈
𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)) ↔ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))) |
11 | | id 22 |
. . . . . . . . . . . . 13
⊢ (∅
∈ V → ∅ ∈ V) |
12 | 8, 9, 2, 10, 11 | glbfval 16991 |
. . . . . . . . . . . 12
⊢ (∅
∈ V → (glb‘∅) = ((𝑥 ∈ 𝒫 ∅ ↦
(℩𝑦 ∈
∅ (∀𝑧 ∈
𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))})) |
13 | 1, 12 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(glb‘∅) = ((𝑥 ∈ 𝒫 ∅ ↦
(℩𝑦 ∈
∅ (∀𝑧 ∈
𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))}) |
14 | | rex0 3938 |
. . . . . . . . . . . . . . 15
⊢ ¬
∃𝑦 ∈ ∅
(∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)) |
15 | | reurex 3160 |
. . . . . . . . . . . . . . 15
⊢
(∃!𝑦 ∈
∅ (∀𝑧 ∈
𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)) → ∃𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))) |
16 | 14, 15 | mto 188 |
. . . . . . . . . . . . . 14
⊢ ¬
∃!𝑦 ∈ ∅
(∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)) |
17 | 16 | abf 3978 |
. . . . . . . . . . . . 13
⊢ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))} = ∅ |
18 | 17 | reseq2i 5393 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 ∅
↦ (℩𝑦
∈ ∅ (∀𝑧
∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))}) = ((𝑥 ∈ 𝒫 ∅ ↦
(℩𝑦 ∈
∅ (∀𝑧 ∈
𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ ∅) |
19 | | res0 5400 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 ∅
↦ (℩𝑦
∈ ∅ (∀𝑧
∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ ∅) =
∅ |
20 | 18, 19 | eqtri 2644 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 ∅
↦ (℩𝑦
∈ ∅ (∀𝑧
∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦)))) ↾ {𝑥 ∣ ∃!𝑦 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑦(le‘∅)𝑧 ∧ ∀𝑤 ∈ ∅ (∀𝑧 ∈ 𝑥 𝑤(le‘∅)𝑧 → 𝑤(le‘∅)𝑦))}) = ∅ |
21 | 13, 20 | eqtri 2644 |
. . . . . . . . . 10
⊢
(glb‘∅) = ∅ |
22 | 21 | breqi 4659 |
. . . . . . . . 9
⊢ ({𝑥, 𝑦} (glb‘∅)𝑧 ↔ {𝑥, 𝑦}∅𝑧) |
23 | 7, 22 | mtbir 313 |
. . . . . . . 8
⊢ ¬
{𝑥, 𝑦} (glb‘∅)𝑧 |
24 | 23 | intnan 960 |
. . . . . . 7
⊢ ¬
(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧) |
25 | 24 | nex 1731 |
. . . . . 6
⊢ ¬
∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧) |
26 | 25 | nex 1731 |
. . . . 5
⊢ ¬
∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧) |
27 | 26 | nex 1731 |
. . . 4
⊢ ¬
∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧) |
28 | 27 | abf 3978 |
. . 3
⊢ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ {𝑥, 𝑦} (glb‘∅)𝑧)} = ∅ |
29 | 6, 28 | eqtri 2644 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘∅)𝑧} = ∅ |
30 | 5, 29 | eqtri 2644 |
1
⊢
(meet‘∅) = ∅ |