Theorem pwsleval

Description: Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015)

	Ref	Expression
Hypotheses	pwsle.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
	pwsle.v	$$⊢B={\mathrm{Base}}_Y$$
	pwsle.o	$$⊢O={\le }_R$$
	pwsle.l	$$⊢\underset{\dot{}}{\le }={\le }_Y$$
	pwsleval.r	$$⊢\phi \to R\in V$$
	pwsleval.i	$$⊢\phi \to I\in W$$
	pwsleval.a	$$⊢\phi \to F\in B$$
	pwsleval.b	$$⊢\phi \to G\in B$$
Assertion	pwsleval	$$⊢\phi \to \left(F\underset{\dot{}}{\le }G\leftrightarrow \forall x\in IF\left(x\right)OG\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwsle.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
2		pwsle.v	$$⊢B={\mathrm{Base}}_Y$$
3		pwsle.o	$$⊢O={\le }_R$$
4		pwsle.l	$$⊢\underset{\dot{}}{\le }={\le }_Y$$
5		pwsleval.r	$$⊢\phi \to R\in V$$
6		pwsleval.i	$$⊢\phi \to I\in W$$
7		pwsleval.a	$$⊢\phi \to F\in B$$
8		pwsleval.b	$$⊢\phi \to G\in B$$
9	1 2 3 4	pwsle	$$⊢\left(R\in V\wedge I\in W\right)\to \underset{\dot{}}{\le }={\circ }_{r}O\cap \left(B\times B\right)$$
10	5 6 9	syl2anc	$$⊢\phi \to \underset{\dot{}}{\le }={\circ }_{r}O\cap \left(B\times B\right)$$
11	10	breqd	$$⊢\phi \to \left(F\underset{\dot{}}{\le }G\leftrightarrow F\left({\circ }_{r}O\cap \left(B\times B\right)\right)G\right)$$
12		brinxp	$$⊢\left(F\in B\wedge G\in B\right)\to \left(F{O}_{f}G\leftrightarrow F\left({\circ }_{r}O\cap \left(B\times B\right)\right)G\right)$$
13	7 8 12	syl2anc	$$⊢\phi \to \left(F{O}_{f}G\leftrightarrow F\left({\circ }_{r}O\cap \left(B\times B\right)\right)G\right)$$
14		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
15	1 14 2 5 6 7	pwselbas	$$⊢\phi \to F:I⟶{\mathrm{Base}}_R$$
16	15	ffnd	$$⊢\phi \to FFnI$$
17	1 14 2 5 6 8	pwselbas	$$⊢\phi \to G:I⟶{\mathrm{Base}}_R$$
18	17	ffnd	$$⊢\phi \to GFnI$$
19		inidm	$$⊢I\cap I=I$$
20		eqidd	$$⊢\left(\phi \wedge x\in I\right)\to F\left(x\right)=F\left(x\right)$$
21		eqidd	$$⊢\left(\phi \wedge x\in I\right)\to G\left(x\right)=G\left(x\right)$$
22	16 18 7 8 19 20 21	ofrfvalg	$$⊢\phi \to \left(F{O}_{f}G\leftrightarrow \forall x\in IF\left(x\right)OG\left(x\right)\right)$$
23	11 13 22	3bitr2d	$$⊢\phi \to \left(F\underset{\dot{}}{\le }G\leftrightarrow \forall x\in IF\left(x\right)OG\left(x\right)\right)$$