Theorem frrlem7

Description: Lemma for well-founded recursion. The well-founded recursion generator's domain is a subclass of A . (Contributed by Scott Fenton, 27-Aug-2022)

	Ref	Expression
Hypotheses	frrlem5.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
	frrlem5.2	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion	frrlem7	⊢ dom 𝐹 ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		frrlem5.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2		frrlem5.2	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
3	1 2	frrlem5	⊢ 𝐹 = ∪ 𝐵
4	3	dmeqi	⊢ dom 𝐹 = dom ∪ 𝐵
5		dmuni	⊢ dom ∪ 𝐵 = ∪ 𝑔 ∈ 𝐵 dom 𝑔
6	4 5	eqtri	⊢ dom 𝐹 = ∪ 𝑔 ∈ 𝐵 dom 𝑔
7	6	sseq1i	⊢ ( dom 𝐹 ⊆ 𝐴 ↔ ∪ 𝑔 ∈ 𝐵 dom 𝑔 ⊆ 𝐴 )
8		iunss	⊢ ( ∪ 𝑔 ∈ 𝐵 dom 𝑔 ⊆ 𝐴 ↔ ∀ 𝑔 ∈ 𝐵 dom 𝑔 ⊆ 𝐴 )
9	7 8	bitri	⊢ ( dom 𝐹 ⊆ 𝐴 ↔ ∀ 𝑔 ∈ 𝐵 dom 𝑔 ⊆ 𝐴 )
10	1	frrlem3	⊢ ( 𝑔 ∈ 𝐵 → dom 𝑔 ⊆ 𝐴 )
11	9 10	mprgbir	⊢ dom 𝐹 ⊆ 𝐴