Description: First version of proof for fsetprcnex , which was much more complicated. (Contributed by AV, 14-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | fsetprcnexALT | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abanssl | |
|
2 | n0 | |
|
3 | vex | |
|
4 | 3 | a1i | |
5 | fsetsnprcnex | |
|
6 | 4 5 | sylan | |
7 | df-nel | |
|
8 | 6 7 | sylib | |
9 | eqid | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | 9 10 11 | cfsetsnfsetf1o | |
13 | 12 | ancoms | |
14 | 13 | adantr | |
15 | f1ovv | |
|
16 | 15 | bicomd | |
17 | 14 16 | syl | |
18 | 8 17 | mtbird | |
19 | 18 | exp31 | |
20 | 19 | exlimiv | |
21 | 2 20 | sylbi | |
22 | 21 | impcom | |
23 | 22 | imp | |
24 | df-nel | |
|
25 | 23 24 | sylibr | |
26 | prcssprc | |
|
27 | 1 25 26 | sylancr | |