This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ⊆ 𝐴