prdsless

Description: Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015)

	Ref	Expression
Hypotheses	prdsbas.p	$⊢ P = S ⨉_{𝑠} R$
	prdsbas.s	$⊢ φ \to S \in V$
	prdsbas.r	$⊢ φ \to R \in W$
	prdsbas.b	$⊢ B = {Base}_{P}$
	prdsbas.i	$⊢ φ \to dom R = I$
	prdsle.l	$⊢ \underset{˙}{\leq} = \leq_{P}$
Assertion	prdsless	$⊢ φ \to \underset{˙}{\leq} \subseteq B \times B$

Step	Hyp	Ref	Expression
1		prdsbas.p	$⊢ P = S ⨉_{𝑠} R$
2		prdsbas.s	$⊢ φ \to S \in V$
3		prdsbas.r	$⊢ φ \to R \in W$
4		prdsbas.b	$⊢ B = {Base}_{P}$
5		prdsbas.i	$⊢ φ \to dom R = I$
6		prdsle.l	$⊢ \underset{˙}{\leq} = \leq_{P}$
7	1 2 3 4 5 6	prdsle	$⊢ φ \to \underset{˙}{\leq} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
8		vex	$⊢ f \in V$
9		vex	$⊢ g \in V$
10	8 9	prss	$⊢ (f \in B \land g \in B) \leftrightarrow \{f, g\} \subseteq B$
11	10	anbi1i	$⊢ ((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{R (x)} g (x)) \leftrightarrow (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))$
12	11	opabbii	$⊢ \{⟨f, g⟩ \| ((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{R (x)} g (x))\} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
13		opabssxp	$⊢ \{⟨f, g⟩ \| ((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{R (x)} g (x))\} \subseteq B \times B$
14	12 13	eqsstrri	$⊢ \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\} \subseteq B \times B$
15	7 14	eqsstrdi	$⊢ φ \to \underset{˙}{\leq} \subseteq B \times B$

Metamath Proof Explorer