Metamath Proof Explorer


Theorem cdleme50f1o

Description: Part of proof of Lemma D in Crawley p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013)

Ref Expression
Hypotheses cdlemef50.b B=BaseK
cdlemef50.l ˙=K
cdlemef50.j ˙=joinK
cdlemef50.m ˙=meetK
cdlemef50.a A=AtomsK
cdlemef50.h H=LHypK
cdlemef50.u U=P˙Q˙W
cdlemef50.d D=t˙U˙Q˙P˙t˙W
cdlemefs50.e E=P˙Q˙D˙s˙t˙W
cdlemef50.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
Assertion cdleme50f1o KHLWHPA¬P˙WQA¬Q˙WF:B1-1 ontoB

Proof

Step Hyp Ref Expression
1 cdlemef50.b B=BaseK
2 cdlemef50.l ˙=K
3 cdlemef50.j ˙=joinK
4 cdlemef50.m ˙=meetK
5 cdlemef50.a A=AtomsK
6 cdlemef50.h H=LHypK
7 cdlemef50.u U=P˙Q˙W
8 cdlemef50.d D=t˙U˙Q˙P˙t˙W
9 cdlemefs50.e E=P˙Q˙D˙s˙t˙W
10 cdlemef50.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
11 1 2 3 4 5 6 7 8 9 10 cdleme50f1 KHLWHPA¬P˙WQA¬Q˙WF:B1-1B
12 1 2 3 4 5 6 7 8 9 10 cdleme50rn KHLWHPA¬P˙WQA¬Q˙WranF=B
13 dff1o5 F:B1-1 ontoBF:B1-1BranF=B
14 11 12 13 sylanbrc KHLWHPA¬P˙WQA¬Q˙WF:B1-1 ontoB