Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
2 | | meetfval.m |
. . 3
⊢ ∧ =
(meet‘𝐾) |
3 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝐾)
∈ V |
4 | | moeq 3382 |
. . . . . . . 8
⊢
∃*𝑧 𝑧 = (𝐺‘{𝑥, 𝑦}) |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → ∃*𝑧 𝑧 = (𝐺‘{𝑥, 𝑦})) |
6 | | eqid 2622 |
. . . . . . 7
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} |
7 | 3, 3, 5, 6 | oprabex 7156 |
. . . . . 6
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} ∈ V |
8 | 7 | a1i 11 |
. . . . 5
⊢ (𝐾 ∈ V →
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} ∈ V) |
9 | | meetfval.u |
. . . . . . . . . . . 12
⊢ 𝐺 = (glb‘𝐾) |
10 | 9 | glbfun 16993 |
. . . . . . . . . . 11
⊢ Fun 𝐺 |
11 | | funbrfv2b 6240 |
. . . . . . . . . . 11
⊢ (Fun
𝐺 → ({𝑥, 𝑦}𝐺𝑧 ↔ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ (𝐺‘{𝑥, 𝑦}) = 𝑧))) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({𝑥, 𝑦}𝐺𝑧 ↔ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ (𝐺‘{𝑥, 𝑦}) = 𝑧)) |
13 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐾) =
(Base‘𝐾) |
14 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(le‘𝐾) =
(le‘𝐾) |
15 | | simpl 473 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ V ∧ {𝑥, 𝑦} ∈ dom 𝐺) → 𝐾 ∈ V) |
16 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ V ∧ {𝑥, 𝑦} ∈ dom 𝐺) → {𝑥, 𝑦} ∈ dom 𝐺) |
17 | 13, 14, 9, 15, 16 | glbelss 16995 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ V ∧ {𝑥, 𝑦} ∈ dom 𝐺) → {𝑥, 𝑦} ⊆ (Base‘𝐾)) |
18 | 17 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ V → ({𝑥, 𝑦} ∈ dom 𝐺 → {𝑥, 𝑦} ⊆ (Base‘𝐾))) |
19 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
20 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
21 | 19, 20 | prss 4351 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ↔ {𝑥, 𝑦} ⊆ (Base‘𝐾)) |
22 | 18, 21 | syl6ibr 242 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ V → ({𝑥, 𝑦} ∈ dom 𝐺 → (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)))) |
23 | | eqcom 2629 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘{𝑥, 𝑦}) = 𝑧 ↔ 𝑧 = (𝐺‘{𝑥, 𝑦})) |
24 | 23 | biimpi 206 |
. . . . . . . . . . . 12
⊢ ((𝐺‘{𝑥, 𝑦}) = 𝑧 → 𝑧 = (𝐺‘{𝑥, 𝑦})) |
25 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ V → ((𝐺‘{𝑥, 𝑦}) = 𝑧 → 𝑧 = (𝐺‘{𝑥, 𝑦}))) |
26 | 22, 25 | anim12d 586 |
. . . . . . . . . 10
⊢ (𝐾 ∈ V → (({𝑥, 𝑦} ∈ dom 𝐺 ∧ (𝐺‘{𝑥, 𝑦}) = 𝑧) → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
27 | 12, 26 | syl5bi 232 |
. . . . . . . . 9
⊢ (𝐾 ∈ V → ({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
28 | 27 | alrimiv 1855 |
. . . . . . . 8
⊢ (𝐾 ∈ V → ∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
29 | 28 | alrimiv 1855 |
. . . . . . 7
⊢ (𝐾 ∈ V → ∀𝑦∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
30 | 29 | alrimiv 1855 |
. . . . . 6
⊢ (𝐾 ∈ V → ∀𝑥∀𝑦∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
31 | | ssoprab2 6711 |
. . . . . 6
⊢
(∀𝑥∀𝑦∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))}) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ V →
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))}) |
33 | 8, 32 | ssexd 4805 |
. . . 4
⊢ (𝐾 ∈ V →
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ∈ V) |
34 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑝 = 𝐾 → (glb‘𝑝) = (glb‘𝐾)) |
35 | 34, 9 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑝 = 𝐾 → (glb‘𝑝) = 𝐺) |
36 | 35 | breqd 4664 |
. . . . . 6
⊢ (𝑝 = 𝐾 → ({𝑥, 𝑦} (glb‘𝑝)𝑧 ↔ {𝑥, 𝑦}𝐺𝑧)) |
37 | 36 | oprabbidv 6709 |
. . . . 5
⊢ (𝑝 = 𝐾 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
38 | | df-meet 16977 |
. . . . 5
⊢ meet =
(𝑝 ∈ V ↦
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧}) |
39 | 37, 38 | fvmptg 6280 |
. . . 4
⊢ ((𝐾 ∈ V ∧
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ∈ V) → (meet‘𝐾) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
40 | 33, 39 | mpdan 702 |
. . 3
⊢ (𝐾 ∈ V →
(meet‘𝐾) =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
41 | 2, 40 | syl5eq 2668 |
. 2
⊢ (𝐾 ∈ V → ∧ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
42 | 1, 41 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → ∧ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |