Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  fin0 Unicode version

Theorem fin0 6419
 Description: A nonempty finite set has at least one element. (Contributed by Jim Kingdon, 10-Sep-2021.)
Assertion
Ref Expression
fin0
Distinct variable group:   ,

Proof of Theorem fin0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 6308 . . 3
21biimpi 118 . 2
3 simplrr 503 . . . . . . 7
4 simpr 108 . . . . . . 7
53, 4breqtrd 3817 . . . . . 6
6 en0 6342 . . . . . 6
75, 6sylib 120 . . . . 5
8 nner 2250 . . . . 5
97, 8syl 14 . . . 4
10 n0r 3268 . . . . . 6
1110necon2bi 2301 . . . . 5
127, 11syl 14 . . . 4
139, 122falsed 651 . . 3
14 simplrr 503 . . . . . . . . . 10
1514adantr 270 . . . . . . . . 9
1615ensymd 6330 . . . . . . . 8
17 bren 6294 . . . . . . . 8
1816, 17sylib 120 . . . . . . 7
19 f1of 5157 . . . . . . . . . . . 12
2019adantl 271 . . . . . . . . . . 11
21 sucidg 4179 . . . . . . . . . . . . 13
2221ad3antlr 477 . . . . . . . . . . . 12
23 simplr 497 . . . . . . . . . . . 12
2422, 23eleqtrrd 2159 . . . . . . . . . . 11
2520, 24ffvelrnd 5335 . . . . . . . . . 10
26 elex2 2616 . . . . . . . . . 10
2725, 26syl 14 . . . . . . . . 9
2827, 10syl 14 . . . . . . . 8
2928, 272thd 173 . . . . . . 7
3018, 29exlimddv 1820 . . . . . 6
3130ex 113 . . . . 5
3231rexlimdva 2478 . . . 4
3332imp 122 . . 3
34 nn0suc 4353 . . . 4