# 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 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to \left({x}{R}{y}\to \left({x}{R}{z}\vee {z}{R}{y}\right)\right)$
Assertion swopolem ${⊢}\left({\phi }\wedge \left({X}\in {A}\wedge {Y}\in {A}\wedge {Z}\in {A}\right)\right)\to \left({X}{R}{Y}\to \left({X}{R}{Z}\vee {Z}{R}{Y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 swopolem.1 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to \left({x}{R}{y}\to \left({x}{R}{z}\vee {z}{R}{y}\right)\right)$
2 1 ralrimivvva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}\to \left({x}{R}{z}\vee {z}{R}{y}\right)\right)$
3 breq1 ${⊢}{x}={X}\to \left({x}{R}{y}↔{X}{R}{y}\right)$
4 breq1 ${⊢}{x}={X}\to \left({x}{R}{z}↔{X}{R}{z}\right)$
5 4 orbi1d ${⊢}{x}={X}\to \left(\left({x}{R}{z}\vee {z}{R}{y}\right)↔\left({X}{R}{z}\vee {z}{R}{y}\right)\right)$
6 3 5 imbi12d ${⊢}{x}={X}\to \left(\left({x}{R}{y}\to \left({x}{R}{z}\vee {z}{R}{y}\right)\right)↔\left({X}{R}{y}\to \left({X}{R}{z}\vee {z}{R}{y}\right)\right)\right)$
7 breq2 ${⊢}{y}={Y}\to \left({X}{R}{y}↔{X}{R}{Y}\right)$
8 breq2 ${⊢}{y}={Y}\to \left({z}{R}{y}↔{z}{R}{Y}\right)$
9 8 orbi2d ${⊢}{y}={Y}\to \left(\left({X}{R}{z}\vee {z}{R}{y}\right)↔\left({X}{R}{z}\vee {z}{R}{Y}\right)\right)$
10 7 9 imbi12d ${⊢}{y}={Y}\to \left(\left({X}{R}{y}\to \left({X}{R}{z}\vee {z}{R}{y}\right)\right)↔\left({X}{R}{Y}\to \left({X}{R}{z}\vee {z}{R}{Y}\right)\right)\right)$
11 breq2 ${⊢}{z}={Z}\to \left({X}{R}{z}↔{X}{R}{Z}\right)$
12 breq1 ${⊢}{z}={Z}\to \left({z}{R}{Y}↔{Z}{R}{Y}\right)$
13 11 12 orbi12d ${⊢}{z}={Z}\to \left(\left({X}{R}{z}\vee {z}{R}{Y}\right)↔\left({X}{R}{Z}\vee {Z}{R}{Y}\right)\right)$
14 13 imbi2d ${⊢}{z}={Z}\to \left(\left({X}{R}{Y}\to \left({X}{R}{z}\vee {z}{R}{Y}\right)\right)↔\left({X}{R}{Y}\to \left({X}{R}{Z}\vee {Z}{R}{Y}\right)\right)\right)$
15 6 10 14 rspc3v ${⊢}\left({X}\in {A}\wedge {Y}\in {A}\wedge {Z}\in {A}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}\to \left({x}{R}{z}\vee {z}{R}{y}\right)\right)\to \left({X}{R}{Y}\to \left({X}{R}{Z}\vee {Z}{R}{Y}\right)\right)\right)$
16 2 15 mpan9 ${⊢}\left({\phi }\wedge \left({X}\in {A}\wedge {Y}\in {A}\wedge {Z}\in {A}\right)\right)\to \left({X}{R}{Y}\to \left({X}{R}{Z}\vee {Z}{R}{Y}\right)\right)$