This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdleme29cl

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

		Ref	Expression
	Hypotheses	cdleme26.b	\|- B = ( Base ` K )
		cdleme26.l	\|- .<_ = ( le ` K )
		cdleme26.j	\|- .\/ = ( join ` K )
		cdleme26.m	\|- ./\ = ( meet ` K )
		cdleme26.a	\|- A = ( Atoms ` K )
		cdleme26.h	\|- H = ( LHyp ` K )
		cdleme27.u	\|- U = ( ( P .\/ Q ) ./\ W )
		cdleme27.f	\|- F = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
		cdleme27.z	\|- Z = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
		cdleme27.n	\|- N = ( ( P .\/ Q ) ./\ ( Z .\/ ( ( s .\/ z ) ./\ W ) ) )
		cdleme27.d	\|- D = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = N ) )
		cdleme27.c	\|- C = if ( s .<_ ( P .\/ Q ) , D , F )
		cdleme29cl.i	\|- I = ( iota_ v e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> v = ( C .\/ ( X ./\ W ) ) ) )
	Assertion	cdleme29cl	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q /\ ( X e. B /\ -. X .<_ W ) ) -> I e. B )

Proof

Step	Hyp	Ref	Expression
1		cdleme26.b	\|- B = ( Base ` K )
2		cdleme26.l	\|- .<_ = ( le ` K )
3		cdleme26.j	\|- .\/ = ( join ` K )
4		cdleme26.m	\|- ./\ = ( meet ` K )
5		cdleme26.a	\|- A = ( Atoms ` K )
6		cdleme26.h	\|- H = ( LHyp ` K )
7		cdleme27.u	\|- U = ( ( P .\/ Q ) ./\ W )
8		cdleme27.f	\|- F = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
9		cdleme27.z	\|- Z = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
10		cdleme27.n	\|- N = ( ( P .\/ Q ) ./\ ( Z .\/ ( ( s .\/ z ) ./\ W ) ) )
11		cdleme27.d	\|- D = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = N ) )
12		cdleme27.c	\|- C = if ( s .<_ ( P .\/ Q ) , D , F )
13		cdleme29cl.i	\|- I = ( iota_ v e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> v = ( C .\/ ( X ./\ W ) ) ) )
14	1 2 3 4 5 6 7 8 9 10 11 12	cdleme29c	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q /\ ( X e. B /\ -. X .<_ W ) ) -> E! v e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> v = ( C .\/ ( X ./\ W ) ) ) )
15		riotacl	\|- ( E! v e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> v = ( C .\/ ( X ./\ W ) ) ) -> ( iota_ v e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> v = ( C .\/ ( X ./\ W ) ) ) ) e. B )
16	14 15	syl	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q /\ ( X e. B /\ -. X .<_ W ) ) -> ( iota_ v e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( X ./\ W ) ) = X ) -> v = ( C .\/ ( X ./\ W ) ) ) ) e. B )
17	13 16	eqeltrid	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q /\ ( X e. B /\ -. X .<_ W ) ) -> I e. B )