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

Metamath Proof Explorer

Theorem predpo

Description: Property of the predecessor class for partial orders. (Contributed by Scott Fenton, 28-Apr-2012) (Proof shortened by Scott Fenton, 28-Oct-2024)

Ref Expression
Assertion predpo ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 dfpo2 ⊢ ( 𝑅 Po 𝐴 ↔ ( ( 𝑅 ∩ ( I ↾ 𝐴 ) ) = ∅ ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ) )
2 1 simprbi ⊢ ( 𝑅 Po 𝐴 → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 )
3 2 ad2antrr ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 )
4 simpr ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
5 simplr ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → 𝑋 ∈ 𝐴 )
6 predtrss ⊢ ( ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ 𝑅 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑋 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
7 3 4 5 6 syl3anc ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
8 7 ex ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )