This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem poeq1

Description: Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997)

Ref Expression
Assertion poeq1 ( 𝑅 = 𝑆 → ( 𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴 ) )

Proof

Step Hyp Ref Expression
1 breq ⊢ ( 𝑅 = 𝑆 → ( 𝑥 𝑅 𝑥 ↔ 𝑥 𝑆 𝑥 ) )
2 1 notbid ⊢ ( 𝑅 = 𝑆 → ( ¬ 𝑥 𝑅 𝑥 ↔ ¬ 𝑥 𝑆 𝑥 ) )
3 breq ⊢ ( 𝑅 = 𝑆 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑆 𝑦 ) )
4 breq ⊢ ( 𝑅 = 𝑆 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑆 𝑧 ) )
5 3 4 anbi12d ⊢ ( 𝑅 = 𝑆 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ↔ ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) ) )
6 breq ⊢ ( 𝑅 = 𝑆 → ( 𝑥 𝑅 𝑧 ↔ 𝑥 𝑆 𝑧 ) )
7 5 6 imbi12d ⊢ ( 𝑅 = 𝑆 → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ) )
8 2 7 anbi12d ⊢ ( 𝑅 = 𝑆 → ( ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ¬ 𝑥 𝑆 𝑥 ∧ ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ) ) )
9 8 ralbidv ⊢ ( 𝑅 = 𝑆 → ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑆 𝑥 ∧ ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ) ) )
10 9 2ralbidv ⊢ ( 𝑅 = 𝑆 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑆 𝑥 ∧ ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ) ) )
11 df-po ⊢ ( 𝑅 Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
12 df-po ⊢ ( 𝑆 Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑆 𝑥 ∧ ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ) )
13 10 11 12 3bitr4g ⊢ ( 𝑅 = 𝑆 → ( 𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴 ) )