Theorem frrlem16

Description: Lemma for general well-founded recursion. Establish a subset relationship. (Contributed by Scott Fenton, 11-Sep-2023)

	Ref	Expression
Assertion	frrlem16	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑤 ∈ TrPred ( 𝑅 , 𝐴 , 𝑧 ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		simplr	⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) → 𝑧 ∈ 𝐴 )
2		simpllr	⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) → 𝑅 Se 𝐴 )
3	1 2	jca	⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) → ( 𝑧 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) )
4		simpr	⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) → 𝑤 ∈ TrPred ( 𝑅 , 𝐴 , 𝑧 ) )
5		trpredtr	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑤 ∈ TrPred ( 𝑅 , 𝐴 , 𝑧 ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) )
6	3 4 5	sylc	⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) )
7	6	ralrimiva	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑤 ∈ TrPred ( 𝑅 , 𝐴 , 𝑧 ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) )