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 ⊢ Y = S ⨉ 𝑠 R
prdsbasmpt.b ⊢ B = Base Y
prdsbasmpt.s ⊢ φ → S ∈ V
prdsbasmpt.i ⊢ φ → I ∈ W
prdsbasmpt.r ⊢ φ → R Fn I
prdsplusgval.f ⊢ φ → F ∈ B
prdsplusgval.g ⊢ φ → G ∈ B
prdsleval.l ⊢ ≤ ˙ = ≤ Y
Assertion prdsleval ⊢ φ → F ≤ ˙ G ↔ ∀ x ∈ I F ⁡ x ≤ R ⁡ x G ⁡ x

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y ⊢ Y = S ⨉ 𝑠 R
2 prdsbasmpt.b ⊢ B = Base Y
3 prdsbasmpt.s ⊢ φ → S ∈ V
4 prdsbasmpt.i ⊢ φ → I ∈ W
5 prdsbasmpt.r ⊢ φ → R Fn I
6 prdsplusgval.f ⊢ φ → F ∈ B
7 prdsplusgval.g ⊢ φ → G ∈ B
8 prdsleval.l ⊢ ≤ ˙ = ≤ Y
9 df-br ⊢ F ≤ ˙ G ↔ F G ∈ ≤ ˙
10 fnex ⊢ R Fn I ∧ I ∈ W → R ∈ V
11 5 4 10 syl2anc ⊢ φ → R ∈ V
12 5 fndmd ⊢ φ → dom ⁡ R = I
13 1 3 11 2 12 8 prdsle ⊢ φ → ≤ ˙ = f g | f g ⊆ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x
14 vex ⊢ f ∈ V
15 vex ⊢ g ∈ V
16 14 15 prss ⊢ f ∈ B ∧ g ∈ B ↔ f g ⊆ B
17 16 anbi1i ⊢ f ∈ B ∧ g ∈ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x ↔ f g ⊆ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x
18 17 opabbii ⊢ f g | f ∈ B ∧ g ∈ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x = f g | f g ⊆ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x
19 13 18 eqtr4di ⊢ φ → ≤ ˙ = f g | f ∈ B ∧ g ∈ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x
20 19 eleq2d ⊢ φ → F G ∈ ≤ ˙ ↔ F G ∈ f g | f ∈ B ∧ g ∈ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x
21 9 20 syl5bb ⊢ φ → F ≤ ˙ G ↔ F G ∈ f g | f ∈ B ∧ g ∈ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x
22 fveq1 ⊢ f = F → f ⁡ x = F ⁡ x
23 fveq1 ⊢ g = G → g ⁡ x = G ⁡ x
24 22 23 breqan12d ⊢ f = F ∧ g = G → f ⁡ x ≤ R ⁡ x g ⁡ x ↔ F ⁡ x ≤ R ⁡ x G ⁡ x
25 24 ralbidv ⊢ f = F ∧ g = G → ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x ↔ ∀ x ∈ I F ⁡ x ≤ R ⁡ x G ⁡ x
26 25 opelopab2a ⊢ F ∈ B ∧ G ∈ B → F G ∈ f g | f ∈ B ∧ g ∈ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x ↔ ∀ x ∈ I F ⁡ x ≤ R ⁡ x G ⁡ x
27 6 7 26 syl2anc ⊢ φ → F G ∈ f g | f ∈ B ∧ g ∈ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x ↔ ∀ x ∈ I F ⁡ x ≤ R ⁡ x G ⁡ x
28 21 27 bitrd ⊢ φ → F ≤ ˙ G ↔ ∀ x ∈ I F ⁡ x ≤ R ⁡ x G ⁡ x