Metamath Proof Explorer

Theorem dicopelval

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

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
dicelval.f ⊢F∈V
dicelval.s ⊢S∈V
Assertion dicopelval ⊢K∈V∧W∈H∧Q∈A∧¬Q≤˙W→FS∈I⁡Q↔F=S⁡ιg∈T|g⁡P=Q∧S∈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 dicelval.f ⊢F∈V
9 dicelval.s ⊢S∈V
10 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
11 10 eleq2d ⊢K∈V∧W∈H∧Q∈A∧¬Q≤˙W→FS∈I⁡Q↔FS∈fs|f=s⁡ιg∈T|g⁡P=Q∧s∈E
12 eqeq1 ⊢f=F→f=s⁡ιg∈T|g⁡P=Q↔F=s⁡ιg∈T|g⁡P=Q
13 12 anbi1d ⊢f=F→f=s⁡ιg∈T|g⁡P=Q∧s∈E↔F=s⁡ιg∈T|g⁡P=Q∧s∈E
14 fveq1 ⊢s=S→s⁡ιg∈T|g⁡P=Q=S⁡ιg∈T|g⁡P=Q
15 14 eqeq2d ⊢s=S→F=s⁡ιg∈T|g⁡P=Q↔F=S⁡ιg∈T|g⁡P=Q
16 eleq1 ⊢s=S→s∈E↔S∈E
17 15 16 anbi12d ⊢s=S→F=s⁡ιg∈T|g⁡P=Q∧s∈E↔F=S⁡ιg∈T|g⁡P=Q∧S∈E
18 8 9 13 17 opelopab ⊢FS∈fs|f=s⁡ιg∈T|g⁡P=Q∧s∈E↔F=S⁡ιg∈T|g⁡P=Q∧S∈E
19 11 18 bitrdi ⊢K∈V∧W∈H∧Q∈A∧¬Q≤˙W→FS∈I⁡Q↔F=S⁡ιg∈T|g⁡P=Q∧S∈E