Metamath Proof Explorer

Theorem structcnvcnv

Description: Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015)

Ref Expression
Assertion structcnvcnv 
|- ( F Struct X -> `' `' F = ( F \ { (/) } ) )

Proof

Step Hyp Ref Expression
1 0nelxp 
 |-  -. (/) e. ( _V X. _V )
2 cnvcnv 
 |-  `' `' F = ( F i^i ( _V X. _V ) )
3 inss2 
 |-  ( F i^i ( _V X. _V ) ) C_ ( _V X. _V )
4 2 3 eqsstri 
 |-  `' `' F C_ ( _V X. _V )
5 4 sseli 
 |-  ( (/) e. `' `' F -> (/) e. ( _V X. _V ) )
6 1 5 mto 
 |-  -. (/) e. `' `' F
7 disjsn 
 |-  ( ( `' `' F i^i { (/) } ) = (/) <-> -. (/) e. `' `' F )
8 6 7 mpbir 
 |-  ( `' `' F i^i { (/) } ) = (/)
9 cnvcnvss 
 |-  `' `' F C_ F
10 reldisj 
 |-  ( `' `' F C_ F -> ( ( `' `' F i^i { (/) } ) = (/) <-> `' `' F C_ ( F \ { (/) } ) ) )
11 9 10 ax-mp 
 |-  ( ( `' `' F i^i { (/) } ) = (/) <-> `' `' F C_ ( F \ { (/) } ) )
12 8 11 mpbi 
 |-  `' `' F C_ ( F \ { (/) } )
13 12 a1i 
 |-  ( F Struct X -> `' `' F C_ ( F \ { (/) } ) )
14 structn0fun 
 |-  ( F Struct X -> Fun ( F \ { (/) } ) )
15 funrel 
 |-  ( Fun ( F \ { (/) } ) -> Rel ( F \ { (/) } ) )
16 14 15 syl 
 |-  ( F Struct X -> Rel ( F \ { (/) } ) )
17 dfrel2 
 |-  ( Rel ( F \ { (/) } ) <-> `' `' ( F \ { (/) } ) = ( F \ { (/) } ) )
18 16 17 sylib 
 |-  ( F Struct X -> `' `' ( F \ { (/) } ) = ( F \ { (/) } ) )
19 difss 
 |-  ( F \ { (/) } ) C_ F
20 cnvss 
 |-  ( ( F \ { (/) } ) C_ F -> `' ( F \ { (/) } ) C_ `' F )
21 cnvss 
 |-  ( `' ( F \ { (/) } ) C_ `' F -> `' `' ( F \ { (/) } ) C_ `' `' F )
22 19 20 21 mp2b 
 |-  `' `' ( F \ { (/) } ) C_ `' `' F
23 18 22 eqsstrrdi 
 |-  ( F Struct X -> ( F \ { (/) } ) C_ `' `' F )
24 13 23 eqssd 
 |-  ( F Struct X -> `' `' F = ( F \ { (/) } ) )