Metamath Proof Explorer

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 
|- ( ( F e. HFStruct /\ G e. HFStruct ) -> ( ( F o. ( # |` _om ) ) = ( G o. ( # |` _om ) ) <-> F = G ) )

Proof

Step Hyp Ref Expression
1 hashomf1o 
 |-  ( # |` _om ) : _om -1-1-onto-> NN0
2 f1ofun 
 |-  ( ( # |` _om ) : _om -1-1-onto-> NN0 -> Fun ( # |` _om ) )
3 1 2 mp1i 
 |-  ( ( F e. HFStruct /\ G e. HFStruct ) -> Fun ( # |` _om ) )
4 hfstructfun 
 |-  ( F e. HFStruct -> Fun F )
5 funrel 
 |-  ( Fun F -> Rel F )
6 4 5 syl 
 |-  ( F e. HFStruct -> Rel F )
7 6 adantr 
 |-  ( ( F e. HFStruct /\ G e. HFStruct ) -> Rel F )
8 hfstructstruct 
 |-  ( F e. HFStruct -> E. x F Struct x )
9 dmstructnn 
 |-  ( F Struct x -> dom F C_ NN )
10 nnssnn0 
 |-  NN C_ NN0
11 9 10 sstrdi 
 |-  ( F Struct x -> dom F C_ NN0 )
12 dff1o5 
 |-  ( ( # |` _om ) : _om -1-1-onto-> NN0 <-> ( ( # |` _om ) : _om -1-1-> NN0 /\ ran ( # |` _om ) = NN0 ) )
13 1 12 mpbi 
 |-  ( ( # |` _om ) : _om -1-1-> NN0 /\ ran ( # |` _om ) = NN0 )
14 13 simpri 
 |-  ran ( # |` _om ) = NN0
15 11 14 sseqtrrdi 
 |-  ( F Struct x -> dom F C_ ran ( # |` _om ) )
16 15 exlimiv 
 |-  ( E. x F Struct x -> dom F C_ ran ( # |` _om ) )
17 8 16 syl 
 |-  ( F e. HFStruct -> dom F C_ ran ( # |` _om ) )
18 17 adantr 
 |-  ( ( F e. HFStruct /\ G e. HFStruct ) -> dom F C_ ran ( # |` _om ) )
19 hfstructfun 
 |-  ( G e. HFStruct -> Fun G )
20 funrel 
 |-  ( Fun G -> Rel G )
21 19 20 syl 
 |-  ( G e. HFStruct -> Rel G )
22 21 adantl 
 |-  ( ( F e. HFStruct /\ G e. HFStruct ) -> Rel G )
23 hfstructstruct 
 |-  ( G e. HFStruct -> E. x G Struct x )
24 dmstructnn 
 |-  ( G Struct x -> dom G C_ NN )
25 24 10 sstrdi 
 |-  ( G Struct x -> dom G C_ NN0 )
26 25 14 sseqtrrdi 
 |-  ( G Struct x -> dom G C_ ran ( # |` _om ) )
27 26 exlimiv 
 |-  ( E. x G Struct x -> dom G C_ ran ( # |` _om ) )
28 23 27 syl 
 |-  ( G e. HFStruct -> dom G C_ ran ( # |` _om ) )
29 28 adantl 
 |-  ( ( F e. HFStruct /\ G e. HFStruct ) -> dom G C_ ran ( # |` _om ) )
30 3 7 18 22 29 cocan2g 
 |-  ( ( F e. HFStruct /\ G e. HFStruct ) -> ( ( F o. ( # |` _om ) ) = ( G o. ( # |` _om ) ) <-> F = G ) )