Theorem joindef

Description: Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018)

	Ref	Expression
Hypotheses	joindef.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	joindef.j	⊢ ∨ = ( join ‘ 𝐾 )
	joindef.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	joindef.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
	joindef.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑍 )
Assertion	joindef	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ ↔ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		joindef.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
2		joindef.j	⊢ ∨ = ( join ‘ 𝐾 )
3		joindef.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
4		joindef.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
5		joindef.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑍 )
6	1 2	joindm	⊢ ( 𝐾 ∈ 𝑉 → dom ∨ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 } )
7	6	eleq2d	⊢ ( 𝐾 ∈ 𝑉 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 } ) )
8	3 7	syl	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 } ) )
9		preq1	⊢ ( 𝑥 = 𝑋 → { 𝑥 , 𝑦 } = { 𝑋 , 𝑦 } )
10	9	eleq1d	⊢ ( 𝑥 = 𝑋 → ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ↔ { 𝑋 , 𝑦 } ∈ dom 𝑈 ) )
11		preq2	⊢ ( 𝑦 = 𝑌 → { 𝑋 , 𝑦 } = { 𝑋 , 𝑌 } )
12	11	eleq1d	⊢ ( 𝑦 = 𝑌 → ( { 𝑋 , 𝑦 } ∈ dom 𝑈 ↔ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) )
13	10 12	opelopabg	⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑍 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 } ↔ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) )
14	4 5 13	syl2anc	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 } ↔ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) )
15	8 14	bitrd	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ ↔ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) )