Description: Part of proof of Lemma E in Crawley p. 113. Value of F at an atom not under W . TODO: FIX COMMENT. TODO: consolidate uses of lhpmat here and elsewhere, and presence/absence of s .<_ ( P .\/ Q ) term. Also, why can proof be shortened with cdleme29cl ? What is difference from cdlemefs27cl ? (Contributed by NM, 29-Mar-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemefrs27.b | |
|
cdlemefrs27.l | |
||
cdlemefrs27.j | |
||
cdlemefrs27.m | |
||
cdlemefrs27.a | |
||
cdlemefrs27.h | |
||
cdlemefrs27.eq | |
||
cdlemefrs27.nb | |
||
cdlemefrs27.rnb | |
||
cdleme29frs.o | |
||
Assertion | cdlemefrs32fva | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemefrs27.b | |
|
2 | cdlemefrs27.l | |
|
3 | cdlemefrs27.j | |
|
4 | cdlemefrs27.m | |
|
5 | cdlemefrs27.a | |
|
6 | cdlemefrs27.h | |
|
7 | cdlemefrs27.eq | |
|
8 | cdlemefrs27.nb | |
|
9 | cdlemefrs27.rnb | |
|
10 | cdleme29frs.o | |
|
11 | simp2rl | |
|
12 | 1 5 | atbase | |
13 | eqid | |
|
14 | 10 13 | cdleme31so | |
15 | 11 12 14 | 3syl | |
16 | ssidd | |
|
17 | simpll | |
|
18 | simpr | |
|
19 | 17 18 | jca | |
20 | 19 | imim1i | |
21 | 20 | ralimi | |
22 | 21 | rgenw | |
23 | 22 | a1i | |
24 | 1 2 3 4 5 6 7 8 9 | cdlemefrs29bpre1 | |
25 | simpl11 | |
|
26 | simpl2r | |
|
27 | simpl3 | |
|
28 | simpr | |
|
29 | 1 2 3 4 5 6 7 | cdlemefrs29pre00 | |
30 | 25 26 27 28 29 | syl31anc | |
31 | 30 | imbi1d | |
32 | 31 | ralbidva | |
33 | 32 | rexbidv | |
34 | 24 33 | mpbid | |
35 | 1 2 3 4 5 6 7 8 9 | cdlemefrs29cpre1 | |
36 | riotass2 | |
|
37 | 16 23 34 35 36 | syl22anc | |
38 | 1 2 3 4 5 6 7 8 | cdlemefrs29bpre0 | |
39 | 38 | adantr | |
40 | 9 39 | riota5 | |
41 | 15 37 40 | 3eqtrd | |