Metamath Proof Explorer

Theorem frrlem1

Description: Lemma for well-founded recursion. The final item we are interested in is the union of acceptable functions B . This lemma just changes bound variables for later use. (Contributed by Paul Chapman, 21-Apr-2012)

Ref Expression
Hypothesis frrlem1.1 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
Assertion frrlem1 𝐵 = { 𝑔 ∣ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) }

Proof

Step Hyp Ref Expression
1 frrlem1.1 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2 fneq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 Fn 𝑥 ↔ 𝑔 Fn 𝑥 ) )
3 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) )
4 reseq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
5 4 oveq2d ⊢ ( 𝑓 = 𝑔 → ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
6 3 5 eqeq12d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
7 6 ralbidv ⊢ ( 𝑓 = 𝑔 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
8 2 7 3anbi13d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( 𝑔 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
9 8 exbidv ⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ∃ 𝑥 ( 𝑔 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
10 fneq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑔 Fn 𝑥 ↔ 𝑔 Fn 𝑧 ) )
11 sseq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴 ) )
12 sseq2 ⊢ ( 𝑥 = 𝑧 → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ↔ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑧 ) )
13 12 raleqbi1dv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑧 ) )
14 predeq3 ⊢ ( 𝑦 = 𝑤 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑤 ) )
15 14 sseq1d ⊢ ( 𝑦 = 𝑤 → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑧 ↔ Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) )
16 15 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑧 ↔ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 )
17 13 16 bitrdi ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ↔ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) )
18 11 17 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ↔ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) )
19 raleq ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑧 ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
20 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑤 ) )
21 id ⊢ ( 𝑦 = 𝑤 → 𝑦 = 𝑤 )
22 14 reseq2d ⊢ ( 𝑦 = 𝑤 → ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
23 21 22 oveq12d ⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
24 20 23 eqeq12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
25 24 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝑧 ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
26 19 25 bitrdi ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
27 10 18 26 3anbi123d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑔 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
28 27 cbvexvw ⊢ ( ∃ 𝑥 ( 𝑔 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑔 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
29 9 28 bitrdi ⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
30 29 cbvabv ⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑔 ∣ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) }
31 1 30 eqtri ⊢ 𝐵 = { 𝑔 ∣ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) }