Theorem hfstructcan

Description: Two HFStructs are equal if and only if their converted forms are equal. (Contributed by Eric Schmidt, 29-Sep-2026)

	Ref	Expression
Assertion	hfstructcan	⊢ ( ( 𝐹 ∈ HFStruct ∧ 𝐺 ∈ HFStruct ) → ( ( 𝐹 ∘ ( ♯ ↾ ω ) ) = ( 𝐺 ∘ ( ♯ ↾ ω ) ) ↔ 𝐹 = 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		hashomf1o	⊢ ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0
2		f1ofun	⊢ ( ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0 → Fun ( ♯ ↾ ω ) )
3	1 2	mp1i	⊢ ( ( 𝐹 ∈ HFStruct ∧ 𝐺 ∈ HFStruct ) → Fun ( ♯ ↾ ω ) )
4		hfstructfun	⊢ ( 𝐹 ∈ HFStruct → Fun 𝐹 )
5		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
6	4 5	syl	⊢ ( 𝐹 ∈ HFStruct → Rel 𝐹 )
7	6	adantr	⊢ ( ( 𝐹 ∈ HFStruct ∧ 𝐺 ∈ HFStruct ) → Rel 𝐹 )
8		hfstructstruct	⊢ ( 𝐹 ∈ HFStruct → ∃ 𝑥 𝐹 Struct 𝑥 )
9		dmstructnn	⊢ ( 𝐹 Struct 𝑥 → dom 𝐹 ⊆ ℕ )
10		nnssnn0	⊢ ℕ ⊆ ℕ0
11	9 10	sstrdi	⊢ ( 𝐹 Struct 𝑥 → dom 𝐹 ⊆ ℕ0 )
12		dff1o5	⊢ ( ( ♯ ↾ ω ) : ω –1-1-onto→ ℕ0 ↔ ( ( ♯ ↾ ω ) : ω –1-1→ ℕ0 ∧ ran ( ♯ ↾ ω ) = ℕ0 ) )
13	1 12	mpbi	⊢ ( ( ♯ ↾ ω ) : ω –1-1→ ℕ0 ∧ ran ( ♯ ↾ ω ) = ℕ0 )
14	13	simpri	⊢ ran ( ♯ ↾ ω ) = ℕ0
15	11 14	sseqtrrdi	⊢ ( 𝐹 Struct 𝑥 → dom 𝐹 ⊆ ran ( ♯ ↾ ω ) )
16	15	exlimiv	⊢ ( ∃ 𝑥 𝐹 Struct 𝑥 → dom 𝐹 ⊆ ran ( ♯ ↾ ω ) )
17	8 16	syl	⊢ ( 𝐹 ∈ HFStruct → dom 𝐹 ⊆ ran ( ♯ ↾ ω ) )
18	17	adantr	⊢ ( ( 𝐹 ∈ HFStruct ∧ 𝐺 ∈ HFStruct ) → dom 𝐹 ⊆ ran ( ♯ ↾ ω ) )
19		hfstructfun	⊢ ( 𝐺 ∈ HFStruct → Fun 𝐺 )
20		funrel	⊢ ( Fun 𝐺 → Rel 𝐺 )
21	19 20	syl	⊢ ( 𝐺 ∈ HFStruct → Rel 𝐺 )
22	21	adantl	⊢ ( ( 𝐹 ∈ HFStruct ∧ 𝐺 ∈ HFStruct ) → Rel 𝐺 )
23		hfstructstruct	⊢ ( 𝐺 ∈ HFStruct → ∃ 𝑥 𝐺 Struct 𝑥 )
24		dmstructnn	⊢ ( 𝐺 Struct 𝑥 → dom 𝐺 ⊆ ℕ )
25	24 10	sstrdi	⊢ ( 𝐺 Struct 𝑥 → dom 𝐺 ⊆ ℕ0 )
26	25 14	sseqtrrdi	⊢ ( 𝐺 Struct 𝑥 → dom 𝐺 ⊆ ran ( ♯ ↾ ω ) )
27	26	exlimiv	⊢ ( ∃ 𝑥 𝐺 Struct 𝑥 → dom 𝐺 ⊆ ran ( ♯ ↾ ω ) )
28	23 27	syl	⊢ ( 𝐺 ∈ HFStruct → dom 𝐺 ⊆ ran ( ♯ ↾ ω ) )
29	28	adantl	⊢ ( ( 𝐹 ∈ HFStruct ∧ 𝐺 ∈ HFStruct ) → dom 𝐺 ⊆ ran ( ♯ ↾ ω ) )
30	3 7 18 22 29	cocan2g	⊢ ( ( 𝐹 ∈ HFStruct ∧ 𝐺 ∈ HFStruct ) → ( ( 𝐹 ∘ ( ♯ ↾ ω ) ) = ( 𝐺 ∘ ( ♯ ↾ ω ) ) ↔ 𝐹 = 𝐺 ) )