Metamath Proof Explorer

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 
|- ( F Struct <. M , N >. <-> ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( M ... N ) ) )

Proof

Step Hyp Ref Expression
1 isstruct2 
 |-  ( F Struct <. M , N >. <-> ( <. M , N >. e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` <. M , N >. ) ) )
2 df-3an 
 |-  ( ( M e. NN /\ N e. NN /\ M <_ N ) <-> ( ( M e. NN /\ N e. NN ) /\ M <_ N ) )
3 brinxp2 
 |-  ( M ( <_ i^i ( NN X. NN ) ) N <-> ( ( M e. NN /\ N e. NN ) /\ M <_ N ) )
4 df-br 
 |-  ( M ( <_ i^i ( NN X. NN ) ) N <-> <. M , N >. e. ( <_ i^i ( NN X. NN ) ) )
5 2 3 4 3bitr2i 
 |-  ( ( M e. NN /\ N e. NN /\ M <_ N ) <-> <. M , N >. e. ( <_ i^i ( NN X. NN ) ) )
6 biid 
 |-  ( Fun ( F \ { (/) } ) <-> Fun ( F \ { (/) } ) )
7 df-ov 
 |-  ( M ... N ) = ( ... ` <. M , N >. )
8 7 sseq2i 
 |-  ( dom F C_ ( M ... N ) <-> dom F C_ ( ... ` <. M , N >. ) )
9 5 6 8 3anbi123i 
 |-  ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( M ... N ) ) <-> ( <. M , N >. e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` <. M , N >. ) ) )
10 1 9 bitr4i 
 |-  ( F Struct <. M , N >. <-> ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( M ... N ) ) )