Theorem oprabss

Description: Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006)

	Ref	Expression
Assertion	oprabss	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		reloprab	$$⊢\mathrm{Rel}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
2		relssdmrn	$$⊢\mathrm{Rel}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\times \mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
3	1 2	ax-mp	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\times \mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
4		reldmoprab	$$⊢\mathrm{Rel}\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
5		df-rel	$$⊢\mathrm{Rel}\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\leftrightarrow \mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}$$
6	4 5	mpbi	$$⊢\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}$$
7		ssv	$$⊢\mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \mathrm{V}$$
8		xpss12	$$⊢\left(\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \mathrm{V}\times \mathrm{V}\wedge \mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \mathrm{V}\right)\to \mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\times \mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}$$
9	6 7 8	mp2an	$$⊢\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\times \mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}$$
10	3 9	sstri	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}$$