Metamath Proof Explorer

Theorem brstruct

Description: The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015)

Ref Expression
Assertion brstruct 
|- Rel Struct

Proof

Step Hyp Ref Expression
1 df-struct 
 |-  Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
2 1 relopabiv 
 |-  Rel Struct