Theorem wfrlem3OLDa

Description: Lemma for well-ordered recursion. Show membership in the class of acceptable functions. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 31-Jul-2020)

	Ref	Expression
Hypotheses	wfrlem1OLD.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
	wfrlem3OLDa.2	⊢ 𝐺 ∈ V
Assertion	wfrlem3OLDa	⊢ ( 𝐺 ∈ 𝐵 ↔ ∃ 𝑧 ( 𝐺 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		wfrlem1OLD.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2		wfrlem3OLDa.2	⊢ 𝐺 ∈ V
3		fneq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 Fn 𝑧 ↔ 𝐺 Fn 𝑧 ) )
4		fveq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
5		reseq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
6	5	fveq2d	⊢ ( 𝑔 = 𝐺 → ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) = ( 𝐹 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
7	4 6	eqeq12d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ↔ ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
8	7	ralbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ↔ ∀ 𝑤 ∈ 𝑧 ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
9	3 8	3anbi13d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ↔ ( 𝐺 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
10	9	exbidv	⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ↔ ∃ 𝑧 ( 𝐺 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
11	1	wfrlem1OLD	⊢ 𝐵 = { 𝑔 ∣ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) }
12	2 10 11	elab2	⊢ ( 𝐺 ∈ 𝐵 ↔ ∃ 𝑧 ( 𝐺 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )