Theorem hfstructhf

Description: A converted HFStruct is a hereditarily finite set. (Contributed by Eric Schmidt, 29-Sep-2026)

	Ref	Expression
Assertion	hfstructhf	⊢ ( 𝐹 ∈ HFStruct → ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		dmco	⊢ dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) = ( ◡ ( ♯ ↾ ω ) “ dom 𝐹 )
2		hashomf1o	⊢ ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0
3		dff1o3	⊢ ( ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0 ↔ ( ( ♯ ↾ ω ) : ω –onto→ ℕ0 ∧ Fun ◡ ( ♯ ↾ ω ) ) )
4	2 3	mpbi	⊢ ( ( ♯ ↾ ω ) : ω –onto→ ℕ0 ∧ Fun ◡ ( ♯ ↾ ω ) )
5	4	simpri	⊢ Fun ◡ ( ♯ ↾ ω )
6		hfstructstruct	⊢ ( 𝐹 ∈ HFStruct → ∃ 𝑥 𝐹 Struct 𝑥 )
7		dmstructfi	⊢ ( 𝐹 Struct 𝑥 → dom 𝐹 ∈ Fin )
8	7	exlimiv	⊢ ( ∃ 𝑥 𝐹 Struct 𝑥 → dom 𝐹 ∈ Fin )
9	6 8	syl	⊢ ( 𝐹 ∈ HFStruct → dom 𝐹 ∈ Fin )
10		imafi	⊢ ( ( Fun ◡ ( ♯ ↾ ω ) ∧ dom 𝐹 ∈ Fin ) → ( ◡ ( ♯ ↾ ω ) “ dom 𝐹 ) ∈ Fin )
11	5 9 10	sylancr	⊢ ( 𝐹 ∈ HFStruct → ( ◡ ( ♯ ↾ ω ) “ dom 𝐹 ) ∈ Fin )
12	1 11	eqeltrid	⊢ ( 𝐹 ∈ HFStruct → dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ Fin )
13		dmcoss	⊢ dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) ⊆ dom ( ♯ ↾ ω )
14		dmhashres	⊢ dom ( ♯ ↾ ω ) = ω
15	13 14	sseqtri	⊢ dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) ⊆ ω
16		omsshf	⊢ ω ⊆ HF
17	15 16	sstri	⊢ dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) ⊆ HF
18		elhf3	⊢ ( dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF ↔ ( dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ Fin ∧ dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) ⊆ HF ) )
19	12 17 18	sylanblrc	⊢ ( 𝐹 ∈ HFStruct → dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF )
20		rncoss	⊢ ran ( 𝐹 ∘ ( ♯ ↾ ω ) ) ⊆ ran 𝐹
21		rnhfstructhf	⊢ ( 𝐹 ∈ HFStruct → ran 𝐹 ∈ HF )
22		hfsshf	⊢ ( ( ran ( 𝐹 ∘ ( ♯ ↾ ω ) ) ⊆ ran 𝐹 ∧ ran 𝐹 ∈ HF ) → ran ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF )
23	20 21 22	sylancr	⊢ ( 𝐹 ∈ HFStruct → ran ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF )
24		relco	⊢ Rel ( 𝐹 ∘ ( ♯ ↾ ω ) )
25		hfrel	⊢ ( Rel ( 𝐹 ∘ ( ♯ ↾ ω ) ) → ( ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF ↔ ( dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF ∧ ran ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF ) ) )
26	24 25	ax-mp	⊢ ( ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF ↔ ( dom ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF ∧ ran ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF ) )
27	19 23 26	sylanbrc	⊢ ( 𝐹 ∈ HFStruct → ( 𝐹 ∘ ( ♯ ↾ ω ) ) ∈ HF )