Metamath Proof Explorer


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 ( 𝐵𝑥 ) = ( 𝐺 ‘ ( 𝐵𝑥 ) ) ) → 𝐵 = 𝐹 )