| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
| 2 | | meetfval.m |
. . 3
⊢ ∧ =
(meet‘𝐾) |
| 3 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘𝐾)
∈ V |
| 4 | | moeq 3713 |
. . . . . . . 8
⊢
∃*𝑧 𝑧 = (𝐺‘{𝑥, 𝑦}) |
| 5 | 4 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → ∃*𝑧 𝑧 = (𝐺‘{𝑥, 𝑦})) |
| 6 | | eqid 2737 |
. . . . . . 7
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} |
| 7 | 3, 3, 5, 6 | oprabex 8001 |
. . . . . 6
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} ∈ V |
| 8 | 7 | a1i 11 |
. . . . 5
⊢ (𝐾 ∈ V →
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))} ∈ V) |
| 9 | | meetfval.u |
. . . . . . . . . . . 12
⊢ 𝐺 = (glb‘𝐾) |
| 10 | 9 | glbfun 18410 |
. . . . . . . . . . 11
⊢ Fun 𝐺 |
| 11 | | funbrfv2b 6966 |
. . . . . . . . . . 11
⊢ (Fun
𝐺 → ({𝑥, 𝑦}𝐺𝑧 ↔ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ (𝐺‘{𝑥, 𝑦}) = 𝑧))) |
| 12 | 10, 11 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({𝑥, 𝑦}𝐺𝑧 ↔ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ (𝐺‘{𝑥, 𝑦}) = 𝑧)) |
| 13 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 14 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(le‘𝐾) =
(le‘𝐾) |
| 15 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ V ∧ {𝑥, 𝑦} ∈ dom 𝐺) → 𝐾 ∈ V) |
| 16 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ V ∧ {𝑥, 𝑦} ∈ dom 𝐺) → {𝑥, 𝑦} ∈ dom 𝐺) |
| 17 | 13, 14, 9, 15, 16 | glbelss 18412 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ V ∧ {𝑥, 𝑦} ∈ dom 𝐺) → {𝑥, 𝑦} ⊆ (Base‘𝐾)) |
| 18 | 17 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ V → ({𝑥, 𝑦} ∈ dom 𝐺 → {𝑥, 𝑦} ⊆ (Base‘𝐾))) |
| 19 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 20 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
| 21 | 19, 20 | prss 4820 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ↔ {𝑥, 𝑦} ⊆ (Base‘𝐾)) |
| 22 | 18, 21 | imbitrrdi 252 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ V → ({𝑥, 𝑦} ∈ dom 𝐺 → (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)))) |
| 23 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ ((𝐺‘{𝑥, 𝑦}) = 𝑧 ↔ 𝑧 = (𝐺‘{𝑥, 𝑦})) |
| 24 | 23 | biimpi 216 |
. . . . . . . . . . 11
⊢ ((𝐺‘{𝑥, 𝑦}) = 𝑧 → 𝑧 = (𝐺‘{𝑥, 𝑦})) |
| 25 | 22, 24 | anim12d1 610 |
. . . . . . . . . 10
⊢ (𝐾 ∈ V → (({𝑥, 𝑦} ∈ dom 𝐺 ∧ (𝐺‘{𝑥, 𝑦}) = 𝑧) → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
| 26 | 12, 25 | biimtrid 242 |
. . . . . . . . 9
⊢ (𝐾 ∈ V → ({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
| 27 | 26 | alrimiv 1927 |
. . . . . . . 8
⊢ (𝐾 ∈ V → ∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
| 28 | 27 | alrimiv 1927 |
. . . . . . 7
⊢ (𝐾 ∈ V → ∀𝑦∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
| 29 | 28 | alrimiv 1927 |
. . . . . 6
⊢ (𝐾 ∈ V → ∀𝑥∀𝑦∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦})))) |
| 30 | | ssoprab2 7501 |
. . . . . 6
⊢
(∀𝑥∀𝑦∀𝑧({𝑥, 𝑦}𝐺𝑧 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))}) |
| 31 | 29, 30 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ V →
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))}) |
| 32 | 8, 31 | ssexd 5324 |
. . . 4
⊢ (𝐾 ∈ V →
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ∈ V) |
| 33 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑝 = 𝐾 → (glb‘𝑝) = (glb‘𝐾)) |
| 34 | 33, 9 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑝 = 𝐾 → (glb‘𝑝) = 𝐺) |
| 35 | 34 | breqd 5154 |
. . . . . 6
⊢ (𝑝 = 𝐾 → ({𝑥, 𝑦} (glb‘𝑝)𝑧 ↔ {𝑥, 𝑦}𝐺𝑧)) |
| 36 | 35 | oprabbidv 7499 |
. . . . 5
⊢ (𝑝 = 𝐾 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
| 37 | | df-meet 18394 |
. . . . 5
⊢ meet =
(𝑝 ∈ V ↦
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧}) |
| 38 | 36, 37 | fvmptg 7014 |
. . . 4
⊢ ((𝐾 ∈ V ∧
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧} ∈ V) → (meet‘𝐾) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
| 39 | 32, 38 | mpdan 687 |
. . 3
⊢ (𝐾 ∈ V →
(meet‘𝐾) =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
| 40 | 2, 39 | eqtrid 2789 |
. 2
⊢ (𝐾 ∈ V → ∧ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |
| 41 | 1, 40 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → ∧ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) |