Theorem fpr2

Description: Law of well-founded recursion over a partial order, part two. Now we establish the value of F within A . (Contributed by Scott Fenton, 11-Sep-2023)

	Ref	Expression
Hypothesis	fprr.1	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion	fpr2	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fprr.1	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
2	1	fpr1	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 )
3	2	fndmd	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → dom 𝐹 = 𝐴 )
4	3	eleq2d	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ 𝐴 ) )
5	4	biimpar	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ dom 𝐹 )
6		fveq2	⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
7		id	⊢ ( 𝑦 = 𝑋 → 𝑦 = 𝑋 )
8		predeq3	⊢ ( 𝑦 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
9	8	reseq2d	⊢ ( 𝑦 = 𝑋 → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
10	7 9	oveq12d	⊢ ( 𝑦 = 𝑋 → ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
11	6 10	eqeq12d	⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) )
12	11	imbi2d	⊢ ( 𝑦 = 𝑋 → ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) ) )
13		eqid	⊢ { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) } = { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) }
14	13	frrlem1	⊢ { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
15	14 1	fprlem1	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑔 ∈ { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) } ∧ ℎ ∈ { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) } ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
16	14 1 15	frrlem10	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
17	16	expcom	⊢ ( 𝑦 ∈ dom 𝐹 → ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
18	12 17	vtoclga	⊢ ( 𝑋 ∈ dom 𝐹 → ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) )
19	18	impcom	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
20	5 19	syldan	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )