Description: Equinumerosity is reflexive for finite ordinals, proved without using the Axiom of Power Sets (unlike enrefg ). (Contributed by BTernaryTau, 31-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | enrefnn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |
|
2 | 1 1 | breq12d | |
3 | id | |
|
4 | 3 3 | breq12d | |
5 | id | |
|
6 | 5 5 | breq12d | |
7 | id | |
|
8 | 7 7 | breq12d | |
9 | eqid | |
|
10 | en0 | |
|
11 | 9 10 | mpbir | |
12 | en2sn | |
|
13 | 12 | el2v | |
14 | 13 | jctr | |
15 | nnord | |
|
16 | orddisj | |
|
17 | 15 16 | syl | |
18 | 17 17 | jca | |
19 | unen | |
|
20 | 14 18 19 | syl2anr | |
21 | df-suc | |
|
22 | 20 21 21 | 3brtr4g | |
23 | 22 | ex | |
24 | 2 4 6 8 11 23 | finds | |