Theorem tfr3ALT

Description: Alternate proof of tfr3 using well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	tfrALT.1	⊢ 𝐹 = recs ( 𝐺 )
Assertion	tfr3ALT	⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → 𝐵 = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		tfrALT.1	⊢ 𝐹 = recs ( 𝐺 )
2		predon	⊢ ( 𝑥 ∈ On → Pred ( E , On , 𝑥 ) = 𝑥 )
3	2	reseq2d	⊢ ( 𝑥 ∈ On → ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) = ( 𝐵 ↾ 𝑥 ) )
4	3	fveq2d	⊢ ( 𝑥 ∈ On → ( 𝐺 ‘ ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) )
5	4	eqeq2d	⊢ ( 𝑥 ∈ On → ( ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) ) ↔ ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) )
6	5	ralbiia	⊢ ( ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) )
7		epweon	⊢ E We On
8		epse	⊢ E Se On
9		df-recs	⊢ recs ( 𝐺 ) = wrecs ( E , On , 𝐺 )
10	1 9	eqtri	⊢ 𝐹 = wrecs ( E , On , 𝐺 )
11	10	wfr3	⊢ ( ( ( E We On ∧ E Se On ) ∧ ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) ) ) ) → 𝐹 = 𝐵 )
12	7 8 11	mpanl12	⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) ) ) → 𝐹 = 𝐵 )
13	6 12	sylan2br	⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → 𝐹 = 𝐵 )
14	13	eqcomd	⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → 𝐵 = 𝐹 )