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

Theorem glbval 16321
 Description: Value of the greatest lower bound function of a poset. Out-of-domain arguments (those not satisfying ) are allowed for convenience, evaluating to the empty set on both sides of the equality. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
Hypotheses
Ref Expression
glbval.b
glbval.l
glbval.g
glbval.p
glbva.k
glbval.ss
Assertion
Ref Expression
glbval
Distinct variable groups:   ,,   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)   ()   (,,)   (,,)   (,,)

Proof of Theorem glbval
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 glbval.b . . . . 5
2 glbval.l . . . . 5
3 glbval.g . . . . 5
4 biid 244 . . . . 5
5 glbva.k . . . . . 6
65adantr 472 . . . . 5
71, 2, 3, 4, 6glbfval 16315 . . . 4
87fveq1d 5881 . . 3
9 glbval.p . . . . . 6
10 simpr 468 . . . . . 6
111, 2, 3, 9, 6, 10glbeu 16320 . . . . 5
12 raleq 2973 . . . . . . . . . 10
13 raleq 2973 . . . . . . . . . . . 12
1413imbi1d 324 . . . . . . . . . . 11
1514ralbidv 2829 . . . . . . . . . 10
1612, 15anbi12d 725 . . . . . . . . 9
1716, 9syl6bbr 271 . . . . . . . 8
1817reubidv 2961 . . . . . . 7
1918elabg 3174 . . . . . 6
2019adantl 473 . . . . 5
2111, 20mpbird 240 . . . 4
22 fvres 5893 . . . 4
2321, 22syl 17 . . 3
24 glbval.ss . . . . . 6
2524adantr 472 . . . . 5
26 fvex 5889 . . . . . . 7
271, 26eqeltri 2545 . . . . . 6
2827elpw2 4565 . . . . 5
2925, 28sylibr 217 . . . 4
3017riotabidv 6272 . . . . 5
31 eqid 2471 . . . . 5
32 riotaex 6274 . . . . 5
3330, 31, 32fvmpt 5963 . . . 4
3429, 33syl 17 . . 3
358, 23, 343eqtrd 2509 . 2
36 ndmfv 5903 . . . 4