Theorem joincl

Description: Closure of join of elements in the domain. (Contributed by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	joincl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	joincl.j	⊢ ∨ = ( join ‘ 𝐾 )
	joincl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	joincl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	joincl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	joincl.e	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ )
Assertion	joincl	⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		joincl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		joincl.j	⊢ ∨ = ( join ‘ 𝐾 )
3		joincl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
4		joincl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		joincl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		joincl.e	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ )
7		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
8	7 2 3 4 5	joinval	⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( ( lub ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
9	7 2 3 4 5	joindef	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ ↔ { 𝑋 , 𝑌 } ∈ dom ( lub ‘ 𝐾 ) ) )
10	6 9	mpbid	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ∈ dom ( lub ‘ 𝐾 ) )
11	1 7 3 10	lubcl	⊢ ( 𝜑 → ( ( lub ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ∈ 𝐵 )
12	8 11	eqeltrd	⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )