Theorem trpredelss

Description: Given a transitive predecessor Y of X , the transitive predecessors of Y form a subclass of the transitive predecessors of X . (Contributed by Scott Fenton, 25-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Assertion	trpredelss	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) → TrPred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		setlikespec	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )
2		trpredss	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → TrPred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴 )
3	1 2	syl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴 )
4	3	sselda	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) → 𝑌 ∈ 𝐴 )
5		simplr	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) → 𝑅 Se 𝐴 )
6		trpredtr	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑦 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) )
7	6	ralrimiv	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
8	7	adantr	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) → ∀ 𝑦 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
9		trpredtr	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) )
10	9	imp	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
11		trpredmintr	⊢ ( ( ( 𝑌 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ∧ Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) ) → TrPred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
12	4 5 8 10 11	syl22anc	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) → TrPred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
13	12	ex	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) → TrPred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) )