cdleme25cl

Description: Show closure of the unique element in cdleme25c . (Contributed by NM, 2-Feb-2013)

	Ref	Expression
Hypotheses	cdleme24.b	\|- B = ( Base ` K )
	cdleme24.l	\|- .<_ = ( le ` K )
	cdleme24.j	\|- .\/ = ( join ` K )
	cdleme24.m	\|- ./\ = ( meet ` K )
	cdleme24.a	\|- A = ( Atoms ` K )
	cdleme24.h	\|- H = ( LHyp ` K )
	cdleme24.u	\|- U = ( ( P .\/ Q ) ./\ W )
	cdleme24.f	\|- F = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
	cdleme24.n	\|- N = ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ s ) ./\ W ) ) )
	cdleme25cl.i	\|- I = ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) )
Assertion	cdleme25cl	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) ) ) -> I e. B )

Step	Hyp	Ref	Expression
1		cdleme24.b	\|- B = ( Base ` K )
2		cdleme24.l	\|- .<_ = ( le ` K )
3		cdleme24.j	\|- .\/ = ( join ` K )
4		cdleme24.m	\|- ./\ = ( meet ` K )
5		cdleme24.a	\|- A = ( Atoms ` K )
6		cdleme24.h	\|- H = ( LHyp ` K )
7		cdleme24.u	\|- U = ( ( P .\/ Q ) ./\ W )
8		cdleme24.f	\|- F = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
9		cdleme24.n	\|- N = ( ( P .\/ Q ) ./\ ( F .\/ ( ( R .\/ s ) ./\ W ) ) )
10		cdleme25cl.i	\|- I = ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) )
11	1 2 3 4 5 6 7 8 9	cdleme25c	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) ) ) -> E! u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) )
12		riotacl	\|- ( E! u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) -> ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) ) e. B )
13	11 12	syl	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) ) ) -> ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = N ) ) e. B )
14	10 13	eqeltrid	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) ) ) -> I e. B )

Metamath Proof Explorer