Description: A function is finitely supported from B to A iff the extended function is finitely supported from D to A . (Contributed by Mario Carneiro, 25-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cantnfs.s | |
|
cantnfs.a | |
||
cantnfs.b | |
||
cantnfrescl.d | |
||
cantnfrescl.b | |
||
cantnfrescl.x | |
||
cantnfrescl.a | |
||
cantnfrescl.t | |
||
Assertion | cantnfrescl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cantnfs.s | |
|
2 | cantnfs.a | |
|
3 | cantnfs.b | |
|
4 | cantnfrescl.d | |
|
5 | cantnfrescl.b | |
|
6 | cantnfrescl.x | |
|
7 | cantnfrescl.a | |
|
8 | cantnfrescl.t | |
|
9 | 7 | adantr | |
10 | 6 9 | eqeltrd | |
11 | 10 | ralrimiva | |
12 | 5 11 | raldifeq | |
13 | eqid | |
|
14 | 13 | fmpt | |
15 | eqid | |
|
16 | 15 | fmpt | |
17 | 12 14 16 | 3bitr3g | |
18 | 3 | mptexd | |
19 | funmpt | |
|
20 | 19 | a1i | |
21 | 4 | mptexd | |
22 | funmpt | |
|
23 | 21 22 | jctir | |
24 | 18 20 23 | jca31 | |
25 | 4 5 6 | extmptsuppeq | |
26 | suppeqfsuppbi | |
|
27 | 24 25 26 | sylc | |
28 | 17 27 | anbi12d | |
29 | 1 2 3 | cantnfs | |
30 | 8 2 4 | cantnfs | |
31 | 28 29 30 | 3bitr4d | |