Metamath Proof Explorer

Theorem ltrniotacnvN

Description: Version of cdleme51finvtrN with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	ltrniotaval.l	\|- .<_ = ( le ` K )
		ltrniotaval.a	\|- A = ( Atoms ` K )
		ltrniotaval.h	\|- H = ( LHyp ` K )
		ltrniotaval.t	\|- T = ( ( LTrn ` K ) ` W )
		ltrniotaval.f	\|- F = ( iota_ f e. T ( f ` P ) = Q )
	Assertion	ltrniotacnvN	\|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> `' F e. T )

Proof

Step	Hyp	Ref	Expression
1		ltrniotaval.l	\|- .<_ = ( le ` K )
2		ltrniotaval.a	\|- A = ( Atoms ` K )
3		ltrniotaval.h	\|- H = ( LHyp ` K )
4		ltrniotaval.t	\|- T = ( ( LTrn ` K ) ` W )
5		ltrniotaval.f	\|- F = ( iota_ f e. T ( f ` P ) = Q )
6		eqid	\|- ( Base ` K ) = ( Base ` K )
7		eqid	\|- ( join ` K ) = ( join ` K )
8		eqid	\|- ( meet ` K ) = ( meet ` K )
9		eqid	\|- ( ( P ( join ` K ) Q ) ( meet ` K ) W ) = ( ( P ( join ` K ) Q ) ( meet ` K ) W )
10		eqid	\|- ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) = ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) )
11		eqid	\|- ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) )
12		eqid	\|- ( x e. ( Base ` K ) \|-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) = ( x e. ( Base ` K ) \|-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) )
13	6 1 7 8 2 3 9 10 11 12 4 5	cdlemg1finvtrlemN	\|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> `' F e. T )