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 e. _om -> A ~~ A )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( x = (/) -> x = (/) )
2	1 1	breq12d	|- ( x = (/) -> ( x ~~ x <-> (/) ~~ (/) ) )
3		id	|- ( x = y -> x = y )
4	3 3	breq12d	|- ( x = y -> ( x ~~ x <-> y ~~ y ) )
5		id	|- ( x = suc y -> x = suc y )
6	5 5	breq12d	|- ( x = suc y -> ( x ~~ x <-> suc y ~~ suc y ) )
7		id	|- ( x = A -> x = A )
8	7 7	breq12d	|- ( x = A -> ( x ~~ x <-> A ~~ A ) )
9		eqid	|- (/) = (/)
10		en0	|- ( (/) ~~ (/) <-> (/) = (/) )
11	9 10	mpbir	|- (/) ~~ (/)
12		en2sn	|- ( ( y e. _V /\ y e. _V ) -> { y } ~~ { y } )
13	12	el2v	|- { y } ~~ { y }
14	13	jctr	|- ( y ~~ y -> ( y ~~ y /\ { y } ~~ { y } ) )
15		nnord	|- ( y e. _om -> Ord y )
16		orddisj	|- ( Ord y -> ( y i^i { y } ) = (/) )
17	15 16	syl	|- ( y e. _om -> ( y i^i { y } ) = (/) )
18	17 17	jca	|- ( y e. _om -> ( ( y i^i { y } ) = (/) /\ ( y i^i { y } ) = (/) ) )
19		unen	|- ( ( ( y ~~ y /\ { y } ~~ { y } ) /\ ( ( y i^i { y } ) = (/) /\ ( y i^i { y } ) = (/) ) ) -> ( y u. { y } ) ~~ ( y u. { y } ) )
20	14 18 19	syl2anr	|- ( ( y e. _om /\ y ~~ y ) -> ( y u. { y } ) ~~ ( y u. { y } ) )
21		df-suc	|- suc y = ( y u. { y } )
22	20 21 21	3brtr4g	|- ( ( y e. _om /\ y ~~ y ) -> suc y ~~ suc y )
23	22	ex	|- ( y e. _om -> ( y ~~ y -> suc y ~~ suc y ) )
24	2 4 6 8 11 23	finds	|- ( A e. _om -> A ~~ A )