Metamath Proof Explorer

Theorem frecseq123

Description: Equality theorem for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021)

Ref Expression
Assertion frecseq123 ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → frecs ( 𝑅 , 𝐴 , 𝐹 ) = frecs ( 𝑆 , 𝐵 , 𝐺 ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → 𝐴 = 𝐵 )
2 1 sseq2d ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵 ) )
3 equid ⊢ 𝑦 = 𝑦
4 predeq123 ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑦 = 𝑦 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑆 , 𝐵 , 𝑦 ) )
5 3 4 mp3an3 ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑆 , 𝐵 , 𝑦 ) )
6 5 3adant3 ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑆 , 𝐵 , 𝑦 ) )
7 6 sseq1d ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ↔ Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) )
8 7 ralbidv ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) )
9 2 8 anbi12d ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ) )
10 simp3 ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → 𝐹 = 𝐺 )
11 10 oveqd ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
12 6 reseq2d ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) )
13 12 oveq2d ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) )
14 11 13 eqtrd ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) )
15 14 eqeq2d ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) )
16 15 ralbidv ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) )
17 9 16 3anbi23d ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) ) )
18 17 exbidv ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) ) )
19 18 abbidv ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) } )
20 19 unieqd ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) } )
21 df-frecs ⊢ frecs ( 𝑅 , 𝐴 , 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
22 df-frecs ⊢ frecs ( 𝑆 , 𝐵 , 𝐺 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) }
23 20 21 22 3eqtr4g ⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → frecs ( 𝑅 , 𝐴 , 𝐹 ) = frecs ( 𝑆 , 𝐵 , 𝐺 ) )