Metamath Proof Explorer


Theorem enrefnn

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 AωAA

Proof

Step Hyp Ref Expression
1 id x=x=
2 1 1 breq12d x=xx
3 id x=yx=y
4 3 3 breq12d x=yxxyy
5 id x=sucyx=sucy
6 5 5 breq12d x=sucyxxsucysucy
7 id x=Ax=A
8 7 7 breq12d x=AxxAA
9 eqid =
10 en0 =
11 9 10 mpbir
12 en2sn yVyVyy
13 12 el2v yy
14 13 jctr yyyyyy
15 nnord yωOrdy
16 orddisj Ordyyy=
17 15 16 syl yωyy=
18 17 17 jca yωyy=yy=
19 unen yyyyyy=yy=yyyy
20 14 18 19 syl2anr yωyyyyyy
21 df-suc sucy=yy
22 20 21 21 3brtr4g yωyysucysucy
23 22 ex yωyysucysucy
24 2 4 6 8 11 23 finds AωAA