Metamath Proof Explorer

Theorem cdleme26f2

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)

Ref Expression
Hypotheses cdleme26.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdleme26.l
cdleme26.j
cdleme26.m
cdleme26.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdleme26.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdleme26f2.u
cdleme26f2.f
cdleme26f2.n
cdleme26f2.e
Assertion cdleme26f2

Proof

Step Hyp Ref Expression
1 cdleme26.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdleme26.l
3 cdleme26.j
4 cdleme26.m
5 cdleme26.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdleme26.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdleme26f2.u
8 cdleme26f2.f
9 cdleme26f2.n
10 cdleme26f2.e
11 simp11
12 simp23
13 simp31
14 simp12r
15 simp12l
16 13 14 15 3jca
17 simp21
18 simp22
19 simp13
20 simp32
21 simp33
22 2 3 4 5 6 7 8 9 cdleme22f2
23 11 12 16 17 18 19 20 21 22 syl323anc
24 simp23l
25 simp23r
26 1 2 3 4 5 6 7 8 9 10 cdleme25cl
27 11 17 18 24 25 15 14 26 syl322anc
28 simp13l
29 simp13r
30 1 fvexi ${⊢}{B}\in \mathrm{V}$
31 30 10 riotasv
32 27 28 29 13 31 syl112anc
33 32 oveq1d
34 23 33 breqtrrd