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

Metamath Proof Explorer

Theorem meetdm

Description: Domain of meet function for a poset-type structure. (Contributed by NM, 16-Sep-2018)

		Ref	Expression
	Hypotheses	meetfval.u	⊢ 𝐺 = ( glb ‘ 𝐾 )
		meetfval.m	⊢ ∧ = ( meet ‘ 𝐾 )
	Assertion	meetdm	⊢ ( 𝐾 ∈ 𝑉 → dom ∧ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝐺 } )

Proof

Step	Hyp	Ref	Expression
1		meetfval.u	⊢ 𝐺 = ( glb ‘ 𝐾 )
2		meetfval.m	⊢ ∧ = ( meet ‘ 𝐾 )
3	1 2	meetfval2	⊢ ( 𝐾 ∈ 𝑉 → ∧ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } )
4	3	dmeqd	⊢ ( 𝐾 ∈ 𝑉 → dom ∧ = dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } )
5		dmoprab	⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) }
6		fvex	⊢ ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ∈ V
7	6	isseti	⊢ ∃ 𝑧 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } )
8		19.42v	⊢ ( ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ ∃ 𝑧 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) )
9	7 8	mpbiran2	⊢ ( ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) ↔ { 𝑥 , 𝑦 } ∈ dom 𝐺 )
10	9	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝐺 }
11	5 10	eqtri	⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝐺 }
12	4 11	eqtrdi	⊢ ( 𝐾 ∈ 𝑉 → dom ∧ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝐺 } )