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		r1fnon	⊢ 𝑅1 Fn On
6		fnfun	⊢ ( 𝑅1 Fn On → Fun 𝑅1 )
7	5 6	ax-mp	⊢ Fun 𝑅1
8		fvelima	⊢ ( ( Fun 𝑅1 ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ∃ 𝑦 ∈ ω ( 𝑅1 ‘ 𝑦 ) = 𝑥 )
9	7 8	mpan	⊢ ( 𝑥 ∈ ( 𝑅1 “ ω ) → ∃ 𝑦 ∈ ω ( 𝑅1 ‘ 𝑦 ) = 𝑥 )
10		r1tr	⊢ Tr ( 𝑅1 ‘ 𝑦 )
11		treq	⊢ ( ( 𝑅1 ‘ 𝑦 ) = 𝑥 → ( Tr ( 𝑅1 ‘ 𝑦 ) ↔ Tr 𝑥 ) )
12	10 11	mpbii	⊢ ( ( 𝑅1 ‘ 𝑦 ) = 𝑥 → Tr 𝑥 )
13	12	rexlimivw	⊢ ( ∃ 𝑦 ∈ ω ( 𝑅1 ‘ 𝑦 ) = 𝑥 → Tr 𝑥 )
14		trss	⊢ ( Tr 𝑥 → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
15	9 13 14	3syl	⊢ ( 𝑥 ∈ ( 𝑅1 “ ω ) → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
16	15	adantl	⊢ ( ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
17		tskr1om	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑅1 “ ω ) ⊆ 𝑇 )
18	17	sseld	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑥 ∈ ( 𝑅1 “ ω ) → 𝑥 ∈ 𝑇 ) )
19		tskss	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ∈ 𝑇 )
20	19	3exp	⊢ ( 𝑇 ∈ Tarski → ( 𝑥 ∈ 𝑇 → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) ) )
21	20	adantr	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑥 ∈ 𝑇 → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) ) )
22	18 21	syld	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑥 ∈ ( 𝑅1 “ ω ) → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) ) )
23	22	imp	⊢ ( ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) )
24	16 23	syld	⊢ ( ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑇 ) )
25	24	rexlimdva	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( ∃ 𝑥 ∈ ( 𝑅1 “ ω ) 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑇 ) )
26	4 25	biimtrid	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑦 ∈ HF → 𝑦 ∈ 𝑇 ) )
27	26	ssrdv	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → HF ⊆ 𝑇 )