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 ) ) )