Step | Hyp | Ref
| Expression |
1 | | elex 3449 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
2 | | meetfval.m |
. . 3
⊢ ∧ =
(meet‘𝐾) |
3 | | fvex 6782 |
. . . . . . 7
⊢
(Base‘𝐾)
∈ V |
4 | | moeq 3646 |
. . . . . . . 8
⊢
∃*𝑧 𝑧 = (𝐺‘{𝑥, 𝑦}) |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → ∃*𝑧 𝑧 = (𝐺‘{𝑥, 𝑦})) |
6 | | eqid 2740 |
. . . . . . 7
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} |
7 | 3, 3, 5, 6 | oprabex 7810 |
. . . . . 6
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} ∈ V |
8 | 7 | a1i 11 |
. . . . 5
⊢ (𝐾 ∈ V →
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} ∈ V) |
9 | | meetfval.u |
. . . . . . . . . . . 12
⊢ 𝐺 = (glb‘𝐾) |
10 | 9 | glbfun 18079 |
. . . . . . . . . . 11
⊢ Fun 𝐺 |
11 | | funbrfv2b 6822 |
. . . . . . . . . . 11
⊢ (Fun
𝐺 → ({𝑥, 𝑦}𝐺𝑧 ↔ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ (𝐺‘{𝑥, 𝑦}) = 𝑧))) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({𝑥, 𝑦}𝐺𝑧 ↔ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ (𝐺‘{𝑥, 𝑦}) = 𝑧)) |
13 | | eqid 2740 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐾) =
(Base‘𝐾) |
14 | | eqid 2740 |
. . . . . . . . . . . . . 14
⊢
(le‘𝐾) =
(le‘𝐾) |
15 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ V ∧ {𝑥, 𝑦} ∈ dom 𝐺) → 𝐾 ∈ V) |
16 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ V ∧ {𝑥, 𝑦} ∈ dom 𝐺) → {𝑥, 𝑦} ∈ dom 𝐺) |
17 | 13, 14, 9, 15, 16 | glbelss 18081 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ V ∧ {𝑥, 𝑦} ∈ dom 𝐺) → {𝑥, 𝑦} ⊆ (Base‘𝐾)) |
18 | 17 | ex 413 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ V → ({𝑥, 𝑦} ∈ dom 𝐺 → {𝑥, 𝑦} ⊆ (Base‘𝐾))) |
19 | | vex 3435 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
20 | | vex 3435 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
21 | 19, 20 | prss 4759 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ↔ {𝑥, 𝑦} ⊆ (Base‘𝐾)) |
22 | 18, 21 | syl6ibr 251 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ V → ({𝑥, 𝑦} ∈ dom 𝐺 → (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)))) |
23 | | eqcom 2747 |
. . . . . . . . . . . 12
⊢ ((𝐺‘{𝑥, 𝑦}) = 𝑧 ↔ 𝑧 = (𝐺‘{𝑥, 𝑦})) |
24 | 23 | biimpi 215 |
. . . . . . . . . . 11
⊢ ((𝐺‘{𝑥, 𝑦}) = 𝑧 → 𝑧 = (𝐺‘{𝑥, 𝑦})) |
25 | 22, 24 | anim12d1 610 |
. . . . . . . . . 10
⊢ (𝐾 ∈ V → (({𝑥, 𝑦} ∈ dom 𝐺 ∧ (𝐺‘{𝑥, 𝑦}) = 𝑧) → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
26 | 12, 25 | syl5bi 241 |
. . . . . . . . 9
⊢ (𝐾 ∈ V → ({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
27 | 26 | alrimiv 1934 |
. . . . . . . 8
⊢ (𝐾 ∈ V → ∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
28 | 27 | alrimiv 1934 |
. . . . . . 7
⊢ (𝐾 ∈ V → ∀𝑦∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
29 | 28 | alrimiv 1934 |
. . . . . 6
⊢ (𝐾 ∈ V → ∀𝑥∀𝑦∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
30 | | ssoprab2 7335 |
. . . . . 6
⊢
(∀𝑥∀𝑦∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))}) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ V →
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))}) |
32 | 8, 31 | ssexd 5252 |
. . . 4
⊢ (𝐾 ∈ V →
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ∈ V) |
33 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑝 = 𝐾 → (glb‘𝑝) = (glb‘𝐾)) |
34 | 33, 9 | eqtr4di 2798 |
. . . . . . 7
⊢ (𝑝 = 𝐾 → (glb‘𝑝) = 𝐺) |
35 | 34 | breqd 5090 |
. . . . . 6
⊢ (𝑝 = 𝐾 → ({𝑥, 𝑦} (glb‘𝑝)𝑧 ↔ {𝑥, 𝑦}𝐺𝑧)) |
36 | 35 | oprabbidv 7333 |
. . . . 5
⊢ (𝑝 = 𝐾 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
37 | | df-meet 18063 |
. . . . 5
⊢ meet =
(𝑝 ∈ V ↦
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧}) |
38 | 36, 37 | fvmptg 6868 |
. . . 4
⊢ ((𝐾 ∈ V ∧
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ∈ V) → (meet‘𝐾) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
39 | 32, 38 | mpdan 684 |
. . 3
⊢ (𝐾 ∈ V →
(meet‘𝐾) =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
40 | 2, 39 | eqtrid 2792 |
. 2
⊢ (𝐾 ∈ V → ∧ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
41 | 1, 40 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → ∧ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |