isstruct

Description: The property of being a structure with components in M ... N . (Contributed by Mario Carneiro, 29-Aug-2015)

		Ref	Expression
	Assertion	isstruct	$⊢ F Struct ⟨M, N⟩ \leftrightarrow ((M \in ℕ \land N \in ℕ \land M \leq N) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq (M \dots N))$

Step	Hyp	Ref	Expression
1		isstruct2	$⊢ F Struct ⟨M, N⟩ \leftrightarrow (⟨M, N⟩ \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (⟨M, N⟩))$
2		df-3an	$⊢ (M \in ℕ \land N \in ℕ \land M \leq N) \leftrightarrow ((M \in ℕ \land N \in ℕ) \land M \leq N)$
3		brinxp2	$⊢ M (\leq \cap (ℕ \times ℕ)) N \leftrightarrow ((M \in ℕ \land N \in ℕ) \land M \leq N)$
4		df-br	$⊢ M (\leq \cap (ℕ \times ℕ)) N \leftrightarrow ⟨M, N⟩ \in (\leq \cap (ℕ \times ℕ))$
5	2 3 4	3bitr2i	$⊢ (M \in ℕ \land N \in ℕ \land M \leq N) \leftrightarrow ⟨M, N⟩ \in (\leq \cap (ℕ \times ℕ))$
6		biid	$⊢ Fun (F ∖ \{\emptyset\}) \leftrightarrow Fun (F ∖ \{\emptyset\})$
7		df-ov	$⊢ (M \dots N) = \dots (⟨M, N⟩)$
8	7	sseq2i	$⊢ dom F \subseteq (M \dots N) \leftrightarrow dom F \subseteq \dots (⟨M, N⟩)$
9	5 6 8	3anbi123i	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq (M \dots N)) \leftrightarrow (⟨M, N⟩ \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (⟨M, N⟩))$
10	1 9	bitr4i	$⊢ F Struct ⟨M, N⟩ \leftrightarrow ((M \in ℕ \land N \in ℕ \land M \leq N) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq (M \dots N))$

Metamath Proof Explorer