Metamath Proof Explorer

Theorem frrlem16

Description: Lemma for general well-founded recursion. Establish a subset relation. (Contributed by Scott Fenton, 11-Sep-2023) Revised notion of transitive closure. (Revised by Scott Fenton, 1-Dec-2024)

Ref Expression
Assertion frrlem16 ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑤 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) )

Proof

Step Hyp Ref Expression
1 predres ⊢ Pred ( 𝑅 , 𝐴 , 𝑤 ) = Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑤 )
2 relres ⊢ Rel ( 𝑅 ↾ 𝐴 )
3 ssttrcl ⊢ ( Rel ( 𝑅 ↾ 𝐴 ) → ( 𝑅 ↾ 𝐴 ) ⊆ t++ ( 𝑅 ↾ 𝐴 ) )
4 2 3 ax-mp ⊢ ( 𝑅 ↾ 𝐴 ) ⊆ t++ ( 𝑅 ↾ 𝐴 )
5 predrelss ⊢ ( ( 𝑅 ↾ 𝐴 ) ⊆ t++ ( 𝑅 ↾ 𝐴 ) → Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑤 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑤 ) )
6 4 5 ax-mp ⊢ Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑤 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑤 )
7 1 6 eqsstri ⊢ Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑤 )
8 inss1 ⊢ ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ⊆ t++ ( 𝑅 ↾ 𝐴 )
9 coss1 ⊢ ( ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ⊆ t++ ( 𝑅 ↾ 𝐴 ) → ( ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ∘ ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( t++ ( 𝑅 ↾ 𝐴 ) ∘ ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ) )
10 8 9 ax-mp ⊢ ( ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ∘ ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( t++ ( 𝑅 ↾ 𝐴 ) ∘ ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) )
11 coss2 ⊢ ( ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ⊆ t++ ( 𝑅 ↾ 𝐴 ) → ( t++ ( 𝑅 ↾ 𝐴 ) ∘ ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( t++ ( 𝑅 ↾ 𝐴 ) ∘ t++ ( 𝑅 ↾ 𝐴 ) ) )
12 8 11 ax-mp ⊢ ( t++ ( 𝑅 ↾ 𝐴 ) ∘ ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( t++ ( 𝑅 ↾ 𝐴 ) ∘ t++ ( 𝑅 ↾ 𝐴 ) )
13 10 12 sstri ⊢ ( ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ∘ ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( t++ ( 𝑅 ↾ 𝐴 ) ∘ t++ ( 𝑅 ↾ 𝐴 ) )
14 ttrcltr ⊢ ( t++ ( 𝑅 ↾ 𝐴 ) ∘ t++ ( 𝑅 ↾ 𝐴 ) ) ⊆ t++ ( 𝑅 ↾ 𝐴 )
15 13 14 sstri ⊢ ( ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ∘ ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ t++ ( 𝑅 ↾ 𝐴 )
16 predtrss ⊢ ( ( ( ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ∘ ( t++ ( 𝑅 ↾ 𝐴 ) ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ t++ ( 𝑅 ↾ 𝐴 ) ∧ 𝑤 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ∧ 𝑧 ∈ 𝐴 ) → Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑤 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) )
17 15 16 mp3an1 ⊢ ( ( 𝑤 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ∧ 𝑧 ∈ 𝐴 ) → Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑤 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) )
18 7 17 sstrid ⊢ ( ( 𝑤 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ∧ 𝑧 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) )
19 18 ancoms ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) )
20 19 ralrimiva ⊢ ( 𝑧 ∈ 𝐴 → ∀ 𝑤 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) )
21 20 adantl ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑤 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) )