This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐹 ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) 𝑂 ( 𝐺 ‘ 𝑥 ) ) )