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 ⊢ B = f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y G f ↾ Pred R A y
frrlem5.2 ⊢ F = frecs ⁡ R A G
Assertion frrlem7 ⊢ dom ⁡ F ⊆ A

Proof

Step Hyp Ref Expression
1 frrlem5.1 ⊢ B = f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y G f ↾ Pred R A y
2 frrlem5.2 ⊢ F = frecs ⁡ R A G
3 1 2 frrlem5 ⊢ F = ⋃ B
4 3 dmeqi ⊢ dom ⁡ F = dom ⁡ ⋃ B
5 dmuni ⊢ dom ⁡ ⋃ B = ⋃ g ∈ B dom ⁡ g
6 4 5 eqtri ⊢ dom ⁡ F = ⋃ g ∈ B dom ⁡ g
7 6 sseq1i ⊢ dom ⁡ F ⊆ A ↔ ⋃ g ∈ B dom ⁡ g ⊆ A
8 iunss ⊢ ⋃ g ∈ B dom ⁡ g ⊆ A ↔ ∀ g ∈ B dom ⁡ g ⊆ A
9 7 8 bitri ⊢ dom ⁡ F ⊆ A ↔ ∀ g ∈ B dom ⁡ g ⊆ A
10 1 frrlem3 ⊢ g ∈ B → dom ⁡ g ⊆ A
11 9 10 mprgbir ⊢ dom ⁡ F ⊆ A