pwsleval

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}$
	pwsleval.r	$⊢ φ \to R \in V$
	pwsleval.i	$⊢ φ \to I \in W$
	pwsleval.a	$⊢ φ \to F \in B$
	pwsleval.b	$⊢ φ \to G \in B$
Assertion	pwsleval	$⊢ φ \to (F \underset{˙}{\leq} G \leftrightarrow \forall x \in I F (x) O G (x))$

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		pwsleval.r	$⊢ φ \to R \in V$
6		pwsleval.i	$⊢ φ \to I \in W$
7		pwsleval.a	$⊢ φ \to F \in B$
8		pwsleval.b	$⊢ φ \to G \in B$
9	1 2 3 4	pwsle	$⊢ (R \in V \land I \in W) \to \underset{˙}{\leq} = \circ_{r} O \cap (B \times B)$
10	5 6 9	syl2anc	$⊢ φ \to \underset{˙}{\leq} = \circ_{r} O \cap (B \times B)$
11	10	breqd	$⊢ φ \to (F \underset{˙}{\leq} G \leftrightarrow F (\circ_{r} O \cap (B \times B)) G)$
12		brinxp	$⊢ (F \in B \land G \in B) \to (F O_{f} G \leftrightarrow F (\circ_{r} O \cap (B \times B)) G)$
13	7 8 12	syl2anc	$⊢ φ \to (F O_{f} G \leftrightarrow F (\circ_{r} O \cap (B \times B)) G)$
14		eqid	$⊢ {Base}_{R} = {Base}_{R}$
15	1 14 2 5 6 7	pwselbas	$⊢ φ \to F : I ⟶ {Base}_{R}$
16	15	ffnd	$⊢ φ \to F Fn I$
17	1 14 2 5 6 8	pwselbas	$⊢ φ \to G : I ⟶ {Base}_{R}$
18	17	ffnd	$⊢ φ \to G Fn I$
19		inidm	$⊢ I \cap I = I$
20		eqidd	$⊢ (φ \land x \in I) \to F (x) = F (x)$
21		eqidd	$⊢ (φ \land x \in I) \to G (x) = G (x)$
22	16 18 7 8 19 20 21	ofrfvalg	$⊢ φ \to (F O_{f} G \leftrightarrow \forall x \in I F (x) O G (x))$
23	11 13 22	3bitr2d	$⊢ φ \to (F \underset{˙}{\leq} G \leftrightarrow \forall x \in I F (x) O G (x))$

Metamath Proof Explorer