Theorem r1omhf

Description: A set is hereditarily finite iff it is finite and all of its elements are hereditarily finite. (Contributed by BTernaryTau, 19-Jan-2026)

	Ref	Expression
Assertion	r1omhf	|- ( A e. U. ( R1 " _om ) <-> ( A e. Fin /\ A. x e. A x e. U. ( R1 " _om ) ) )

Proof

Step	Hyp	Ref	Expression
1		r1omfi	|- U. ( R1 " _om ) C_ Fin
2	1	sseli	|- ( A e. U. ( R1 " _om ) -> A e. Fin )
3		r1funlim	|- ( Fun R1 /\ Lim dom R1 )
4	3	simpli	|- Fun R1
5		eluniima	|- ( Fun R1 -> ( A e. U. ( R1 " _om ) <-> E. y e. _om A e. ( R1 ` y ) ) )
6	4 5	ax-mp	|- ( A e. U. ( R1 " _om ) <-> E. y e. _om A e. ( R1 ` y ) )
7		r19.41v	|- ( E. y e. _om ( A e. ( R1 ` y ) /\ x e. A ) <-> ( E. y e. _om A e. ( R1 ` y ) /\ x e. A ) )
8		r1elcl	|- ( ( A e. ( R1 ` y ) /\ x e. A ) -> x e. ( R1 ` y ) )
9	8	reximi	|- ( E. y e. _om ( A e. ( R1 ` y ) /\ x e. A ) -> E. y e. _om x e. ( R1 ` y ) )
10	7 9	sylbir	|- ( ( E. y e. _om A e. ( R1 ` y ) /\ x e. A ) -> E. y e. _om x e. ( R1 ` y ) )
11	6 10	sylanb	|- ( ( A e. U. ( R1 " _om ) /\ x e. A ) -> E. y e. _om x e. ( R1 ` y ) )
12		eluniima	|- ( Fun R1 -> ( x e. U. ( R1 " _om ) <-> E. y e. _om x e. ( R1 ` y ) ) )
13	4 12	ax-mp	|- ( x e. U. ( R1 " _om ) <-> E. y e. _om x e. ( R1 ` y ) )
14	11 13	sylibr	|- ( ( A e. U. ( R1 " _om ) /\ x e. A ) -> x e. U. ( R1 " _om ) )
15	14	ralrimiva	|- ( A e. U. ( R1 " _om ) -> A. x e. A x e. U. ( R1 " _om ) )
16	2 15	jca	|- ( A e. U. ( R1 " _om ) -> ( A e. Fin /\ A. x e. A x e. U. ( R1 " _om ) ) )
17		limom	|- Lim _om
18		r1filimi	|- ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " _om ) /\ Lim _om ) -> A e. U. ( R1 " _om ) )
19	17 18	mp3an3	|- ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " _om ) ) -> A e. U. ( R1 " _om ) )
20	16 19	impbii	|- ( A e. U. ( R1 " _om ) <-> ( A e. Fin /\ A. x e. A x e. U. ( R1 " _om ) ) )