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 ⊢ 𝑈 = ( lub ‘ 𝐾 )
joinfval.j ⊢ ∨ = ( join ‘ 𝐾 )
Assertion joinfval2 ( 𝐾 ∈ 𝑉 → ∨ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } )

Proof

Step Hyp Ref Expression
1 joinfval.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
2 joinfval.j ⊢ ∨ = ( join ‘ 𝐾 )
3 1 2 joinfval ⊢ ( 𝐾 ∈ 𝑉 → ∨ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } )
4 1 lubfun ⊢ Fun 𝑈
5 funbrfv2b ⊢ ( Fun 𝑈 → ( { 𝑥 , 𝑦 } 𝑈 𝑧 ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) ) )
6 4 5 ax-mp ⊢ ( { 𝑥 , 𝑦 } 𝑈 𝑧 ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) )
7 eqcom ⊢ ( ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ↔ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) )
8 7 anbi2i ⊢ ( ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) )
9 6 8 bitri ⊢ ( { 𝑥 , 𝑦 } 𝑈 𝑧 ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) )
10 9 oprabbii ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) }
11 3 10 eqtrdi ⊢ ( 𝐾 ∈ 𝑉 → ∨ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } )