Theorem ssrel2

Description: A subclass relationship depends only on a relation's ordered pairs. This version of ssrel is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018)

	Ref	Expression
Assertion	ssrel2	$$⊢R\subseteq A\times B\to \left(R\subseteq S\leftrightarrow \forall x\in A\forall y\in B\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssel	$$⊢R\subseteq S\to \left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)$$
2	1	a1d	$$⊢R\subseteq S\to \left(\left(x\in A\wedge y\in B\right)\to \left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\right)$$
3	2	ralrimivv	$$⊢R\subseteq S\to \forall x\in A\forall y\in B\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)$$
4		eleq1	$$⊢z=⟨x,y⟩\to \left(z\in R\leftrightarrow ⟨x,y⟩\in R\right)$$
5		eleq1	$$⊢z=⟨x,y⟩\to \left(z\in S\leftrightarrow ⟨x,y⟩\in S\right)$$
6	4 5	imbi12d	$$⊢z=⟨x,y⟩\to \left(\left(z\in R\to z\in S\right)\leftrightarrow \left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\right)$$
7	6	biimprcd	$$⊢\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\to \left(z=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)$$
8	7	2ralimi	$$⊢\forall x\in A\forall y\in B\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\to \forall x\in A\forall y\in B\left(z=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)$$
9		r19.23v	$$⊢\forall y\in B\left(z=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)\leftrightarrow \left(\exists y\in Bz=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)$$
10	9	ralbii	$$⊢\forall x\in A\forall y\in B\left(z=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)\leftrightarrow \forall x\in A\left(\exists y\in Bz=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)$$
11		r19.23v	$$⊢\forall x\in A\left(\exists y\in Bz=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)\leftrightarrow \left(\exists x\in A\exists y\in Bz=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)$$
12	10 11	bitri	$$⊢\forall x\in A\forall y\in B\left(z=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)\leftrightarrow \left(\exists x\in A\exists y\in Bz=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)$$
13	8 12	sylib	$$⊢\forall x\in A\forall y\in B\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\to \left(\exists x\in A\exists y\in Bz=⟨x,y⟩\to \left(z\in R\to z\in S\right)\right)$$
14	13	com23	$$⊢\forall x\in A\forall y\in B\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\to \left(z\in R\to \left(\exists x\in A\exists y\in Bz=⟨x,y⟩\to z\in S\right)\right)$$
15	14	a2d	$$⊢\forall x\in A\forall y\in B\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\to \left(\left(z\in R\to \exists x\in A\exists y\in Bz=⟨x,y⟩\right)\to \left(z\in R\to z\in S\right)\right)$$
16	15	alimdv	$$⊢\forall x\in A\forall y\in B\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\to \left(\forall z\left(z\in R\to \exists x\in A\exists y\in Bz=⟨x,y⟩\right)\to \forall z\left(z\in R\to z\in S\right)\right)$$
17		df-ss	$$⊢R\subseteq A\times B\leftrightarrow \forall z\left(z\in R\to z\in \left(A\times B\right)\right)$$
18		elxp2	$$⊢z\in \left(A\times B\right)\leftrightarrow \exists x\in A\exists y\in Bz=⟨x,y⟩$$
19	18	imbi2i	$$⊢\left(z\in R\to z\in \left(A\times B\right)\right)\leftrightarrow \left(z\in R\to \exists x\in A\exists y\in Bz=⟨x,y⟩\right)$$
20	19	albii	$$⊢\forall z\left(z\in R\to z\in \left(A\times B\right)\right)\leftrightarrow \forall z\left(z\in R\to \exists x\in A\exists y\in Bz=⟨x,y⟩\right)$$
21	17 20	bitri	$$⊢R\subseteq A\times B\leftrightarrow \forall z\left(z\in R\to \exists x\in A\exists y\in Bz=⟨x,y⟩\right)$$
22		df-ss	$$⊢R\subseteq S\leftrightarrow \forall z\left(z\in R\to z\in S\right)$$
23	16 21 22	3imtr4g	$$⊢\forall x\in A\forall y\in B\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\to \left(R\subseteq A\times B\to R\subseteq S\right)$$
24	23	com12	$$⊢R\subseteq A\times B\to \left(\forall x\in A\forall y\in B\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\to R\subseteq S\right)$$
25	3 24	impbid2	$$⊢R\subseteq A\times B\to \left(R\subseteq S\leftrightarrow \forall x\in A\forall y\in B\left(⟨x,y⟩\in R\to ⟨x,y⟩\in S\right)\right)$$