Metamath Proof Explorer


Theorem meetval

Description: Meet value. Since both sides evaluate to (/) when they don't exist, for convenience we drop the { X , Y } e. dom G requirement. (Contributed by NM, 9-Sep-2018)

Ref Expression
Hypotheses meetdef.u G=glbK
meetdef.m ˙=meetK
meetdef.k φKV
meetdef.x φXW
meetdef.y φYZ
Assertion meetval φX˙Y=GXY

Proof

Step Hyp Ref Expression
1 meetdef.u G=glbK
2 meetdef.m ˙=meetK
3 meetdef.k φKV
4 meetdef.x φXW
5 meetdef.y φYZ
6 1 2 meetfval2 KV˙=xyz|xydomGz=Gxy
7 3 6 syl φ˙=xyz|xydomGz=Gxy
8 7 oveqd φX˙Y=Xxyz|xydomGz=GxyY
9 8 adantr φXYdomGX˙Y=Xxyz|xydomGz=GxyY
10 simpr φXYdomGXYdomG
11 eqidd φXYdomGGXY=GXY
12 fvexd φGXYV
13 preq12 x=Xy=Yxy=XY
14 13 eleq1d x=Xy=YxydomGXYdomG
15 14 3adant3 x=Xy=Yz=GXYxydomGXYdomG
16 simp3 x=Xy=Yz=GXYz=GXY
17 13 fveq2d x=Xy=YGxy=GXY
18 17 3adant3 x=Xy=Yz=GXYGxy=GXY
19 16 18 eqeq12d x=Xy=Yz=GXYz=GxyGXY=GXY
20 15 19 anbi12d x=Xy=Yz=GXYxydomGz=GxyXYdomGGXY=GXY
21 moeq *zz=Gxy
22 21 moani *zxydomGz=Gxy
23 eqid xyz|xydomGz=Gxy=xyz|xydomGz=Gxy
24 20 22 23 ovigg XWYZGXYVXYdomGGXY=GXYXxyz|xydomGz=GxyY=GXY
25 4 5 12 24 syl3anc φXYdomGGXY=GXYXxyz|xydomGz=GxyY=GXY
26 25 adantr φXYdomGXYdomGGXY=GXYXxyz|xydomGz=GxyY=GXY
27 10 11 26 mp2and φXYdomGXxyz|xydomGz=GxyY=GXY
28 9 27 eqtrd φXYdomGX˙Y=GXY
29 1 2 3 4 5 meetdef φXYdom˙XYdomG
30 29 notbid φ¬XYdom˙¬XYdomG
31 df-ov X˙Y=˙XY
32 ndmfv ¬XYdom˙˙XY=
33 31 32 eqtrid ¬XYdom˙X˙Y=
34 30 33 syl6bir φ¬XYdomGX˙Y=
35 34 imp φ¬XYdomGX˙Y=
36 ndmfv ¬XYdomGGXY=
37 36 adantl φ¬XYdomGGXY=
38 35 37 eqtr4d φ¬XYdomGX˙Y=GXY
39 28 38 pm2.61dan φX˙Y=GXY