Theorem tskhf

Description: A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf .) (Contributed by NM, 22-Feb-2011) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026)

	Ref	Expression
Assertion	tskhf	|- ( ( T e. Tarski /\ T =/= (/) ) -> HF C_ T )

Proof

Step	Hyp	Ref	Expression
1		df-hf	|- HF = U. ( R1 " _om )
2	1	eleq2i	|- ( y e. HF <-> y e. U. ( R1 " _om ) )
3		eluni2	|- ( y e. U. ( R1 " _om ) <-> E. x e. ( R1 " _om ) y e. x )
4	2 3	bitri	|- ( y e. HF <-> E. x e. ( R1 " _om ) y e. x )
5		r1fun	|- Fun R1
6		fvelima	|- ( ( Fun R1 /\ x e. ( R1 " _om ) ) -> E. y e. _om ( R1 ` y ) = x )
7	5 6	mpan	|- ( x e. ( R1 " _om ) -> E. y e. _om ( R1 ` y ) = x )
8		r1tr	|- Tr ( R1 ` y )
9		treq	|- ( ( R1 ` y ) = x -> ( Tr ( R1 ` y ) <-> Tr x ) )
10	8 9	mpbii	|- ( ( R1 ` y ) = x -> Tr x )
11	10	rexlimivw	|- ( E. y e. _om ( R1 ` y ) = x -> Tr x )
12		trss	|- ( Tr x -> ( y e. x -> y C_ x ) )
13	7 11 12	3syl	|- ( x e. ( R1 " _om ) -> ( y e. x -> y C_ x ) )
14	13	adantl	|- ( ( ( T e. Tarski /\ T =/= (/) ) /\ x e. ( R1 " _om ) ) -> ( y e. x -> y C_ x ) )
15		tskr1om	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( R1 " _om ) C_ T )
16	15	sseld	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( x e. ( R1 " _om ) -> x e. T ) )
17		tskss	|- ( ( T e. Tarski /\ x e. T /\ y C_ x ) -> y e. T )
18	17	3exp	|- ( T e. Tarski -> ( x e. T -> ( y C_ x -> y e. T ) ) )
19	18	adantr	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( x e. T -> ( y C_ x -> y e. T ) ) )
20	16 19	syld	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( x e. ( R1 " _om ) -> ( y C_ x -> y e. T ) ) )
21	20	imp	|- ( ( ( T e. Tarski /\ T =/= (/) ) /\ x e. ( R1 " _om ) ) -> ( y C_ x -> y e. T ) )
22	14 21	syld	|- ( ( ( T e. Tarski /\ T =/= (/) ) /\ x e. ( R1 " _om ) ) -> ( y e. x -> y e. T ) )
23	22	rexlimdva	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( E. x e. ( R1 " _om ) y e. x -> y e. T ) )
24	4 23	biimtrid	|- ( ( T e. Tarski /\ T =/= (/) ) -> ( y e. HF -> y e. T ) )
25	24	ssrdv	|- ( ( T e. Tarski /\ T =/= (/) ) -> HF C_ T )