Description: Express the predicate F converges to A . Similar to clim2 , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | clim2cf.nf | |
|
clim2cf.z | |
||
clim2cf.m | |
||
clim2cf.f | |
||
clim2cf.fv | |
||
clim2cf.a | |
||
clim2cf.b | |
||
Assertion | clim2cf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clim2cf.nf | |
|
2 | clim2cf.z | |
|
3 | clim2cf.m | |
|
4 | clim2cf.f | |
|
5 | clim2cf.fv | |
|
6 | clim2cf.a | |
|
7 | clim2cf.b | |
|
8 | 6 | biantrurd | |
9 | 2 | uztrn2 | |
10 | 7 | biantrurd | |
11 | 9 10 | sylan2 | |
12 | 11 | anassrs | |
13 | 12 | ralbidva | |
14 | 13 | rexbidva | |
15 | 14 | ralbidv | |
16 | 1 2 3 4 5 | clim2f | |
17 | 8 15 16 | 3bitr4rd | |