Metamath Proof Explorer


Theorem cdleme26f2ALTN

Description: Part of proof of Lemma E in Crawley p. 113. cdleme26fALTN with s and t swapped (this case is not mentioned by them). If s <_ t \/ v, then f(s) <_ f_s(t) \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme26.b B = Base K
cdleme26.l ˙ = K
cdleme26.j ˙ = join K
cdleme26.m ˙ = meet K
cdleme26.a A = Atoms K
cdleme26.h H = LHyp K
cdleme26f2.u U = P ˙ Q ˙ W
cdleme26f2.f G = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme26f2.n O = P ˙ Q ˙ G ˙ T ˙ s ˙ W
cdleme26f2.e E = ι u B | s A ¬ s ˙ W ¬ s ˙ P ˙ Q u = O
Assertion cdleme26f2ALTN K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W G ˙ E ˙ V

Proof

Step Hyp Ref Expression
1 cdleme26.b B = Base K
2 cdleme26.l ˙ = K
3 cdleme26.j ˙ = join K
4 cdleme26.m ˙ = meet K
5 cdleme26.a A = Atoms K
6 cdleme26.h H = LHyp K
7 cdleme26f2.u U = P ˙ Q ˙ W
8 cdleme26f2.f G = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme26f2.n O = P ˙ Q ˙ G ˙ T ˙ s ˙ W
10 cdleme26f2.e E = ι u B | s A ¬ s ˙ W ¬ s ˙ P ˙ Q u = O
11 simp11 K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W K HL W H
12 simp23 K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W T A ¬ T ˙ W
13 simp31r K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W ¬ s ˙ P ˙ Q
14 simp12r K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W T ˙ P ˙ Q
15 simp12l K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W P Q
16 13 14 15 3jca K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W ¬ s ˙ P ˙ Q T ˙ P ˙ Q P Q
17 simp21 K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W P A ¬ P ˙ W
18 simp22 K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W Q A ¬ Q ˙ W
19 simp13 K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W s A ¬ s ˙ W
20 simp32 K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W s T s ˙ T ˙ V
21 simp33 K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W V A V ˙ W
22 2 3 4 5 6 7 8 9 cdleme22f2 K HL W H T A ¬ T ˙ W ¬ s ˙ P ˙ Q T ˙ P ˙ Q P Q P A ¬ P ˙ W Q A ¬ Q ˙ W s A ¬ s ˙ W s T s ˙ T ˙ V V A V ˙ W G ˙ O ˙ V
23 11 12 16 17 18 19 20 21 22 syl323anc K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W G ˙ O ˙ V
24 simp23l K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W T A
25 simp23r K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W ¬ T ˙ W
26 1 2 3 4 5 6 7 8 9 10 cdleme25cl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W P Q T ˙ P ˙ Q E B
27 11 17 18 24 25 15 14 26 syl322anc K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W E B
28 simp13l K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W s A
29 simp31 K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q
30 1 fvexi B V
31 30 10 riotasv E B s A ¬ s ˙ W ¬ s ˙ P ˙ Q E = O
32 27 28 29 31 syl3anc K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W E = O
33 32 oveq1d K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W E ˙ V = O ˙ V
34 23 33 breqtrrd K HL W H P Q T ˙ P ˙ Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W ¬ s ˙ W ¬ s ˙ P ˙ Q s T s ˙ T ˙ V V A V ˙ W G ˙ E ˙ V