Theorem meetval2lem

Description: Lemma for meetval2 and meeteu . (Contributed by NM, 12-Sep-2018) TODO: combine this through meeteu into meetlem ?

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

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		breq2	|- ( y = X -> ( x .<_ y <-> x .<_ X ) )
8		breq2	|- ( y = Y -> ( x .<_ y <-> x .<_ Y ) )
9	7 8	ralprg	|- ( ( X e. B /\ Y e. B ) -> ( A. y e. { X , Y } x .<_ y <-> ( x .<_ X /\ x .<_ Y ) ) )
10		breq2	|- ( y = X -> ( z .<_ y <-> z .<_ X ) )
11		breq2	|- ( y = Y -> ( z .<_ y <-> z .<_ Y ) )
12	10 11	ralprg	|- ( ( X e. B /\ Y e. B ) -> ( A. y e. { X , Y } z .<_ y <-> ( z .<_ X /\ z .<_ Y ) ) )
13	12	imbi1d	|- ( ( X e. B /\ Y e. B ) -> ( ( A. y e. { X , Y } z .<_ y -> z .<_ x ) <-> ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) )
14	13	ralbidv	|- ( ( X e. B /\ Y e. B ) -> ( A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) <-> A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) )
15	9 14	anbi12d	|- ( ( 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 ) ) ) )