rtrclreclem3

Description: The reflexive, transitive closure is indeed transitive. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 13-Jul-2024)

		Ref	Expression
	Hypothesis	rtrclreclem.1	⊢ ( 𝜑 → Rel 𝑅 )
	Assertion	rtrclreclem3	⊢ ( 𝜑 → ( ( trec ‘ 𝑅 ) ∘ ( trec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		rtrclreclem.1	⊢ ( 𝜑 → Rel 𝑅 )
2		df-co	⊢ ( ( trec ‘ 𝑅 ) ∘ ( trec ‘ 𝑅 ) ) = { ⟨ 𝑒 , 𝑔 ⟩ ∣ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) }
3		elopab	⊢ ( 𝑑 ∈ { ⟨ 𝑒 , 𝑔 ⟩ ∣ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) } ↔ ∃ 𝑒 ∃ 𝑔 ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ ∧ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ) )
4		eqeq1	⊢ ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ → ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ ↔ ⟨ 𝑒 , 𝑔 ⟩ = ⟨ 𝑒 , 𝑔 ⟩ ) )
5	4	anbi1d	⊢ ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ → ( ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ ∧ ( ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ∧ 𝜑 ) ) ↔ ( ⟨ 𝑒 , 𝑔 ⟩ = ⟨ 𝑒 , 𝑔 ⟩ ∧ ( ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ∧ 𝜑 ) ) ) )
6		simprr	⊢ ( ( ⟨ 𝑒 , 𝑔 ⟩ = ⟨ 𝑒 , 𝑔 ⟩ ∧ ( ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ∧ 𝜑 ) ) → 𝜑 )
7		simprl	⊢ ( ( ⟨ 𝑒 , 𝑔 ⟩ = ⟨ 𝑒 , 𝑔 ⟩ ∧ ( ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ∧ 𝜑 ) ) → ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) )
8		simpl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ) → 𝑒 ( t*rec ‘ 𝑅 ) 𝑓 )
9		simprr	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ) → 𝜑 )
10	1	dfrtrclrec2	⊢ ( 𝜑 → ( 𝑒 ( t*rec ‘ 𝑅 ) 𝑓 ↔ ∃ 𝑛 ∈ ℕ₀ 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ) )
11	9 10	syl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ) → ( 𝑒 ( t*rec ‘ 𝑅 ) 𝑓 ↔ ∃ 𝑛 ∈ ℕ₀ 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ) )
12	8 11	mpbid	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ) → ∃ 𝑛 ∈ ℕ₀ 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 )
13		simprl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ) → 𝑓 ( t*rec ‘ 𝑅 ) 𝑔 )
14		simprrl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ) → 𝜑 )
15	1	dfrtrclrec2	⊢ ( 𝜑 → ( 𝑓 ( t*rec ‘ 𝑅 ) 𝑔 ↔ ∃ 𝑚 ∈ ℕ₀ 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ) )
16	14 15	syl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ) → ( 𝑓 ( t*rec ‘ 𝑅 ) 𝑔 ↔ ∃ 𝑚 ∈ ℕ₀ 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ) )
17	13 16	mpbid	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ) → ∃ 𝑚 ∈ ℕ₀ 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 )
18		simprrl	⊢ ( ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) → 𝑛 ∈ ℕ₀ )
19	18	adantl	⊢ ( ( 𝑓 ( t*rec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) → 𝑛 ∈ ℕ₀ )
20	19	adantl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → 𝑛 ∈ ℕ₀ )
21		simprr	⊢ ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) → 𝑚 ∈ ℕ₀ )
22	21	adantl	⊢ ( ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) → 𝑚 ∈ ℕ₀ )
23	22	adantl	⊢ ( ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) → 𝑚 ∈ ℕ₀ )
24	23	adantl	⊢ ( ( 𝑓 ( t*rec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) → 𝑚 ∈ ℕ₀ )
25	24	adantl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → 𝑚 ∈ ℕ₀ )
26	20 25	nn0addcld	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → ( 𝑛 + 𝑚 ) ∈ ℕ₀ )
27	20	adantl	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → 𝑛 ∈ ℕ₀ )
28	27	nn0cnd	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → 𝑛 ∈ ℂ )
29	25	adantl	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → 𝑚 ∈ ℕ₀ )
30	29	nn0cnd	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → 𝑚 ∈ ℂ )
31	28 30	addcomd	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → ( 𝑛 + 𝑚 ) = ( 𝑚 + 𝑛 ) )
32		eleq1	⊢ ( ( 𝑛 + 𝑚 ) = ( 𝑚 + 𝑛 ) → ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ↔ ( 𝑚 + 𝑛 ) ∈ ℕ₀ ) )
33	32	anbi1d	⊢ ( ( 𝑛 + 𝑚 ) = ( 𝑚 + 𝑛 ) → ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) ↔ ( ( 𝑚 + 𝑛 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) ) )
34		simprrl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → 𝜑 )
35	34	adantl	⊢ ( ( ( 𝑚 + 𝑛 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → 𝜑 )
36	35 1	syl	⊢ ( ( ( 𝑚 + 𝑛 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → Rel 𝑅 )
37	25	adantl	⊢ ( ( ( 𝑚 + 𝑛 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → 𝑚 ∈ ℕ₀ )
38	20	adantl	⊢ ( ( ( 𝑚 + 𝑛 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → 𝑛 ∈ ℕ₀ )
39	36 37 38	relexpaddd	⊢ ( ( ( 𝑚 + 𝑛 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → ( ( 𝑅 ↑_𝑟 𝑚 ) ∘ ( 𝑅 ↑_𝑟 𝑛 ) ) = ( 𝑅 ↑_𝑟 ( 𝑚 + 𝑛 ) ) )
40		oveq2	⊢ ( ( 𝑛 + 𝑚 ) = ( 𝑚 + 𝑛 ) → ( 𝑅 ↑_𝑟 ( 𝑛 + 𝑚 ) ) = ( 𝑅 ↑_𝑟 ( 𝑚 + 𝑛 ) ) )
41	40	eqeq2d	⊢ ( ( 𝑛 + 𝑚 ) = ( 𝑚 + 𝑛 ) → ( ( ( 𝑅 ↑_𝑟 𝑚 ) ∘ ( 𝑅 ↑_𝑟 𝑛 ) ) = ( 𝑅 ↑_𝑟 ( 𝑛 + 𝑚 ) ) ↔ ( ( 𝑅 ↑_𝑟 𝑚 ) ∘ ( 𝑅 ↑_𝑟 𝑛 ) ) = ( 𝑅 ↑_𝑟 ( 𝑚 + 𝑛 ) ) ) )
42	39 41	syl5ibr	⊢ ( ( 𝑛 + 𝑚 ) = ( 𝑚 + 𝑛 ) → ( ( ( 𝑚 + 𝑛 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → ( ( 𝑅 ↑_𝑟 𝑚 ) ∘ ( 𝑅 ↑_𝑟 𝑛 ) ) = ( 𝑅 ↑_𝑟 ( 𝑛 + 𝑚 ) ) ) )
43	33 42	sylbid	⊢ ( ( 𝑛 + 𝑚 ) = ( 𝑚 + 𝑛 ) → ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → ( ( 𝑅 ↑_𝑟 𝑚 ) ∘ ( 𝑅 ↑_𝑟 𝑛 ) ) = ( 𝑅 ↑_𝑟 ( 𝑛 + 𝑚 ) ) ) )
44	31 43	mpcom	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → ( ( 𝑅 ↑_𝑟 𝑚 ) ∘ ( 𝑅 ↑_𝑟 𝑛 ) ) = ( 𝑅 ↑_𝑟 ( 𝑛 + 𝑚 ) ) )
45		simprrl	⊢ ( ( 𝑓 ( t*rec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) → 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 )
46	45	adantl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 )
47		simprrl	⊢ ( ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) → 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 )
48	47	adantl	⊢ ( ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) → 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 )
49	48	adantl	⊢ ( ( 𝑓 ( t*rec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) → 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 )
50	49	adantl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 )
51	50	adantl	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 )
52		vex	⊢ 𝑓 ∈ V
53		breq2	⊢ ( ℎ = 𝑓 → ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) ℎ ↔ 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ) )
54		breq1	⊢ ( ℎ = 𝑓 → ( ℎ ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ↔ 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ) )
55	53 54	anbi12d	⊢ ( ℎ = 𝑓 → ( ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) ℎ ∧ ℎ ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ) ↔ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ) ) )
56	52 55	spcev	⊢ ( ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ) → ∃ ℎ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) ℎ ∧ ℎ ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ) )
57	46 51 56	syl2an2	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → ∃ ℎ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) ℎ ∧ ℎ ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ) )
58		vex	⊢ 𝑒 ∈ V
59		vex	⊢ 𝑔 ∈ V
60	58 59	brco	⊢ ( 𝑒 ( ( 𝑅 ↑_𝑟 𝑚 ) ∘ ( 𝑅 ↑_𝑟 𝑛 ) ) 𝑔 ↔ ∃ ℎ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) ℎ ∧ ℎ ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ) )
61	57 60	sylibr	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → 𝑒 ( ( 𝑅 ↑_𝑟 𝑚 ) ∘ ( 𝑅 ↑_𝑟 𝑛 ) ) 𝑔 )
62	44 61	breqdi	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → 𝑒 ( 𝑅 ↑_𝑟 ( 𝑛 + 𝑚 ) ) 𝑔 )
63		oveq2	⊢ ( 𝑖 = ( 𝑛 + 𝑚 ) → ( 𝑅 ↑_𝑟 𝑖 ) = ( 𝑅 ↑_𝑟 ( 𝑛 + 𝑚 ) ) )
64	63	breqd	⊢ ( 𝑖 = ( 𝑛 + 𝑚 ) → ( 𝑒 ( 𝑅 ↑_𝑟 𝑖 ) 𝑔 ↔ 𝑒 ( 𝑅 ↑_𝑟 ( 𝑛 + 𝑚 ) ) 𝑔 ) )
65	64	rspcev	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ 𝑒 ( 𝑅 ↑_𝑟 ( 𝑛 + 𝑚 ) ) 𝑔 ) → ∃ 𝑖 ∈ ℕ₀ 𝑒 ( 𝑅 ↑_𝑟 𝑖 ) 𝑔 )
66	62 65	syldan	⊢ ( ( ( 𝑛 + 𝑚 ) ∈ ℕ₀ ∧ ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) ) → ∃ 𝑖 ∈ ℕ₀ 𝑒 ( 𝑅 ↑_𝑟 𝑖 ) 𝑔 )
67	26 66	mpancom	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → ∃ 𝑖 ∈ ℕ₀ 𝑒 ( 𝑅 ↑_𝑟 𝑖 ) 𝑔 )
68		df-br	⊢ ( 𝑒 ( trec ‘ 𝑅 ) 𝑔 ↔ ⟨ 𝑒 , 𝑔 ⟩ ∈ ( trec ‘ 𝑅 ) )
69	34 1	syl	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → Rel 𝑅 )
70	69	dfrtrclrec2	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → ( 𝑒 ( t*rec ‘ 𝑅 ) 𝑔 ↔ ∃ 𝑖 ∈ ℕ₀ 𝑒 ( 𝑅 ↑_𝑟 𝑖 ) 𝑔 ) )
71	68 70	bitr3id	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → ( ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ↔ ∃ 𝑖 ∈ ℕ₀ 𝑒 ( 𝑅 ↑_𝑟 𝑖 ) 𝑔 ) )
72	67 71	mpbird	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) )
73	72	expcom	⊢ ( ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) ) → ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
74	73	expcom	⊢ ( ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) ) → ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 → ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) ) )
75	74	expcom	⊢ ( ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ ( 𝑛 ∈ ℕ₀ ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) → ( 𝜑 → ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 → ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) ) ) )
76	75	anassrs	⊢ ( ( ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) → ( 𝜑 → ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 → ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) ) ) )
77	76	impcom	⊢ ( ( 𝜑 ∧ ( ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) → ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 → ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) ) )
78	77	anassrs	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) → ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 → ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) ) )
79	78	impcom	⊢ ( ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) → ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
80	79	anassrs	⊢ ( ( ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) → ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
81	80	impcom	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) )
82	81	anassrs	⊢ ( ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ) ∧ ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) )
83	82	expcom	⊢ ( ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
84	83	expcom	⊢ ( 𝑚 ∈ ℕ₀ → ( 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 → ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) ) )
85	84	rexlimiv	⊢ ( ∃ 𝑚 ∈ ℕ₀ 𝑓 ( 𝑅 ↑_𝑟 𝑚 ) 𝑔 → ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
86	17 85	mpcom	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) )
87	86	expcom	⊢ ( ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ ( 𝜑 ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) → ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
88	87	anassrs	⊢ ( ( ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) → ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
89	88	impcom	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) )
90	89	anassrs	⊢ ( ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ) ∧ ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) )
91	90	expcom	⊢ ( ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 ∧ 𝑛 ∈ ℕ₀ ) → ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
92	91	expcom	⊢ ( 𝑛 ∈ ℕ₀ → ( 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 → ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) ) )
93	92	rexlimiv	⊢ ( ∃ 𝑛 ∈ ℕ₀ 𝑒 ( 𝑅 ↑_𝑟 𝑛 ) 𝑓 → ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
94	12 93	mpcom	⊢ ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ ( 𝑓 ( trec ‘ 𝑅 ) 𝑔 ∧ 𝜑 ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) )
95	94	anassrs	⊢ ( ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ∧ 𝜑 ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) )
96	95	expcom	⊢ ( 𝜑 → ( ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
97	96	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) ) )
98	6 7 97	sylc	⊢ ( ( ⟨ 𝑒 , 𝑔 ⟩ = ⟨ 𝑒 , 𝑔 ⟩ ∧ ( ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ∧ 𝜑 ) ) → ⟨ 𝑒 , 𝑔 ⟩ ∈ ( t*rec ‘ 𝑅 ) )
99		eleq1	⊢ ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ → ( 𝑑 ∈ ( trec ‘ 𝑅 ) ↔ ⟨ 𝑒 , 𝑔 ⟩ ∈ ( trec ‘ 𝑅 ) ) )
100	98 99	syl5ibr	⊢ ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ → ( ( ⟨ 𝑒 , 𝑔 ⟩ = ⟨ 𝑒 , 𝑔 ⟩ ∧ ( ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ∧ 𝜑 ) ) → 𝑑 ∈ ( t*rec ‘ 𝑅 ) ) )
101	5 100	sylbid	⊢ ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ → ( ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ ∧ ( ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ∧ 𝜑 ) ) → 𝑑 ∈ ( t*rec ‘ 𝑅 ) ) )
102	101	anabsi5	⊢ ( ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ ∧ ( ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ∧ 𝜑 ) ) → 𝑑 ∈ ( t*rec ‘ 𝑅 ) )
103	102	anassrs	⊢ ( ( ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ ∧ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ) ∧ 𝜑 ) → 𝑑 ∈ ( t*rec ‘ 𝑅 ) )
104	103	expcom	⊢ ( 𝜑 → ( ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ ∧ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ) → 𝑑 ∈ ( t*rec ‘ 𝑅 ) ) )
105	104	exlimdvv	⊢ ( 𝜑 → ( ∃ 𝑒 ∃ 𝑔 ( 𝑑 = ⟨ 𝑒 , 𝑔 ⟩ ∧ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) ) → 𝑑 ∈ ( t*rec ‘ 𝑅 ) ) )
106	3 105	syl5bi	⊢ ( 𝜑 → ( 𝑑 ∈ { ⟨ 𝑒 , 𝑔 ⟩ ∣ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) } → 𝑑 ∈ ( t*rec ‘ 𝑅 ) ) )
107		eleq2	⊢ ( ( ( trec ‘ 𝑅 ) ∘ ( trec ‘ 𝑅 ) ) = { ⟨ 𝑒 , 𝑔 ⟩ ∣ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) } → ( 𝑑 ∈ ( ( trec ‘ 𝑅 ) ∘ ( trec ‘ 𝑅 ) ) ↔ 𝑑 ∈ { ⟨ 𝑒 , 𝑔 ⟩ ∣ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) } ) )
108	107	imbi1d	⊢ ( ( ( trec ‘ 𝑅 ) ∘ ( trec ‘ 𝑅 ) ) = { ⟨ 𝑒 , 𝑔 ⟩ ∣ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) } → ( ( 𝑑 ∈ ( ( trec ‘ 𝑅 ) ∘ ( trec ‘ 𝑅 ) ) → 𝑑 ∈ ( trec ‘ 𝑅 ) ) ↔ ( 𝑑 ∈ { ⟨ 𝑒 , 𝑔 ⟩ ∣ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) } → 𝑑 ∈ ( trec ‘ 𝑅 ) ) ) )
109	106 108	syl5ibr	⊢ ( ( ( trec ‘ 𝑅 ) ∘ ( trec ‘ 𝑅 ) ) = { ⟨ 𝑒 , 𝑔 ⟩ ∣ ∃ 𝑓 ( 𝑒 ( trec ‘ 𝑅 ) 𝑓 ∧ 𝑓 ( trec ‘ 𝑅 ) 𝑔 ) } → ( 𝜑 → ( 𝑑 ∈ ( ( trec ‘ 𝑅 ) ∘ ( trec ‘ 𝑅 ) ) → 𝑑 ∈ ( t*rec ‘ 𝑅 ) ) ) )
110	2 109	ax-mp	⊢ ( 𝜑 → ( 𝑑 ∈ ( ( trec ‘ 𝑅 ) ∘ ( trec ‘ 𝑅 ) ) → 𝑑 ∈ ( t*rec ‘ 𝑅 ) ) )
111	110	ssrdv	⊢ ( 𝜑 → ( ( trec ‘ 𝑅 ) ∘ ( trec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) )

Metamath Proof Explorer

Theorem rtrclreclem3

Proof