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

Metamath Proof Explorer

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 𝑈 ) )