Theorem isstruct

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

	Ref	Expression
Assertion	isstruct	⊢ ( 𝐹 Struct ⟨ 𝑀 , 𝑁 ⟩ ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑀 ... 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isstruct2	⊢ ( 𝐹 Struct ⟨ 𝑀 , 𝑁 ⟩ ↔ ( ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) )
2		df-3an	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑀 ≤ 𝑁 ) )
3		brinxp2	⊢ ( 𝑀 ( ≤ ∩ ( ℕ × ℕ ) ) 𝑁 ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑀 ≤ 𝑁 ) )
4		df-br	⊢ ( 𝑀 ( ≤ ∩ ( ℕ × ℕ ) ) 𝑁 ↔ ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ≤ ∩ ( ℕ × ℕ ) ) )
5	2 3 4	3bitr2i	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ↔ ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ≤ ∩ ( ℕ × ℕ ) ) )
6		biid	⊢ ( Fun ( 𝐹 ∖ { ∅ } ) ↔ Fun ( 𝐹 ∖ { ∅ } ) )
7		df-ov	⊢ ( 𝑀 ... 𝑁 ) = ( ... ‘ ⟨ 𝑀 , 𝑁 ⟩ )
8	7	sseq2i	⊢ ( dom 𝐹 ⊆ ( 𝑀 ... 𝑁 ) ↔ dom 𝐹 ⊆ ( ... ‘ ⟨ 𝑀 , 𝑁 ⟩ ) )
9	5 6 8	3anbi123i	⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑀 ... 𝑁 ) ) ↔ ( ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) )
10	1 9	bitr4i	⊢ ( 𝐹 Struct ⟨ 𝑀 , 𝑁 ⟩ ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑀 ... 𝑁 ) ) )