Metamath Proof Explorer

Theorem isstruct2

Description: The property of being a structure with components in ( 1stX ) ... ( 2ndX ) . (Contributed by Mario Carneiro, 29-Aug-2015)

Ref Expression
Assertion isstruct2 
|- ( F Struct X <-> ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) )

Proof

Step Hyp Ref Expression
1 brstruct 
 |-  Rel Struct
2 1 brrelex12i 
 |-  ( F Struct X -> ( F e. _V /\ X e. _V ) )
3 ssun1 
 |-  F C_ ( F u. { (/) } )
4 undif1 
 |-  ( ( F \ { (/) } ) u. { (/) } ) = ( F u. { (/) } )
5 3 4 sseqtrri 
 |-  F C_ ( ( F \ { (/) } ) u. { (/) } )
6 simp2 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> Fun ( F \ { (/) } ) )
7 6 funfnd 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> ( F \ { (/) } ) Fn dom ( F \ { (/) } ) )
8 elinel2 
 |-  ( X e. ( <_ i^i ( NN X. NN ) ) -> X e. ( NN X. NN ) )
9 1st2nd2 
 |-  ( X e. ( NN X. NN ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
10 8 9 syl 
 |-  ( X e. ( <_ i^i ( NN X. NN ) ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
11 10 3ad2ant1 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
12 11 fveq2d 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> ( ... ` X ) = ( ... ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
13 df-ov 
 |-  ( ( 1st ` X ) ... ( 2nd ` X ) ) = ( ... ` <. ( 1st ` X ) , ( 2nd ` X ) >. )
14 fzfi 
 |-  ( ( 1st ` X ) ... ( 2nd ` X ) ) e. Fin
15 13 14 eqeltrri 
 |-  ( ... ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) e. Fin
16 12 15 eqeltrdi 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> ( ... ` X ) e. Fin )
17 difss 
 |-  ( F \ { (/) } ) C_ F
18 dmss 
 |-  ( ( F \ { (/) } ) C_ F -> dom ( F \ { (/) } ) C_ dom F )
19 17 18 ax-mp 
 |-  dom ( F \ { (/) } ) C_ dom F
20 simp3 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> dom F C_ ( ... ` X ) )
21 19 20 sstrid 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> dom ( F \ { (/) } ) C_ ( ... ` X ) )
22 16 21 ssfid 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> dom ( F \ { (/) } ) e. Fin )
23 fnfi 
 |-  ( ( ( F \ { (/) } ) Fn dom ( F \ { (/) } ) /\ dom ( F \ { (/) } ) e. Fin ) -> ( F \ { (/) } ) e. Fin )
24 7 22 23 syl2anc 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> ( F \ { (/) } ) e. Fin )
25 p0ex 
 |-  { (/) } e. _V
26 unexg 
 |-  ( ( ( F \ { (/) } ) e. Fin /\ { (/) } e. _V ) -> ( ( F \ { (/) } ) u. { (/) } ) e. _V )
27 24 25 26 sylancl 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> ( ( F \ { (/) } ) u. { (/) } ) e. _V )
28 ssexg 
 |-  ( ( F C_ ( ( F \ { (/) } ) u. { (/) } ) /\ ( ( F \ { (/) } ) u. { (/) } ) e. _V ) -> F e. _V )
29 5 27 28 sylancr 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> F e. _V )
30 elex 
 |-  ( X e. ( <_ i^i ( NN X. NN ) ) -> X e. _V )
31 30 3ad2ant1 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> X e. _V )
32 29 31 jca 
 |-  ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) -> ( F e. _V /\ X e. _V ) )
33 simpr 
 |-  ( ( f = F /\ x = X ) -> x = X )
34 33 eleq1d 
 |-  ( ( f = F /\ x = X ) -> ( x e. ( <_ i^i ( NN X. NN ) ) <-> X e. ( <_ i^i ( NN X. NN ) ) ) )
35 simpl 
 |-  ( ( f = F /\ x = X ) -> f = F )
36 35 difeq1d 
 |-  ( ( f = F /\ x = X ) -> ( f \ { (/) } ) = ( F \ { (/) } ) )
37 36 funeqd 
 |-  ( ( f = F /\ x = X ) -> ( Fun ( f \ { (/) } ) <-> Fun ( F \ { (/) } ) ) )
38 35 dmeqd 
 |-  ( ( f = F /\ x = X ) -> dom f = dom F )
39 33 fveq2d 
 |-  ( ( f = F /\ x = X ) -> ( ... ` x ) = ( ... ` X ) )
40 38 39 sseq12d 
 |-  ( ( f = F /\ x = X ) -> ( dom f C_ ( ... ` x ) <-> dom F C_ ( ... ` X ) ) )
41 34 37 40 3anbi123d 
 |-  ( ( f = F /\ x = X ) -> ( ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) <-> ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) ) )
42 df-struct 
 |-  Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
43 41 42 brabga 
 |-  ( ( F e. _V /\ X e. _V ) -> ( F Struct X <-> ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) ) )
44 2 32 43 pm5.21nii 
 |-  ( F Struct X <-> ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) )