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