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