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 ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) )