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 φxAyAzAxRyxRzzRy
Assertion swopolem φXAYAZAXRYXRZZRY

Proof

Step Hyp Ref Expression
1 swopolem.1 φxAyAzAxRyxRzzRy
2 1 ralrimivvva φxAyAzAxRyxRzzRy
3 breq1 x=XxRyXRy
4 breq1 x=XxRzXRz
5 4 orbi1d x=XxRzzRyXRzzRy
6 3 5 imbi12d x=XxRyxRzzRyXRyXRzzRy
7 breq2 y=YXRyXRY
8 breq2 y=YzRyzRY
9 8 orbi2d y=YXRzzRyXRzzRY
10 7 9 imbi12d y=YXRyXRzzRyXRYXRzzRY
11 breq2 z=ZXRzXRZ
12 breq1 z=ZzRYZRY
13 11 12 orbi12d z=ZXRzzRYXRZZRY
14 13 imbi2d z=ZXRYXRzzRYXRYXRZZRY
15 6 10 14 rspc3v XAYAZAxAyAzAxRyxRzzRyXRYXRZZRY
16 2 15 mpan9 φXAYAZAXRYXRZZRY