refimssco

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

		Ref	Expression
	Assertion	refimssco	$⊢ {I ↾}_{(dom A \cup ran A)} \subseteq A \to A^{-1} \subseteq {(A \circ A)}^{-1}$

Step	Hyp	Ref	Expression
1		breq2	$⊢ z = x \to (x A z \leftrightarrow x A x)$
2		breq1	$⊢ z = x \to (z A y \leftrightarrow x A y)$
3	1 2	anbi12d	$⊢ z = x \to ((x A z \land z A y) \leftrightarrow (x A x \land x A y))$
4	3	biimprd	$⊢ z = x \to ((x A x \land x A y) \to (x A z \land z A y))$
5	4	spimevw	$⊢ (x A x \land x A y) \to \exists z (x A z \land z A y)$
6	5	ex	$⊢ x A x \to (x A y \to \exists z (x A z \land z A y))$
7	6	adantr	$⊢ (x A x \land y A y) \to (x A y \to \exists z (x A z \land z A y))$
8	7	com12	$⊢ x A y \to ((x A x \land y A y) \to \exists z (x A z \land z A y))$
9	8	a2i	$⊢ (x A y \to (x A x \land y A y)) \to (x A y \to \exists z (x A z \land z A y))$
10		19.37v	$⊢ \exists z (x A y \to (x A z \land z A y)) \leftrightarrow (x A y \to \exists z (x A z \land z A y))$
11	9 10	sylibr	$⊢ (x A y \to (x A x \land y A y)) \to \exists z (x A y \to (x A z \land z A y))$
12	11	2alimi	$⊢ \forall x \forall y (x A y \to (x A x \land y A y)) \to \forall x \forall y \exists z (x A y \to (x A z \land z A y))$
13		reflexg	$⊢ {I ↾}_{(dom A \cup ran A)} \subseteq A \leftrightarrow \forall x \forall y (x A y \to (x A x \land y A y))$
14		cnvssco	$⊢ A^{-1} \subseteq {(A \circ A)}^{-1} \leftrightarrow \forall x \forall y \exists z (x A y \to (x A z \land z A y))$
15	12 13 14	3imtr4i	$⊢ {I ↾}_{(dom A \cup ran A)} \subseteq A \to A^{-1} \subseteq {(A \circ A)}^{-1}$

Metamath Proof Explorer