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