Theorem refimssco

Description: Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020)

	Ref	Expression
Assertion	refimssco	|- ( ( _I |` ( dom A u. ran A ) ) C_ A -> `' A C_ `' ( A o. A ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	|- ( z = x -> ( x A z <-> x A x ) )
2		breq1	|- ( z = x -> ( z A y <-> x A y ) )
3	1 2	anbi12d	|- ( z = x -> ( ( x A z /\ z A y ) <-> ( x A x /\ x A y ) ) )
4	3	biimprd	|- ( z = x -> ( ( x A x /\ x A y ) -> ( x A z /\ z A y ) ) )
5	4	spimevw	|- ( ( x A x /\ x A y ) -> E. z ( x A z /\ z A y ) )
6	5	ex	|- ( x A x -> ( x A y -> E. z ( x A z /\ z A y ) ) )
7	6	adantr	|- ( ( x A x /\ y A y ) -> ( x A y -> E. z ( x A z /\ z A y ) ) )
8	7	com12	|- ( x A y -> ( ( x A x /\ y A y ) -> E. z ( x A z /\ z A y ) ) )
9	8	a2i	|- ( ( x A y -> ( x A x /\ y A y ) ) -> ( x A y -> E. z ( x A z /\ z A y ) ) )
10		19.37v	|- ( E. z ( x A y -> ( x A z /\ z A y ) ) <-> ( x A y -> E. z ( x A z /\ z A y ) ) )
11	9 10	sylibr	|- ( ( x A y -> ( x A x /\ y A y ) ) -> E. z ( x A y -> ( x A z /\ z A y ) ) )
12	11	2alimi	|- ( A. x A. y ( x A y -> ( x A x /\ y A y ) ) -> A. x A. y E. z ( x A y -> ( x A z /\ z A y ) ) )
13		reflexg	|- ( ( _I |` ( dom A u. ran A ) ) C_ A <-> A. x A. y ( x A y -> ( x A x /\ y A y ) ) )
14		cnvssco	|- ( `' A C_ `' ( A o. A ) <-> A. x A. y E. z ( x A y -> ( x A z /\ z A y ) ) )
15	12 13 14	3imtr4i	|- ( ( _I |` ( dom A u. ran A ) ) C_ A -> `' A C_ `' ( A o. A ) )