oprabss

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

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

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

Metamath Proof Explorer