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 | |
|
meetdef.m | |
||
meetdef.k | |
||
meetdef.x | |
||
meetdef.y | |
||
Assertion | meetval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | meetdef.u | |
|
2 | meetdef.m | |
|
3 | meetdef.k | |
|
4 | meetdef.x | |
|
5 | meetdef.y | |
|
6 | 1 2 | meetfval2 | |
7 | 3 6 | syl | |
8 | 7 | oveqd | |
9 | 8 | adantr | |
10 | simpr | |
|
11 | eqidd | |
|
12 | fvexd | |
|
13 | preq12 | |
|
14 | 13 | eleq1d | |
15 | 14 | 3adant3 | |
16 | simp3 | |
|
17 | 13 | fveq2d | |
18 | 17 | 3adant3 | |
19 | 16 18 | eqeq12d | |
20 | 15 19 | anbi12d | |
21 | moeq | |
|
22 | 21 | moani | |
23 | eqid | |
|
24 | 20 22 23 | ovigg | |
25 | 4 5 12 24 | syl3anc | |
26 | 25 | adantr | |
27 | 10 11 26 | mp2and | |
28 | 9 27 | eqtrd | |
29 | 1 2 3 4 5 | meetdef | |
30 | 29 | notbid | |
31 | df-ov | |
|
32 | ndmfv | |
|
33 | 31 32 | eqtrid | |
34 | 30 33 | syl6bir | |
35 | 34 | imp | |
36 | ndmfv | |
|
37 | 36 | adantl | |
38 | 35 37 | eqtr4d | |
39 | 28 38 | pm2.61dan | |