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 = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑥 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝑓 ∖ { ∅ } ) ∧ dom 𝑓 ⊆ ( ... ‘ 𝑥 ) ) }
2	1	relopabi	⊢ Rel Struct