Theorem joinval2lem

Description: Lemma for joinval2 and joineu . (Contributed by NM, 12-Sep-2018) TODO: combine this through joineu into joinlem ?

	Ref	Expression
Hypotheses	joinval2.b	|- B = ( Base ` K )
	joinval2.l	|- .<_ = ( le ` K )
	joinval2.j	|- .\/ = ( join ` K )
	joinval2.k	|- ( ph -> K e. V )
	joinval2.x	|- ( ph -> X e. B )
	joinval2.y	|- ( ph -> Y e. B )
Assertion	joinval2lem	|- ( ( X e. B /\ Y e. B ) -> ( ( A. y e. { X , Y } y .<_ x /\ A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) ) <-> ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		joinval2.b	|- B = ( Base ` K )
2		joinval2.l	|- .<_ = ( le ` K )
3		joinval2.j	|- .\/ = ( join ` K )
4		joinval2.k	|- ( ph -> K e. V )
5		joinval2.x	|- ( ph -> X e. B )
6		joinval2.y	|- ( ph -> Y e. B )
7		breq1	|- ( y = X -> ( y .<_ x <-> X .<_ x ) )
8		breq1	|- ( y = Y -> ( y .<_ x <-> Y .<_ x ) )
9	7 8	ralprg	|- ( ( X e. B /\ Y e. B ) -> ( A. y e. { X , Y } y .<_ x <-> ( X .<_ x /\ Y .<_ x ) ) )
10		breq1	|- ( y = X -> ( y .<_ z <-> X .<_ z ) )
11		breq1	|- ( y = Y -> ( y .<_ z <-> Y .<_ z ) )
12	10 11	ralprg	|- ( ( X e. B /\ Y e. B ) -> ( A. y e. { X , Y } y .<_ z <-> ( X .<_ z /\ Y .<_ z ) ) )
13	12	imbi1d	|- ( ( X e. B /\ Y e. B ) -> ( ( A. y e. { X , Y } y .<_ z -> x .<_ z ) <-> ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) )
14	13	ralbidv	|- ( ( X e. B /\ Y e. B ) -> ( A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) <-> A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) )
15	9 14	anbi12d	|- ( ( X e. B /\ Y e. B ) -> ( ( A. y e. { X , Y } y .<_ x /\ A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) ) <-> ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) )