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	Could not format assertion : No typesetting found for |- ( ( T e. Tarski /\ T =/= (/) ) -> HF C_ T ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-hf	Could not format HF = U. ( R1 " _om ) : No typesetting found for |- HF = U. ( R1 " _om ) with typecode |-
2	1	eleq2i	Could not format ( y e. HF <-> y e. U. ( R1 " _om ) ) : No typesetting found for |- ( y e. HF <-> y e. U. ( R1 " _om ) ) with typecode |-
3		eluni2	$$⊢y\in \bigcup R_1\left[\mathrm{\omega }\right]\leftrightarrow \exists x\in R_1\left[\mathrm{\omega }\right]y\in x$$
4	2 3	bitri	Could not format ( y e. HF <-> E. x e. ( R1 " _om ) y e. x ) : No typesetting found for |- ( y e. HF <-> E. x e. ( R1 " _om ) y e. x ) with typecode |-
5		r1fnon	$$⊢R_{1}Fn\mathrm{On}$$
6		fnfun	$$⊢R_{1}Fn\mathrm{On}\to \mathrm{Fun}{R}_1$$
7	5 6	ax-mp	$$⊢\mathrm{Fun}{R}_1$$
8		fvelima	$$⊢\left(\mathrm{Fun}{R}_1\wedge x\in R_1\left[\mathrm{\omega }\right]\right)\to \exists y\in \mathrm{\omega }{R}_1\left(y\right)=x$$
9	7 8	mpan	$$⊢x\in R_1\left[\mathrm{\omega }\right]\to \exists y\in \mathrm{\omega }{R}_1\left(y\right)=x$$
10		r1tr	$$⊢\mathrm{Tr}{R}_1\left(y\right)$$
11		treq	$$⊢R_1\left(y\right)=x\to \left(\mathrm{Tr}{R}_1\left(y\right)\leftrightarrow \mathrm{Tr}x\right)$$
12	10 11	mpbii	$$⊢R_1\left(y\right)=x\to \mathrm{Tr}x$$
13	12	rexlimivw	$$⊢\exists y\in \mathrm{\omega }{R}_1\left(y\right)=x\to \mathrm{Tr}x$$
14		trss	$$⊢\mathrm{Tr}x\to \left(y\in x\to y\subseteq x\right)$$
15	9 13 14	3syl	$$⊢x\in R_1\left[\mathrm{\omega }\right]\to \left(y\in x\to y\subseteq x\right)$$
16	15	adantl	$$⊢\left(\left(T\in \mathrm{Tarski}\wedge T\ne \varnothing \right)\wedge x\in R_1\left[\mathrm{\omega }\right]\right)\to \left(y\in x\to y\subseteq x\right)$$
17		tskr1om	$$⊢\left(T\in \mathrm{Tarski}\wedge T\ne \varnothing \right)\to R_1\left[\mathrm{\omega }\right]\subseteq T$$
18	17	sseld	$$⊢\left(T\in \mathrm{Tarski}\wedge T\ne \varnothing \right)\to \left(x\in R_1\left[\mathrm{\omega }\right]\to x\in T\right)$$
19		tskss	$$⊢\left(T\in \mathrm{Tarski}\wedge x\in T\wedge y\subseteq x\right)\to y\in T$$
20	19	3exp	$$⊢T\in \mathrm{Tarski}\to \left(x\in T\to \left(y\subseteq x\to y\in T\right)\right)$$
21	20	adantr	$$⊢\left(T\in \mathrm{Tarski}\wedge T\ne \varnothing \right)\to \left(x\in T\to \left(y\subseteq x\to y\in T\right)\right)$$
22	18 21	syld	$$⊢\left(T\in \mathrm{Tarski}\wedge T\ne \varnothing \right)\to \left(x\in R_1\left[\mathrm{\omega }\right]\to \left(y\subseteq x\to y\in T\right)\right)$$
23	22	imp	$$⊢\left(\left(T\in \mathrm{Tarski}\wedge T\ne \varnothing \right)\wedge x\in R_1\left[\mathrm{\omega }\right]\right)\to \left(y\subseteq x\to y\in T\right)$$
24	16 23	syld	$$⊢\left(\left(T\in \mathrm{Tarski}\wedge T\ne \varnothing \right)\wedge x\in R_1\left[\mathrm{\omega }\right]\right)\to \left(y\in x\to y\in T\right)$$
25	24	rexlimdva	$$⊢\left(T\in \mathrm{Tarski}\wedge T\ne \varnothing \right)\to \left(\exists x\in R_1\left[\mathrm{\omega }\right]y\in x\to y\in T\right)$$
26	4 25	biimtrid	Could not format ( ( T e. Tarski /\ T =/= (/) ) -> ( y e. HF -> y e. T ) ) : No typesetting found for |- ( ( T e. Tarski /\ T =/= (/) ) -> ( y e. HF -> y e. T ) ) with typecode |-
27	26	ssrdv	Could not format ( ( T e. Tarski /\ T =/= (/) ) -> HF C_ T ) : No typesetting found for |- ( ( T e. Tarski /\ T =/= (/) ) -> HF C_ T ) with typecode |-