Metamath Proof Explorer

Theorem wfrlem1

Description: Lemma for well-ordered 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 Scott Fenton, 21-Apr-2011)

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

Proof

Step Hyp Ref Expression
1 wfrlem1.1 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2 fneq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 Fn 𝑥 ↔ 𝑔 Fn 𝑥 ) )
3 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) )
4 reseq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
5 4 fveq2d ⊢ ( 𝑓 = 𝑔 → ( 𝐹 ‘ ( 𝑓 ↾ 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 14 reseq2d ⊢ ( 𝑦 = 𝑤 → ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
22 21 fveq2d ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
23 20 22 eqeq12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑔 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
24 23 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝑧 ( 𝑔 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
25 19 24 bitrdi ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑔 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
26 10 18 25 3anbi123d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑔 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑔 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
27 26 cbvexvw ⊢ ( ∃ 𝑥 ( 𝑔 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑔 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
28 9 27 bitrdi ⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
29 28 cbvabv ⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑔 ∣ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) }
30 1 29 eqtri ⊢ 𝐵 = { 𝑔 ∣ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) }