Theorem brstruct

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

	Ref	Expression
Assertion	brstruct	$$⊢\mathrm{Rel}\mathrm{Struct}$$

Proof

Step	Hyp	Ref	Expression
1		df-struct	$$⊢\mathrm{Struct}=\left\{⟨f,x⟩|\left(x\in \left(\le \cap \left(\mathbb{N}\times \mathbb{N}\right)\right)\wedge \mathrm{Fun}\left(f\setminus \left\{\varnothing \right\}\right)\wedge \mathrm{dom}f\subseteq \dots \left(x\right)\right)\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\mathrm{Struct}$$