Metamath Proof Explorer

Theorem pocl

Description: Characteristic properties of a partial order in class notation. (Contributed by NM, 27-Mar-1997) Reduce axiom usage and shorten proof. (Revised by GG, 3-Oct-2024)

Ref Expression
Assertion pocl ⊢ R Po A → B ∈ A ∧ C ∈ A ∧ D ∈ A → ¬ B R B ∧ B R C ∧ C R D → B R D

Proof

Step Hyp Ref Expression
1 df-po ⊢ R Po A ↔ ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z
2 1 biimpi ⊢ R Po A → ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z
3 id ⊢ x = B → x = B
4 3 3 breq12d ⊢ x = B → x R x ↔ B R B
5 4 notbid ⊢ x = B → ¬ x R x ↔ ¬ B R B
6 breq1 ⊢ x = B → x R y ↔ B R y
7 6 anbi1d ⊢ x = B → x R y ∧ y R z ↔ B R y ∧ y R z
8 breq1 ⊢ x = B → x R z ↔ B R z
9 7 8 imbi12d ⊢ x = B → x R y ∧ y R z → x R z ↔ B R y ∧ y R z → B R z
10 5 9 anbi12d ⊢ x = B → ¬ x R x ∧ x R y ∧ y R z → x R z ↔ ¬ B R B ∧ B R y ∧ y R z → B R z
11 breq2 ⊢ y = C → B R y ↔ B R C
12 breq1 ⊢ y = C → y R z ↔ C R z
13 11 12 anbi12d ⊢ y = C → B R y ∧ y R z ↔ B R C ∧ C R z
14 13 imbi1d ⊢ y = C → B R y ∧ y R z → B R z ↔ B R C ∧ C R z → B R z
15 14 anbi2d ⊢ y = C → ¬ B R B ∧ B R y ∧ y R z → B R z ↔ ¬ B R B ∧ B R C ∧ C R z → B R z
16 breq2 ⊢ z = D → C R z ↔ C R D
17 16 anbi2d ⊢ z = D → B R C ∧ C R z ↔ B R C ∧ C R D
18 breq2 ⊢ z = D → B R z ↔ B R D
19 17 18 imbi12d ⊢ z = D → B R C ∧ C R z → B R z ↔ B R C ∧ C R D → B R D
20 19 anbi2d ⊢ z = D → ¬ B R B ∧ B R C ∧ C R z → B R z ↔ ¬ B R B ∧ B R C ∧ C R D → B R D
21 10 15 20 rspc3v ⊢ B ∈ A ∧ C ∈ A ∧ D ∈ A → ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z → ¬ B R B ∧ B R C ∧ C R D → B R D
22 2 21 syl5com ⊢ R Po A → B ∈ A ∧ C ∈ A ∧ D ∈ A → ¬ B R B ∧ B R C ∧ C R D → B R D