Metamath Proof Explorer

Theorem prdsless

Description: Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015)

Ref Expression
Hypotheses prdsbas.p ⊢ P = S ⨉ 𝑠 R
prdsbas.s ⊢ φ → S ∈ V
prdsbas.r ⊢ φ → R ∈ W
prdsbas.b ⊢ B = Base P
prdsbas.i ⊢ φ → dom ⁡ R = I
prdsle.l ⊢ ≤ ˙ = ≤ P
Assertion prdsless ⊢ φ → ≤ ˙ ⊆ B × B

Proof

Step Hyp Ref Expression
1 prdsbas.p ⊢ P = S ⨉ 𝑠 R
2 prdsbas.s ⊢ φ → S ∈ V
3 prdsbas.r ⊢ φ → R ∈ W
4 prdsbas.b ⊢ B = Base P
5 prdsbas.i ⊢ φ → dom ⁡ R = I
6 prdsle.l ⊢ ≤ ˙ = ≤ P
7 1 2 3 4 5 6 prdsle ⊢ φ → ≤ ˙ = f g | f g ⊆ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x
8 vex ⊢ f ∈ V
9 vex ⊢ g ∈ V
10 8 9 prss ⊢ f ∈ B ∧ g ∈ B ↔ f g ⊆ B
11 10 anbi1i ⊢ f ∈ B ∧ g ∈ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x ↔ f g ⊆ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x
12 11 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
13 opabssxp ⊢ f g | f ∈ B ∧ g ∈ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x ⊆ B × B
14 12 13 eqsstrri ⊢ f g | f g ⊆ B ∧ ∀ x ∈ I f ⁡ x ≤ R ⁡ x g ⁡ x ⊆ B × B
15 7 14 eqsstrdi ⊢ φ → ≤ ˙ ⊆ B × B