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 ( 𝑅 , 𝐴 , 𝑋 ) ) )