Theorem pwsleval

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

	Ref	Expression
Hypotheses	pwsle.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
	pwsle.v	⊢ 𝐵 = ( Base ‘ 𝑌 )
	pwsle.o	⊢ 𝑂 = ( le ‘ 𝑅 )
	pwsle.l	⊢ ≤ = ( le ‘ 𝑌 )
	pwsleval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	pwsleval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	pwsleval.a	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	pwsleval.b	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion	pwsleval	⊢ ( 𝜑 → ( 𝐹 ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐺 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pwsle.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2		pwsle.v	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		pwsle.o	⊢ 𝑂 = ( le ‘ 𝑅 )
4		pwsle.l	⊢ ≤ = ( le ‘ 𝑌 )
5		pwsleval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
6		pwsleval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7		pwsleval.a	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8		pwsleval.b	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
9	1 2 3 4	pwsle	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ≤ = ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) )
10	5 6 9	syl2anc	⊢ ( 𝜑 → ≤ = ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) )
11	10	breqd	⊢ ( 𝜑 → ( 𝐹 ≤ 𝐺 ↔ 𝐹 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝐺 ) )
12		brinxp	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∘r 𝑂 𝐺 ↔ 𝐹 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝐺 ) )
13	7 8 12	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘r 𝑂 𝐺 ↔ 𝐹 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝐺 ) )
14		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15	1 14 2 5 6 7	pwselbas	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
16	15	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐼 )
17	1 14 2 5 6 8	pwselbas	⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
18	17	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐼 )
19		inidm	⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
20		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
21		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
22	16 18 7 8 19 20 21	ofrfvalg	⊢ ( 𝜑 → ( 𝐹 ∘r 𝑂 𝐺 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐺 ‘ 𝑥 ) ) )
23	11 13 22	3bitr2d	⊢ ( 𝜑 → ( 𝐹 ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐺 ‘ 𝑥 ) ) )