pwsle

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

	Ref	Expression
Hypotheses	pwsle.y	$⊢ Y = R ↑_{𝑠} I$
	pwsle.v	$⊢ B = {Base}_{Y}$
	pwsle.o	$⊢ O = \leq_{R}$
	pwsle.l	$⊢ \underset{˙}{\leq} = \leq_{Y}$
Assertion	pwsle	$⊢ (R \in V \land I \in W) \to \underset{˙}{\leq} = \circ_{r} O \cap (B \times B)$

Proof

Step	Hyp	Ref	Expression
1		pwsle.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsle.v	$⊢ B = {Base}_{Y}$
3		pwsle.o	$⊢ O = \leq_{R}$
4		pwsle.l	$⊢ \underset{˙}{\leq} = \leq_{Y}$
5		vex	$⊢ f \in V$
6		vex	$⊢ g \in V$
7	5 6	prss	$⊢ (f \in B \land g \in B) \leftrightarrow \{f, g\} \subseteq B$
8		eqid	$⊢ Scalar (R) = Scalar (R)$
9	1 8	pwsval	$⊢ (R \in V \land I \in W) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
10	9	fveq2d	$⊢ (R \in V \land I \in W) \to {Base}_{Y} = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
11	2 10	eqtrid	$⊢ (R \in V \land I \in W) \to B = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
12	11	sseq2d	$⊢ (R \in V \land I \in W) \to (\{f, g\} \subseteq B \leftrightarrow \{f, g\} \subseteq {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))})$
13	7 12	syl5bb	$⊢ (R \in V \land I \in W) \to ((f \in B \land g \in B) \leftrightarrow \{f, g\} \subseteq {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))})$
14	13	anbi1d	$⊢ (R \in V \land I \in W) \to (((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{(I \times \{R\}) (x)} g (x)) \leftrightarrow (\{f, g\} \subseteq {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} \land \forall x \in I f (x) \leq_{(I \times \{R\}) (x)} g (x)))$
15		fvconst2g	$⊢ (R \in V \land x \in I) \to (I \times \{R\}) (x) = R$
16	15	ad4ant14	$⊢ (((R \in V \land I \in W) \land (f \in B \land g \in B)) \land x \in I) \to (I \times \{R\}) (x) = R$
17	16	fveq2d	$⊢ (((R \in V \land I \in W) \land (f \in B \land g \in B)) \land x \in I) \to \leq_{(I \times \{R\}) (x)} = \leq_{R}$
18	17 3	eqtr4di	$⊢ (((R \in V \land I \in W) \land (f \in B \land g \in B)) \land x \in I) \to \leq_{(I \times \{R\}) (x)} = O$
19	18	breqd	$⊢ (((R \in V \land I \in W) \land (f \in B \land g \in B)) \land x \in I) \to (f (x) \leq_{(I \times \{R\}) (x)} g (x) \leftrightarrow f (x) O g (x))$
20	19	ralbidva	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to (\forall x \in I f (x) \leq_{(I \times \{R\}) (x)} g (x) \leftrightarrow \forall x \in I f (x) O g (x))$
21		eqid	$⊢ {Base}_{R} = {Base}_{R}$
22		simpll	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to R \in V$
23		simplr	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to I \in W$
24		simprl	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to f \in B$
25	1 21 2 22 23 24	pwselbas	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to f : I ⟶ {Base}_{R}$
26	25	ffnd	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to f Fn I$
27		simprr	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to g \in B$
28	1 21 2 22 23 27	pwselbas	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to g : I ⟶ {Base}_{R}$
29	28	ffnd	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to g Fn I$
30		inidm	$⊢ I \cap I = I$
31		eqidd	$⊢ (((R \in V \land I \in W) \land (f \in B \land g \in B)) \land x \in I) \to f (x) = f (x)$
32		eqidd	$⊢ (((R \in V \land I \in W) \land (f \in B \land g \in B)) \land x \in I) \to g (x) = g (x)$
33	26 29 24 27 30 31 32	ofrfvalg	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to (f O_{f} g \leftrightarrow \forall x \in I f (x) O g (x))$
34	20 33	bitr4d	$⊢ ((R \in V \land I \in W) \land (f \in B \land g \in B)) \to (\forall x \in I f (x) \leq_{(I \times \{R\}) (x)} g (x) \leftrightarrow f O_{f} g)$
35	34	pm5.32da	$⊢ (R \in V \land I \in W) \to (((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{(I \times \{R\}) (x)} g (x)) \leftrightarrow ((f \in B \land g \in B) \land f O_{f} g))$
36		brinxp2	$⊢ f (\circ_{r} O \cap (B \times B)) g \leftrightarrow ((f \in B \land g \in B) \land f O_{f} g)$
37	35 36	bitr4di	$⊢ (R \in V \land I \in W) \to (((f \in B \land g \in B) \land \forall x \in I f (x) \leq_{(I \times \{R\}) (x)} g (x)) \leftrightarrow f (\circ_{r} O \cap (B \times B)) g)$
38	14 37	bitr3d	$⊢ (R \in V \land I \in W) \to ((\{f, g\} \subseteq {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} \land \forall x \in I f (x) \leq_{(I \times \{R\}) (x)} g (x)) \leftrightarrow f (\circ_{r} O \cap (B \times B)) g)$
39	38	opabbidv	$⊢ (R \in V \land I \in W) \to \{⟨f, g⟩ \| (\{f, g\} \subseteq {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} \land \forall x \in I f (x) \leq_{(I \times \{R\}) (x)} g (x))\} = \{⟨f, g⟩ \| f (\circ_{r} O \cap (B \times B)) g\}$
40	9	fveq2d	$⊢ (R \in V \land I \in W) \to \leq_{Y} = \leq_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
41	4 40	eqtrid	$⊢ (R \in V \land I \in W) \to \underset{˙}{\leq} = \leq_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
42		eqid	$⊢ Scalar (R) ⨉_{𝑠} (I \times \{R\}) = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
43		fvexd	$⊢ (R \in V \land I \in W) \to Scalar (R) \in V$
44		simpr	$⊢ (R \in V \land I \in W) \to I \in W$
45		snex	$⊢ \{R\} \in V$
46		xpexg	$⊢ (I \in W \land \{R\} \in V) \to I \times \{R\} \in V$
47	44 45 46	sylancl	$⊢ (R \in V \land I \in W) \to I \times \{R\} \in V$
48		eqid	$⊢ {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
49		snnzg	$⊢ R \in V \to \{R\} \neq \emptyset$
50	49	adantr	$⊢ (R \in V \land I \in W) \to \{R\} \neq \emptyset$
51		dmxp	$⊢ \{R\} \neq \emptyset \to dom (I \times \{R\}) = I$
52	50 51	syl	$⊢ (R \in V \land I \in W) \to dom (I \times \{R\}) = I$
53		eqid	$⊢ \leq_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} = \leq_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
54	42 43 47 48 52 53	prdsle	$⊢ (R \in V \land I \in W) \to \leq_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} = \{⟨f, g⟩ \| (\{f, g\} \subseteq {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} \land \forall x \in I f (x) \leq_{(I \times \{R\}) (x)} g (x))\}$
55	41 54	eqtrd	$⊢ (R \in V \land I \in W) \to \underset{˙}{\leq} = \{⟨f, g⟩ \| (\{f, g\} \subseteq {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} \land \forall x \in I f (x) \leq_{(I \times \{R\}) (x)} g (x))\}$
56		relinxp	$⊢ Rel (\circ_{r} O \cap (B \times B))$
57	56	a1i	$⊢ (R \in V \land I \in W) \to Rel (\circ_{r} O \cap (B \times B))$
58		dfrel4v	$⊢ Rel (\circ_{r} O \cap (B \times B)) \leftrightarrow \circ_{r} O \cap (B \times B) = \{⟨f, g⟩ \| f (\circ_{r} O \cap (B \times B)) g\}$
59	57 58	sylib	$⊢ (R \in V \land I \in W) \to \circ_{r} O \cap (B \times B) = \{⟨f, g⟩ \| f (\circ_{r} O \cap (B \times B)) g\}$
60	39 55 59	3eqtr4d	$⊢ (R \in V \land I \in W) \to \underset{˙}{\leq} = \circ_{r} O \cap (B \times B)$

Metamath Proof Explorer

Theorem pwsle

Proof