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