This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swopolem

Description: Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014)

Ref Expression
Hypothesis swopolem.1 ⊢ φ ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A → x R y → x R z ∨ z R y
Assertion swopolem ⊢ φ ∧ X ∈ A ∧ Y ∈ A ∧ Z ∈ A → X R Y → X R Z ∨ Z R Y

Proof

Step Hyp Ref Expression
1 swopolem.1 ⊢ φ ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A → x R y → x R z ∨ z R y
2 1 ralrimivvva ⊢ φ → ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A x R y → x R z ∨ z R y
3 breq1 ⊢ x = X → x R y ↔ X R y
4 breq1 ⊢ x = X → x R z ↔ X R z
5 4 orbi1d ⊢ x = X → x R z ∨ z R y ↔ X R z ∨ z R y
6 3 5 imbi12d ⊢ x = X → x R y → x R z ∨ z R y ↔ X R y → X R z ∨ z R y
7 breq2 ⊢ y = Y → X R y ↔ X R Y
8 breq2 ⊢ y = Y → z R y ↔ z R Y
9 8 orbi2d ⊢ y = Y → X R z ∨ z R y ↔ X R z ∨ z R Y
10 7 9 imbi12d ⊢ y = Y → X R y → X R z ∨ z R y ↔ X R Y → X R z ∨ z R Y
11 breq2 ⊢ z = Z → X R z ↔ X R Z
12 breq1 ⊢ z = Z → z R Y ↔ Z R Y
13 11 12 orbi12d ⊢ z = Z → X R z ∨ z R Y ↔ X R Z ∨ Z R Y
14 13 imbi2d ⊢ z = Z → X R Y → X R z ∨ z R Y ↔ X R Y → X R Z ∨ Z R Y
15 6 10 14 rspc3v ⊢ X ∈ A ∧ Y ∈ A ∧ Z ∈ A → ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A x R y → x R z ∨ z R y → X R Y → X R Z ∨ Z R Y
16 2 15 mpan9 ⊢ φ ∧ X ∈ A ∧ Y ∈ A ∧ Z ∈ A → X R Y → X R Z ∨ Z R Y