Metamath Proof Explorer

Theorem prdsleval

Description: Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypotheses prdsbasmpt.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsbasmpt.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsbasmpt.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsbasmpt.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsbasmpt.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
prdsplusgval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
prdsplusgval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
prdsleval.l ⊢ ≤ = ( le ‘ 𝑌 )
Assertion prdsleval ( 𝜑 → ( 𝐹 ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsbasmpt.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsbasmpt.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 prdsbasmpt.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 prdsbasmpt.r ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
6 prdsplusgval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7 prdsplusgval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8 prdsleval.l ⊢ ≤ = ( le ‘ 𝑌 )
9 df-br ⊢ ( 𝐹 ≤ 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ≤ )
10 fnex ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
11 5 4 10 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ V )
12 5 fndmd ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
13 1 3 11 2 12 8 prdsle ⊢ ( 𝜑 → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
14 vex ⊢ 𝑓 ∈ V
15 vex ⊢ 𝑔 ∈ V
16 14 15 prss ⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ↔ { 𝑓 , 𝑔 } ⊆ 𝐵 )
17 16 anbi1i ⊢ ( ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
18 17 opabbii ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) }
19 13 18 eqtr4di ⊢ ( 𝜑 → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
20 19 eleq2d ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ≤ ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ) )
21 9 20 syl5bb ⊢ ( 𝜑 → ( 𝐹 ≤ 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ) )
22 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
23 fveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
24 22 23 breqan12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
25 24 ralbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
26 25 opelopab2a ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
27 6 7 26 syl2anc ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
28 21 27 bitrd ⊢ ( 𝜑 → ( 𝐹 ≤ 𝐺 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )