This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem joinfval2

Description: Value of join function for a poset-type structure. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

Ref Expression
Hypotheses joinfval.u ⊢ U = lub ⁡ K
joinfval.j ⊢ ∨ ˙ = join ⁡ K
Assertion joinfval2 ⊢ K ∈ V → ∨ ˙ = x y z | x y ∈ dom ⁡ U ∧ z = U ⁡ x y

Proof

Step Hyp Ref Expression
1 joinfval.u ⊢ U = lub ⁡ K
2 joinfval.j ⊢ ∨ ˙ = join ⁡ K
3 1 2 joinfval ⊢ K ∈ V → ∨ ˙ = x y z | x y U z
4 1 lubfun ⊢ Fun ⁡ U
5 funbrfv2b ⊢ Fun ⁡ U → x y U z ↔ x y ∈ dom ⁡ U ∧ U ⁡ x y = z
6 4 5 ax-mp ⊢ x y U z ↔ x y ∈ dom ⁡ U ∧ U ⁡ x y = z
7 eqcom ⊢ U ⁡ x y = z ↔ z = U ⁡ x y
8 7 anbi2i ⊢ x y ∈ dom ⁡ U ∧ U ⁡ x y = z ↔ x y ∈ dom ⁡ U ∧ z = U ⁡ x y
9 6 8 bitri ⊢ x y U z ↔ x y ∈ dom ⁡ U ∧ z = U ⁡ x y
10 9 oprabbii ⊢ x y z | x y U z = x y z | x y ∈ dom ⁡ U ∧ z = U ⁡ x y
11 3 10 eqtrdi ⊢ K ∈ V → ∨ ˙ = x y z | x y ∈ dom ⁡ U ∧ z = U ⁡ x y