Theorem meetdm

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

	Ref	Expression
Hypotheses	meetfval.u	|- G = ( glb ` K )
	meetfval.m	|- ./\ = ( meet ` K )
Assertion	meetdm	|- ( K e. V -> dom ./\ = { <. x , y >. | { x , y } e. dom G } )

Proof

Step	Hyp	Ref	Expression
1		meetfval.u	|- G = ( glb ` K )
2		meetfval.m	|- ./\ = ( meet ` K )
3	1 2	meetfval2	|- ( K e. V -> ./\ = { <. <. x , y >. , z >. | ( { x , y } e. dom G /\ z = ( G ` { x , y } ) ) } )
4	3	dmeqd	|- ( K e. V -> dom ./\ = dom { <. <. x , y >. , z >. | ( { x , y } e. dom G /\ z = ( G ` { x , y } ) ) } )
5		dmoprab	|- dom { <. <. x , y >. , z >. | ( { x , y } e. dom G /\ z = ( G ` { x , y } ) ) } = { <. x , y >. | E. z ( { x , y } e. dom G /\ z = ( G ` { x , y } ) ) }
6		fvex	|- ( G ` { x , y } ) e. _V
7	6	isseti	|- E. z z = ( G ` { x , y } )
8		19.42v	|- ( E. z ( { x , y } e. dom G /\ z = ( G ` { x , y } ) ) <-> ( { x , y } e. dom G /\ E. z z = ( G ` { x , y } ) ) )
9	7 8	mpbiran2	|- ( E. z ( { x , y } e. dom G /\ z = ( G ` { x , y } ) ) <-> { x , y } e. dom G )
10	9	opabbii	|- { <. x , y >. | E. z ( { x , y } e. dom G /\ z = ( G ` { x , y } ) ) } = { <. x , y >. | { x , y } e. dom G }
11	5 10	eqtri	|- dom { <. <. x , y >. , z >. | ( { x , y } e. dom G /\ z = ( G ` { x , y } ) ) } = { <. x , y >. | { x , y } e. dom G }
12	4 11	eqtrdi	|- ( K e. V -> dom ./\ = { <. x , y >. | { x , y } e. dom G } )