This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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