Metamath Proof Explorer

Theorem idsset

Description: _I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Assertion idsset 
|- _I = ( SSet i^i `' SSet )

Proof

Step Hyp Ref Expression
1 reli 
 |-  Rel _I
2 relsset 
 |-  Rel SSet
3 relin1 
 |-  ( Rel SSet -> Rel ( SSet i^i `' SSet ) )
4 2 3 ax-mp 
 |-  Rel ( SSet i^i `' SSet )
5 eqss 
 |-  ( y = z <-> ( y C_ z /\ z C_ y ) )
6 vex 
 |-  z e. _V
7 6 ideq 
 |-  ( y _I z <-> y = z )
8 brin 
 |-  ( y ( SSet i^i `' SSet ) z <-> ( y SSet z /\ y `' SSet z ) )
9 6 brsset 
 |-  ( y SSet z <-> y C_ z )
10 vex 
 |-  y e. _V
11 10 6 brcnv 
 |-  ( y `' SSet z <-> z SSet y )
12 10 brsset 
 |-  ( z SSet y <-> z C_ y )
13 11 12 bitri 
 |-  ( y `' SSet z <-> z C_ y )
14 9 13 anbi12i 
 |-  ( ( y SSet z /\ y `' SSet z ) <-> ( y C_ z /\ z C_ y ) )
15 8 14 bitri 
 |-  ( y ( SSet i^i `' SSet ) z <-> ( y C_ z /\ z C_ y ) )
16 5 7 15 3bitr4i 
 |-  ( y _I z <-> y ( SSet i^i `' SSet ) z )
17 1 4 16 eqbrriv 
 |-  _I = ( SSet i^i `' SSet )