# 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
`|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x R y -> ( x R z \/ z R y ) ) )`
Assertion swopolem
`|- ( ( ph /\ ( X e. A /\ Y e. A /\ Z e. A ) ) -> ( X R Y -> ( X R Z \/ Z R Y ) ) )`

### Proof

Step Hyp Ref Expression
1 swopolem.1
` |-  ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x R y -> ( x R z \/ z R y ) ) )`
2 1 ralrimivvva
` |-  ( ph -> A. x e. A A. y e. A A. z e. 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 e. A /\ Y e. A /\ Z e. A ) -> ( A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) ) -> ( X R Y -> ( X R Z \/ Z R Y ) ) ) )`
16 2 15 mpan9
` |-  ( ( ph /\ ( X e. A /\ Y e. A /\ Z e. A ) ) -> ( X R Y -> ( X R Z \/ Z R Y ) ) )`