New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  csucex Unicode version

Theorem csucex 6259
 Description: The function mapping to its cardinal successor exists. (Contributed by Scott Fenton, 30-Jul-2019.)
Assertion
Ref Expression
csucex 1c

Proof of Theorem csucex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brcnv 4892 . . . . . . . . . 10
2 vex 2862 . . . . . . . . . . 11
32br1st 4858 . . . . . . . . . 10
41, 3bitri 240 . . . . . . . . 9
54anbi1i 676 . . . . . . . 8 AddC 1c AddC 1c
6 19.41v 1901 . . . . . . . 8 AddC 1c AddC 1c
75, 6bitr4i 243 . . . . . . 7 AddC 1c AddC 1c
87exbii 1582 . . . . . 6 AddC 1c AddC 1c
9 excom 1741 . . . . . . 7 AddC 1c AddC 1c
10 vex 2862 . . . . . . . . . 10
112, 10opex 4588 . . . . . . . . 9
12 breq1 4642 . . . . . . . . . 10 AddC 1c AddC 1c
13 brres 4949 . . . . . . . . . . 11 AddC 1c AddC 1c
142, 10braddcfn 5826 . . . . . . . . . . . 12 AddC
15 opelxp 4811 . . . . . . . . . . . . . 14 1c 1c
162, 15mpbiran 884 . . . . . . . . . . . . 13 1c 1c
17 elsn 3748 . . . . . . . . . . . . 13 1c 1c
1816, 17bitri 240 . . . . . . . . . . . 12 1c 1c
1914, 18anbi12ci 679 . . . . . . . . . . 11 AddC 1c 1c
2013, 19bitri 240 . . . . . . . . . 10 AddC 1c 1c
2112, 20syl6bb 252 . . . . . . . . 9 AddC 1c 1c
2211, 21ceqsexv 2894 . . . . . . . 8 AddC 1c 1c
2322exbii 1582 . . . . . . 7 AddC 1c 1c
249, 23bitri 240 . . . . . 6 AddC 1c 1c
258, 24bitri 240 . . . . 5 AddC 1c 1c
26 1cex 4142 . . . . . 6 1c
27 addceq2 4384 . . . . . . 7 1c 1c
2827eqeq1d 2361 . . . . . 6 1c 1c
2926, 28ceqsexv 2894 . . . . 5 1c 1c
3025, 29bitri 240 . . . 4 AddC 1c 1c
32 mptv 5718 . . . . . 6 1c 1c
3332eleq2i 2417 . . . . 5 1c 1c
34 vex 2862 . . . . . 6
35 addceq1 4383 . . . . . . 7 1c 1c
3635eqeq2d 2364 . . . . . 6 1c 1c
37 eqeq1 2359 . . . . . . 7 1c 1c
38 eqcom 2355 . . . . . . 7 1c 1c
3937, 38syl6bb 252 . . . . . 6 1c 1c
402, 34, 36, 39opelopab 4708 . . . . 5 1c 1c
4133, 40bitri 240 . . . 4 1c 1c
4230, 31, 413bitr4ri 269 . . 3 1c AddC 1c
4342eqrelriv 4850 . 2 1c AddC 1c