Metamath Proof Explorer


Theorem wrecseq123

Description: General equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018)

Ref Expression
Assertion wrecseq123 ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → wrecs ( 𝑅 , 𝐴 , 𝐹 ) = wrecs ( 𝑆 , 𝐵 , 𝐺 ) )

Proof

Step Hyp Ref Expression
1 sseq2 ( 𝐴 = 𝐵 → ( 𝑥𝐴𝑥𝐵 ) )
2 1 3ad2ant2 ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → ( 𝑥𝐴𝑥𝐵 ) )
3 predeq1 ( 𝑅 = 𝑆 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑆 , 𝐴 , 𝑦 ) )
4 predeq2 ( 𝐴 = 𝐵 → Pred ( 𝑆 , 𝐴 , 𝑦 ) = Pred ( 𝑆 , 𝐵 , 𝑦 ) )
5 3 4 sylan9eq ( ( 𝑅 = 𝑆𝐴 = 𝐵 ) → 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 5 reseq2d ( ( 𝑅 = 𝑆𝐴 = 𝐵 ) → ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) )
12 11 3adant3 ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) )
13 10 12 fveq12d ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) )
14 13 eqeq2d ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → ( ( 𝑓𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝑓𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) )
15 14 ralbidv ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → ( ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) )
16 9 15 3anbi23d ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐵 ∧ ∀ 𝑦𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) ) )
17 16 exbidv ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐵 ∧ ∀ 𝑦𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) ) )
18 17 abbidv ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐵 ∧ ∀ 𝑦𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) } )
19 18 unieqd ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐵 ∧ ∀ 𝑦𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) } )
20 df-wrecs wrecs ( 𝑅 , 𝐴 , 𝐹 ) = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
21 df-wrecs wrecs ( 𝑆 , 𝐵 , 𝐺 ) = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐵 ∧ ∀ 𝑦𝑥 Pred ( 𝑆 , 𝐵 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑆 , 𝐵 , 𝑦 ) ) ) ) }
22 19 20 21 3eqtr4g ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → wrecs ( 𝑅 , 𝐴 , 𝐹 ) = wrecs ( 𝑆 , 𝐵 , 𝐺 ) )