Metamath Proof Explorer

Theorem dicopelval2

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 20-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
dicval2.g ⊢G=ιg∈T|g⁡P=Q
dicelval2.f ⊢F∈V
dicelval2.s ⊢S∈V
Assertion dicopelval2 ⊢K∈V∧W∈H∧Q∈A∧¬Q≤˙W→FS∈I⁡Q↔F=S⁡G∧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 dicval2.g ⊢G=ιg∈T|g⁡P=Q
9 dicelval2.f ⊢F∈V
10 dicelval2.s ⊢S∈V
11 1 2 3 4 5 6 7 9 10 dicopelval ⊢K∈V∧W∈H∧Q∈A∧¬Q≤˙W→FS∈I⁡Q↔F=S⁡ιg∈T|g⁡P=Q∧S∈E
12 8 fveq2i ⊢S⁡G=S⁡ιg∈T|g⁡P=Q
13 12 eqeq2i ⊢F=S⁡G↔F=S⁡ιg∈T|g⁡P=Q
14 13 anbi1i ⊢F=S⁡G∧S∈E↔F=S⁡ιg∈T|g⁡P=Q∧S∈E
15 11 14 bitr4di ⊢K∈V∧W∈H∧Q∈A∧¬Q≤˙W→FS∈I⁡Q↔F=S⁡G∧S∈E