Theorem meetval2

Description: Value of meet for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011) (Revised by NM, 11-Sep-2018)

	Ref	Expression
Hypotheses	meetval2.b	|- B = ( Base ` K )
	meetval2.l	|- .<_ = ( le ` K )
	meetval2.m	|- ./\ = ( meet ` K )
	meetval2.k	|- ( ph -> K e. V )
	meetval2.x	|- ( ph -> X e. B )
	meetval2.y	|- ( ph -> Y e. B )
Assertion	meetval2	|- ( ph -> ( X ./\ Y ) = ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		meetval2.b	|- B = ( Base ` K )
2		meetval2.l	|- .<_ = ( le ` K )
3		meetval2.m	|- ./\ = ( meet ` K )
4		meetval2.k	|- ( ph -> K e. V )
5		meetval2.x	|- ( ph -> X e. B )
6		meetval2.y	|- ( ph -> Y e. B )
7		eqid	|- ( glb ` K ) = ( glb ` K )
8	7 3 4 5 6	meetval	|- ( ph -> ( X ./\ Y ) = ( ( glb ` K ) ` { X , Y } ) )
9		biid	|- ( ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) <-> ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) )
10	5 6	prssd	|- ( ph -> { X , Y } C_ B )
11	1 2 7 9 4 10	glbval	|- ( ph -> ( ( glb ` K ) ` { X , Y } ) = ( iota_ x e. B ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) ) )
12	1 2 3 4 5 6	meetval2lem	|- ( ( X e. B /\ Y e. B ) -> ( ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) <-> ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )
13	12	riotabidv	|- ( ( X e. B /\ Y e. B ) -> ( iota_ x e. B ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) ) = ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )
14	5 6 13	syl2anc	|- ( ph -> ( iota_ x e. B ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) ) = ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )
15	8 11 14	3eqtrd	|- ( ph -> ( X ./\ Y ) = ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )