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 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } )