This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cossssid

Description: Equivalent expressions for the class of cosets by R to be a subset of the identity class. (Contributed by Peter Mazsa, 27-Jul-2021)

Ref Expression
Assertion cossssid 
|- ( ,~ R C_ _I <-> ,~ R C_ ( _I i^i ( dom ,~ R X. ran ,~ R ) ) )

Proof

Step Hyp Ref Expression
1 iss2 
 |-  ( ,~ R C_ _I <-> ,~ R = ( _I i^i ( dom ,~ R X. ran ,~ R ) ) )
2 refrelcoss2 
 |-  ( ( _I i^i ( dom ,~ R X. ran ,~ R ) ) C_ ,~ R /\ Rel ,~ R )
3 2 simpli 
 |-  ( _I i^i ( dom ,~ R X. ran ,~ R ) ) C_ ,~ R
4 eqss 
 |-  ( ,~ R = ( _I i^i ( dom ,~ R X. ran ,~ R ) ) <-> ( ,~ R C_ ( _I i^i ( dom ,~ R X. ran ,~ R ) ) /\ ( _I i^i ( dom ,~ R X. ran ,~ R ) ) C_ ,~ R ) )
5 3 4 mpbiran2 
 |-  ( ,~ R = ( _I i^i ( dom ,~ R X. ran ,~ R ) ) <-> ,~ R C_ ( _I i^i ( dom ,~ R X. ran ,~ R ) ) )
6 1 5 bitri 
 |-  ( ,~ R C_ _I <-> ,~ R C_ ( _I i^i ( dom ,~ R X. ran ,~ R ) ) )