Metamath Proof Explorer

Theorem caovordig

Description: Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014)

Ref Expression
Hypothesis caovordig.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S → x R y → z F x R z F y
Assertion caovordig ⊢ φ ∧ A ∈ S ∧ B ∈ S ∧ C ∈ S → A R B → C F A R C F B

Proof

Step Hyp Ref Expression
1 caovordig.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S → x R y → z F x R z F y
2 1 ralrimivvva ⊢ φ → ∀ x ∈ S ∀ y ∈ S ∀ z ∈ S x R y → z F x R z F y
3 breq1 ⊢ x = A → x R y ↔ A R y
4 oveq2 ⊢ x = A → z F x = z F A
5 4 breq1d ⊢ x = A → z F x R z F y ↔ z F A R z F y
6 3 5 imbi12d ⊢ x = A → x R y → z F x R z F y ↔ A R y → z F A R z F y
7 breq2 ⊢ y = B → A R y ↔ A R B
8 oveq2 ⊢ y = B → z F y = z F B
9 8 breq2d ⊢ y = B → z F A R z F y ↔ z F A R z F B
10 7 9 imbi12d ⊢ y = B → A R y → z F A R z F y ↔ A R B → z F A R z F B
11 oveq1 ⊢ z = C → z F A = C F A
12 oveq1 ⊢ z = C → z F B = C F B
13 11 12 breq12d ⊢ z = C → z F A R z F B ↔ C F A R C F B
14 13 imbi2d ⊢ z = C → A R B → z F A R z F B ↔ A R B → C F A R C F B
15 6 10 14 rspc3v ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ S → ∀ x ∈ S ∀ y ∈ S ∀ z ∈ S x R y → z F x R z F y → A R B → C F A R C F B
16 2 15 mpan9 ⊢ φ ∧ A ∈ S ∧ B ∈ S ∧ C ∈ S → A R B → C F A R C F B