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 ˙=K
ltrniotaval.a A=AtomsK
ltrniotaval.h H=LHypK
ltrniotaval.t T=LTrnKW
ltrniotaval.f F=ιfT|fP=Q
Assertion ltrniotacnvN KHLWHPA¬P˙WQA¬Q˙WF-1T

Proof

Step Hyp Ref Expression
1 ltrniotaval.l ˙=K
2 ltrniotaval.a A=AtomsK
3 ltrniotaval.h H=LHypK
4 ltrniotaval.t T=LTrnKW
5 ltrniotaval.f F=ιfT|fP=Q
6 eqid BaseK=BaseK
7 eqid joinK=joinK
8 eqid meetK=meetK
9 eqid PjoinKQmeetKW=PjoinKQmeetKW
10 eqid tjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKW=tjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKW
11 eqid PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKW=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKW
12 eqid xBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWx=xBaseKifPQ¬x˙WιzBaseK|sA¬s˙WsjoinKxmeetKW=xz=ifs˙PjoinKQιyBaseK|tA¬t˙W¬t˙PjoinKQy=PjoinKQmeetKtjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKsjoinKtmeetKWs/ttjoinKPjoinKQmeetKWmeetKQjoinKPjoinKtmeetKWjoinKxmeetKWx
13 6 1 7 8 2 3 9 10 11 12 4 5 cdlemg1finvtrlemN KHLWHPA¬P˙WQA¬Q˙WF-1T