Theorem frrlem3

Description: Lemma for well-founded recursion. An acceptable function's domain is a subset of A . (Contributed by Paul Chapman, 21-Apr-2012)

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

Proof

Step	Hyp	Ref	Expression
1		frrlem1.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2	1	frrlem1	⊢ 𝐵 = { 𝑔 ∣ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) }
3	2	abeq2i	⊢ ( 𝑔 ∈ 𝐵 ↔ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
4		fndm	⊢ ( 𝑔 Fn 𝑧 → dom 𝑔 = 𝑧 )
5	4	sseq1d	⊢ ( 𝑔 Fn 𝑧 → ( dom 𝑔 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴 ) )
6	5	biimpar	⊢ ( ( 𝑔 Fn 𝑧 ∧ 𝑧 ⊆ 𝐴 ) → dom 𝑔 ⊆ 𝐴 )
7	6	adantrr	⊢ ( ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) → dom 𝑔 ⊆ 𝐴 )
8	7	3adant3	⊢ ( ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) → dom 𝑔 ⊆ 𝐴 )
9	8	exlimiv	⊢ ( ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) → dom 𝑔 ⊆ 𝐴 )
10	3 9	sylbi	⊢ ( 𝑔 ∈ 𝐵 → dom 𝑔 ⊆ 𝐴 )