Theorem trpredpo

Description: If R partially orders A , then the transitive predecessors are the same as the immediate predecessors . (Contributed by Scott Fenton, 28-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Assertion	trpredpo	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		simp2	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑋 ∈ 𝐴 )
2		simp3	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Se 𝐴 )
3		predpo	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
4	3	ralrimiv	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
5	4	3adant3	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
6		ssidd	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
7		trpredmintr	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
8	1 2 5 6 7	syl22anc	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
9		setlikespec	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )
10		trpredpred	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
11	9 10	syl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
12	11	3adant1	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
13	8 12	eqssd	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )