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	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → HF ⊆ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		df-hf	⊢ HF = ∪ ( 𝑅1 “ ω )
2	1	eleq2i	⊢ ( 𝑦 ∈ HF ↔ 𝑦 ∈ ∪ ( 𝑅1 “ ω ) )
3		eluni2	⊢ ( 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ↔ ∃ 𝑥 ∈ ( 𝑅1 “ ω ) 𝑦 ∈ 𝑥 )
4	2 3	bitri	⊢ ( 𝑦 ∈ HF ↔ ∃ 𝑥 ∈ ( 𝑅1 “ ω ) 𝑦 ∈ 𝑥 )
5		r1fun	⊢ Fun 𝑅1
6		fvelima	⊢ ( ( Fun 𝑅1 ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ∃ 𝑦 ∈ ω ( 𝑅1 ‘ 𝑦 ) = 𝑥 )
7	5 6	mpan	⊢ ( 𝑥 ∈ ( 𝑅1 “ ω ) → ∃ 𝑦 ∈ ω ( 𝑅1 ‘ 𝑦 ) = 𝑥 )
8		r1tr	⊢ Tr ( 𝑅1 ‘ 𝑦 )
9		treq	⊢ ( ( 𝑅1 ‘ 𝑦 ) = 𝑥 → ( Tr ( 𝑅1 ‘ 𝑦 ) ↔ Tr 𝑥 ) )
10	8 9	mpbii	⊢ ( ( 𝑅1 ‘ 𝑦 ) = 𝑥 → Tr 𝑥 )
11	10	rexlimivw	⊢ ( ∃ 𝑦 ∈ ω ( 𝑅1 ‘ 𝑦 ) = 𝑥 → Tr 𝑥 )
12		trss	⊢ ( Tr 𝑥 → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
13	7 11 12	3syl	⊢ ( 𝑥 ∈ ( 𝑅1 “ ω ) → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
14	13	adantl	⊢ ( ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
15		tskr1om	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑅1 “ ω ) ⊆ 𝑇 )
16	15	sseld	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑥 ∈ ( 𝑅1 “ ω ) → 𝑥 ∈ 𝑇 ) )
17		tskss	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ∈ 𝑇 )
18	17	3exp	⊢ ( 𝑇 ∈ Tarski → ( 𝑥 ∈ 𝑇 → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) ) )
19	18	adantr	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑥 ∈ 𝑇 → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) ) )
20	16 19	syld	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑥 ∈ ( 𝑅1 “ ω ) → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) ) )
21	20	imp	⊢ ( ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) )
22	14 21	syld	⊢ ( ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑇 ) )
23	22	rexlimdva	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( ∃ 𝑥 ∈ ( 𝑅1 “ ω ) 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑇 ) )
24	4 23	biimtrid	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑦 ∈ HF → 𝑦 ∈ 𝑇 ) )
25	24	ssrdv	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → HF ⊆ 𝑇 )