Step |
Hyp |
Ref |
Expression |
1 |
|
meetfval.u |
⊢ 𝐺 = ( glb ‘ 𝐾 ) |
2 |
|
meetfval.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
3 |
|
elex |
⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V ) |
4 |
|
fvex |
⊢ ( Base ‘ 𝐾 ) ∈ V |
5 |
|
moeq |
⊢ ∃* 𝑧 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) |
6 |
5
|
a1i |
⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ∃* 𝑧 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) |
7 |
|
eqid |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } |
8 |
4 4 6 7
|
oprabex |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } ∈ V |
9 |
8
|
a1i |
⊢ ( 𝐾 ∈ V → { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } ∈ V ) |
10 |
1
|
glbfun |
⊢ Fun 𝐺 |
11 |
|
funbrfv2b |
⊢ ( Fun 𝐺 → ( { 𝑥 , 𝑦 } 𝐺 𝑧 ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) ) ) |
12 |
10 11
|
ax-mp |
⊢ ( { 𝑥 , 𝑦 } 𝐺 𝑧 ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) ) |
13 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
14 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
15 |
|
simpl |
⊢ ( ( 𝐾 ∈ V ∧ { 𝑥 , 𝑦 } ∈ dom 𝐺 ) → 𝐾 ∈ V ) |
16 |
|
simpr |
⊢ ( ( 𝐾 ∈ V ∧ { 𝑥 , 𝑦 } ∈ dom 𝐺 ) → { 𝑥 , 𝑦 } ∈ dom 𝐺 ) |
17 |
13 14 1 15 16
|
glbelss |
⊢ ( ( 𝐾 ∈ V ∧ { 𝑥 , 𝑦 } ∈ dom 𝐺 ) → { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝐾 ) ) |
18 |
17
|
ex |
⊢ ( 𝐾 ∈ V → ( { 𝑥 , 𝑦 } ∈ dom 𝐺 → { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝐾 ) ) ) |
19 |
|
vex |
⊢ 𝑥 ∈ V |
20 |
|
vex |
⊢ 𝑦 ∈ V |
21 |
19 20
|
prss |
⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ↔ { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝐾 ) ) |
22 |
18 21
|
syl6ibr |
⊢ ( 𝐾 ∈ V → ( { 𝑥 , 𝑦 } ∈ dom 𝐺 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ) |
23 |
|
eqcom |
⊢ ( ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ↔ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) |
24 |
23
|
biimpi |
⊢ ( ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = 𝑧 → 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) |
25 |
22 24
|
anim12d1 |
⊢ ( 𝐾 ∈ V → ( ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) ) ) |
26 |
12 25
|
syl5bi |
⊢ ( 𝐾 ∈ V → ( { 𝑥 , 𝑦 } 𝐺 𝑧 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) ) ) |
27 |
26
|
alrimiv |
⊢ ( 𝐾 ∈ V → ∀ 𝑧 ( { 𝑥 , 𝑦 } 𝐺 𝑧 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) ) ) |
28 |
27
|
alrimiv |
⊢ ( 𝐾 ∈ V → ∀ 𝑦 ∀ 𝑧 ( { 𝑥 , 𝑦 } 𝐺 𝑧 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) ) ) |
29 |
28
|
alrimiv |
⊢ ( 𝐾 ∈ V → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( { 𝑥 , 𝑦 } 𝐺 𝑧 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) ) ) |
30 |
|
ssoprab2 |
⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( { 𝑥 , 𝑦 } 𝐺 𝑧 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) ) → { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } ⊆ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } ) |
31 |
29 30
|
syl |
⊢ ( 𝐾 ∈ V → { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } ⊆ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } ) |
32 |
9 31
|
ssexd |
⊢ ( 𝐾 ∈ V → { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } ∈ V ) |
33 |
|
fveq2 |
⊢ ( 𝑝 = 𝐾 → ( glb ‘ 𝑝 ) = ( glb ‘ 𝐾 ) ) |
34 |
33 1
|
eqtr4di |
⊢ ( 𝑝 = 𝐾 → ( glb ‘ 𝑝 ) = 𝐺 ) |
35 |
34
|
breqd |
⊢ ( 𝑝 = 𝐾 → ( { 𝑥 , 𝑦 } ( glb ‘ 𝑝 ) 𝑧 ↔ { 𝑥 , 𝑦 } 𝐺 𝑧 ) ) |
36 |
35
|
oprabbidv |
⊢ ( 𝑝 = 𝐾 → { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } ( glb ‘ 𝑝 ) 𝑧 } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } ) |
37 |
|
df-meet |
⊢ meet = ( 𝑝 ∈ V ↦ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } ( glb ‘ 𝑝 ) 𝑧 } ) |
38 |
36 37
|
fvmptg |
⊢ ( ( 𝐾 ∈ V ∧ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } ∈ V ) → ( meet ‘ 𝐾 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } ) |
39 |
32 38
|
mpdan |
⊢ ( 𝐾 ∈ V → ( meet ‘ 𝐾 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } ) |
40 |
2 39
|
syl5eq |
⊢ ( 𝐾 ∈ V → ∧ = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } ) |
41 |
3 40
|
syl |
⊢ ( 𝐾 ∈ 𝑉 → ∧ = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } ) |