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

Theorem joinval 15762
 Description: Join 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
joindef.u
joindef.j
joindef.k
joindef.x
joindef.y
Assertion
Ref Expression
joinval

Proof of Theorem joinval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 joindef.k . . . . . 6
2 joindef.u . . . . . . 7
3 joindef.j . . . . . . 7
42, 3joinfval2 15759 . . . . . 6
51, 4syl 16 . . . . 5
65oveqd 6313 . . . 4
8 simpr 461 . . . 4
9 eqidd 2458 . . . 4
10 joindef.x . . . . . 6
11 joindef.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, 11joindef 15761 . . . . . 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