Metamath Proof Explorer


Theorem dicelval1sta

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

Ref Expression
Hypotheses dicelval1sta.l ˙ = K
dicelval1sta.a A = Atoms K
dicelval1sta.h H = LHyp K
dicelval1sta.p P = oc K W
dicelval1sta.t T = LTrn K W
dicelval1sta.i I = DIsoC K W
Assertion dicelval1sta K V W H Q A ¬ Q ˙ W Y I Q 1 st Y = 2 nd Y ι g T | g P = Q

Proof

Step Hyp Ref Expression
1 dicelval1sta.l ˙ = K
2 dicelval1sta.a A = Atoms K
3 dicelval1sta.h H = LHyp K
4 dicelval1sta.p P = oc K W
5 dicelval1sta.t T = LTrn K W
6 dicelval1sta.i I = DIsoC K W
7 eqid TEndo K W = TEndo K W
8 1 2 3 4 5 7 6 dicval K V W H Q A ¬ Q ˙ W I Q = f s | f = s ι g T | g P = Q s TEndo K W
9 8 eleq2d K V W H Q A ¬ Q ˙ W Y I Q Y f s | f = s ι g T | g P = Q s TEndo K W
10 9 biimp3a K V W H Q A ¬ Q ˙ W Y I Q Y f s | f = s ι g T | g P = Q s TEndo K W
11 eqeq1 f = 1 st Y f = s ι g T | g P = Q 1 st Y = s ι g T | g P = Q
12 11 anbi1d f = 1 st Y f = s ι g T | g P = Q s TEndo K W 1 st Y = s ι g T | g P = Q s TEndo K W
13 fveq1 s = 2 nd Y s ι g T | g P = Q = 2 nd Y ι g T | g P = Q
14 13 eqeq2d s = 2 nd Y 1 st Y = s ι g T | g P = Q 1 st Y = 2 nd Y ι g T | g P = Q
15 eleq1 s = 2 nd Y s TEndo K W 2 nd Y TEndo K W
16 14 15 anbi12d s = 2 nd Y 1 st Y = s ι g T | g P = Q s TEndo K W 1 st Y = 2 nd Y ι g T | g P = Q 2 nd Y TEndo K W
17 12 16 elopabi Y f s | f = s ι g T | g P = Q s TEndo K W 1 st Y = 2 nd Y ι g T | g P = Q 2 nd Y TEndo K W
18 10 17 syl K V W H Q A ¬ Q ˙ W Y I Q 1 st Y = 2 nd Y ι g T | g P = Q 2 nd Y TEndo K W
19 18 simpld K V W H Q A ¬ Q ˙ W Y I Q 1 st Y = 2 nd Y ι g T | g P = Q