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

Metamath Proof Explorer

Theorem meetdef

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

Ref Expression
Hypotheses meetdef.u ⊢ 𝐺 = ( glb ‘ 𝐾 )
meetdef.m ⊢ ∧ = ( meet ‘ 𝐾 )
meetdef.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
meetdef.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
meetdef.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑍 )
Assertion meetdef ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ↔ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) )

Proof

Step Hyp Ref Expression
1 meetdef.u ⊢ 𝐺 = ( glb ‘ 𝐾 )
2 meetdef.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 meetdef.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
4 meetdef.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
5 meetdef.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑍 )
6 1 2 meetdm ⊢ ( 𝐾 ∈ 𝑉 → 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 𝐺 ) )