Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  meetval Structured version   Unicode version

Theorem meetval 15776
 Description: Meet value. Since both sides evaluate to when they don't exist, for convenience we drop the requirement. (Contributed by NM, 9-Sep-2018.)
Hypotheses
Ref Expression
meetdef.u
meetdef.m
meetdef.k
meetdef.x
meetdef.y
Assertion
Ref Expression
meetval

Proof of Theorem meetval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 meetdef.k . . . . . 6
2 meetdef.u . . . . . . 7
3 meetdef.m . . . . . . 7
42, 3meetfval2 15773 . . . . . 6
51, 4syl 16 . . . . 5
65oveqd 6313 . . . 4
8 simpr 461 . . . 4
9 eqidd 2458 . . . 4
10 meetdef.x . . . . . 6
11 meetdef.y . . . . . 6
12 fvex 5882 . . . . . . 7
1312a1i 11 . . . . . 6
14 preq12 4113 . . . . . . . . . 10
1514eleq1d 2526 . . . . . . . . 9
16153adant3 1016 . . . . . . . 8
17 simp3 998 . . . . . . . . 9
1814fveq2d 5876 . . . . . . . . . 10
19183adant3 1016 . . . . . . . . 9
2017, 19eqeq12d 2479 . . . . . . . 8
2116, 20anbi12d 710 . . . . . . 7
22 moeq 3275 . . . . . . . 8
2322moani 2346 . . . . . . 7
24 eqid 2457 . . . . . . 7
2521, 23, 24ovigg 6422 . . . . . 6
2610, 11, 13, 25syl3anc 1228 . . . . 5
2726adantr 465 . . . 4
288, 9, 27mp2and 679 . . 3
297, 28eqtrd 2498 . 2
302, 3, 1, 10, 11meetdef 15775 . . . . . 6
3130notbid 294 . . . . 5
32 df-ov 6299 . . . . . 6
33 ndmfv 5896 . . . . . 6
3432, 33syl5eq 2510 . . . . 5
3531, 34syl6bir 229 . . . 4
3635imp 429 . . 3
37 ndmfv 5896 . . . 4