Description: Lemma for isfin3-2 . K sets are subsets of the base. (Contributed by Stefan O'Rear, 6-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isf32lem.a | |
|
isf32lem.b | |
||
isf32lem.c | |
||
isf32lem.d | |
||
isf32lem.e | |
||
isf32lem.f | |
||
Assertion | isf32lem8 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isf32lem.a | |
|
2 | isf32lem.b | |
|
3 | isf32lem.c | |
|
4 | isf32lem.d | |
|
5 | isf32lem.e | |
|
6 | isf32lem.f | |
|
7 | 6 | fveq1i | |
8 | 4 | ssrab3 | |
9 | 1 2 3 4 | isf32lem5 | |
10 | 5 | fin23lem22 | |
11 | 8 9 10 | sylancr | |
12 | f1of | |
|
13 | 11 12 | syl | |
14 | fvco3 | |
|
15 | 13 14 | sylan | |
16 | 13 | ffvelrnda | |
17 | fveq2 | |
|
18 | suceq | |
|
19 | 18 | fveq2d | |
20 | 17 19 | difeq12d | |
21 | eqid | |
|
22 | fvex | |
|
23 | 22 | difexi | |
24 | 20 21 23 | fvmpt | |
25 | 16 24 | syl | |
26 | 15 25 | eqtrd | |
27 | 7 26 | eqtrid | |
28 | 1 | adantr | |
29 | 8 16 | sselid | |
30 | 28 29 | ffvelrnd | |
31 | 30 | elpwid | |
32 | 31 | ssdifssd | |
33 | 27 32 | eqsstrd | |