prdsleval

Description: Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

	Ref	Expression
Hypotheses	prdsbasmpt.y	$⊢ Y = S ⨉_{𝑠} R$
	prdsbasmpt.b	$⊢ B = {Base}_{Y}$
	prdsbasmpt.s	$⊢ φ \to S \in V$
	prdsbasmpt.i	$⊢ φ \to I \in W$
	prdsbasmpt.r	$⊢ φ \to R Fn I$
	prdsplusgval.f	$⊢ φ \to F \in B$
	prdsplusgval.g	$⊢ φ \to G \in B$
	prdsleval.l	$⊢ \underset{˙}{\leq} = \leq_{Y}$
Assertion	prdsleval	$⊢ φ \to (F \underset{˙}{\leq} G \leftrightarrow \forall x \in I F (x) \leq_{R (x)} G (x))$

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdsbasmpt.b	$⊢ B = {Base}_{Y}$
3		prdsbasmpt.s	$⊢ φ \to S \in V$
4		prdsbasmpt.i	$⊢ φ \to I \in W$
5		prdsbasmpt.r	$⊢ φ \to R Fn I$
6		prdsplusgval.f	$⊢ φ \to F \in B$
7		prdsplusgval.g	$⊢ φ \to G \in B$
8		prdsleval.l	$⊢ \underset{˙}{\leq} = \leq_{Y}$
9		df-br	$⊢ F \underset{˙}{\leq} G \leftrightarrow ⟨F, G⟩ \in \underset{˙}{\leq}$
10		fnex	$⊢ (R Fn I \land I \in W) \to R \in V$
11	5 4 10	syl2anc	$⊢ φ \to R \in V$
12	5	fndmd	$⊢ φ \to dom R = I$
13	1 3 11 2 12 8	prdsle	$⊢ φ \to \underset{˙}{\leq} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
14		vex	$⊢ f \in V$
15		vex	$⊢ g \in V$
16	14 15	prss	$⊢ (f \in B \land g \in B) \leftrightarrow \{f, g\} \subseteq B$
17	16	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))$
18	17	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))\}$
19	13 18	eqtr4di	$⊢ φ \to \underset{˙}{\leq} = \{⟨f, g⟩ \| ((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
20	19	eleq2d	$⊢ φ \to (⟨F, G⟩ \in \underset{˙}{\leq} \leftrightarrow ⟨F, G⟩ \in \{⟨f, g⟩ \| ((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{R (x)} g (x))\})$
21	9 20	bitrid	$⊢ φ \to (F \underset{˙}{\leq} G \leftrightarrow ⟨F, G⟩ \in \{⟨f, g⟩ \| ((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{R (x)} g (x))\})$
22		fveq1	$⊢ f = F \to f (x) = F (x)$
23		fveq1	$⊢ g = G \to g (x) = G (x)$
24	22 23	breqan12d	$⊢ (f = F \land g = G) \to (f (x) \leq_{R (x)} g (x) \leftrightarrow F (x) \leq_{R (x)} G (x))$
25	24	ralbidv	$⊢ (f = F \land g = G) \to (\forall x \in I f (x) \leq_{R (x)} g (x) \leftrightarrow \forall x \in I F (x) \leq_{R (x)} G (x))$
26	25	opelopab2a	$⊢ (F \in B \land G \in B) \to (⟨F, G⟩ \in \{⟨f, g⟩ \| ((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{R (x)} g (x))\} \leftrightarrow \forall x \in I F (x) \leq_{R (x)} G (x))$
27	6 7 26	syl2anc	$⊢ φ \to (⟨F, G⟩ \in \{⟨f, g⟩ \| ((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{R (x)} g (x))\} \leftrightarrow \forall x \in I F (x) \leq_{R (x)} G (x))$
28	21 27	bitrd	$⊢ φ \to (F \underset{˙}{\leq} G \leftrightarrow \forall x \in I F (x) \leq_{R (x)} G (x))$

Metamath Proof Explorer

Theorem prdsleval

Proof