Metamath Proof Explorer

Theorem dicelvalN

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 25-Feb-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dicval.l ⊢≤˙=≤K
dicval.a ⊢A=Atoms⁡K
dicval.h ⊢H=LHyp⁡K
dicval.p ⊢P=oc⁡K⁡W
dicval.t ⊢T=LTrn⁡K⁡W
dicval.e ⊢E=TEndo⁡K⁡W
dicval.i ⊢I=DIsoC⁡K⁡W
Assertion dicelvalN ⊢K∈V∧W∈H∧Q∈A∧¬Q≤˙W→Y∈I⁡Q↔Y∈V×V∧1st⁡Y=2nd⁡Y⁡ιg∈T|g⁡P=Q∧2nd⁡Y∈E

Proof

Step Hyp Ref Expression
1 dicval.l ⊢≤˙=≤K
2 dicval.a ⊢A=Atoms⁡K
3 dicval.h ⊢H=LHyp⁡K
4 dicval.p ⊢P=oc⁡K⁡W
5 dicval.t ⊢T=LTrn⁡K⁡W
6 dicval.e ⊢E=TEndo⁡K⁡W
7 dicval.i ⊢I=DIsoC⁡K⁡W
8 1 2 3 4 5 6 7 dicval ⊢K∈V∧W∈H∧Q∈A∧¬Q≤˙W→I⁡Q=fs|f=s⁡ιg∈T|g⁡P=Q∧s∈E
9 8 eleq2d ⊢K∈V∧W∈H∧Q∈A∧¬Q≤˙W→Y∈I⁡Q↔Y∈fs|f=s⁡ιg∈T|g⁡P=Q∧s∈E
10 vex ⊢f∈V
11 vex ⊢s∈V
12 10 11 op1std ⊢Y=fs→1st⁡Y=f
13 10 11 op2ndd ⊢Y=fs→2nd⁡Y=s
14 13 fveq1d ⊢Y=fs→2nd⁡Y⁡ιg∈T|g⁡P=Q=s⁡ιg∈T|g⁡P=Q
15 12 14 eqeq12d ⊢Y=fs→1st⁡Y=2nd⁡Y⁡ιg∈T|g⁡P=Q↔f=s⁡ιg∈T|g⁡P=Q
16 13 eleq1d ⊢Y=fs→2nd⁡Y∈E↔s∈E
17 15 16 anbi12d ⊢Y=fs→1st⁡Y=2nd⁡Y⁡ιg∈T|g⁡P=Q∧2nd⁡Y∈E↔f=s⁡ιg∈T|g⁡P=Q∧s∈E
18 17 elopaba ⊢Y∈fs|f=s⁡ιg∈T|g⁡P=Q∧s∈E↔Y∈V×V∧1st⁡Y=2nd⁡Y⁡ιg∈T|g⁡P=Q∧2nd⁡Y∈E
19 9 18 bitrdi ⊢K∈V∧W∈H∧Q∈A∧¬Q≤˙W→Y∈I⁡Q↔Y∈V×V∧1st⁡Y=2nd⁡Y⁡ιg∈T|g⁡P=Q∧2nd⁡Y∈E