Metamath Proof Explorer


Theorem joinfval

Description: Value of join function for a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018) TODO: prove joinfval2 first to reduce net proof size (existence part)?

Ref Expression
Hypotheses joinfval.u U = lub K
joinfval.j ˙ = join K
Assertion joinfval K V ˙ = x y z | x y U z

Proof

Step Hyp Ref Expression
1 joinfval.u U = lub K
2 joinfval.j ˙ = join K
3 elex K V K V
4 fvex Base K V
5 moeq * z z = U x y
6 5 a1i x Base K y Base K * z z = U x y
7 eqid x y z | x Base K y Base K z = U x y = x y z | x Base K y Base K z = U x y
8 4 4 6 7 oprabex x y z | x Base K y Base K z = U x y V
9 8 a1i K V x y z | x Base K y Base K z = U x y V
10 1 lubfun Fun U
11 funbrfv2b Fun U x y U z x y dom U U x y = z
12 10 11 ax-mp x y U z x y dom U U x y = z
13 eqid Base K = Base K
14 eqid K = K
15 simpl K V x y dom U K V
16 simpr K V x y dom U x y dom U
17 13 14 1 15 16 lubelss K V x y dom U x y Base K
18 17 ex K V x y dom U x y Base K
19 vex x V
20 vex y V
21 19 20 prss x Base K y Base K x y Base K
22 18 21 syl6ibr K V x y dom U x Base K y Base K
23 eqcom U x y = z z = U x y
24 23 biimpi U x y = z z = U x y
25 22 24 anim12d1 K V x y dom U U x y = z x Base K y Base K z = U x y
26 12 25 syl5bi K V x y U z x Base K y Base K z = U x y
27 26 alrimiv K V z x y U z x Base K y Base K z = U x y
28 27 alrimiv K V y z x y U z x Base K y Base K z = U x y
29 28 alrimiv K V x y z x y U z x Base K y Base K z = U x y
30 ssoprab2 x y z x y U z x Base K y Base K z = U x y x y z | x y U z x y z | x Base K y Base K z = U x y
31 29 30 syl K V x y z | x y U z x y z | x Base K y Base K z = U x y
32 9 31 ssexd K V x y z | x y U z V
33 fveq2 p = K lub p = lub K
34 33 1 eqtr4di p = K lub p = U
35 34 breqd p = K x y lub p z x y U z
36 35 oprabbidv p = K x y z | x y lub p z = x y z | x y U z
37 df-join join = p V x y z | x y lub p z
38 36 37 fvmptg K V x y z | x y U z V join K = x y z | x y U z
39 32 38 mpdan K V join K = x y z | x y U z
40 2 39 syl5eq K V ˙ = x y z | x y U z
41 3 40 syl K V ˙ = x y z | x y U z