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

Metamath Proof Explorer

Theorem frrlem9

Description: Lemma for well-founded recursion. Show that the well-founded recursive generator produces a function. Hypothesis three will be eliminated using different induction rules depending on if we use partial orders or the axiom of infinity. (Contributed by Scott Fenton, 27-Aug-2022)

Ref Expression
Hypotheses frrlem9.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
frrlem9.2 ⊢ F = frecs ⁡ R A G
frrlem9.3 ⊢ φ ∧ g ∈ B ∧ h ∈ B → x g u ∧ x h v → u = v
Assertion frrlem9 ⊢ φ → Fun ⁡ F

Proof

Step Hyp Ref Expression
1 frrlem9.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 frrlem9.2 ⊢ F = frecs ⁡ R A G
3 frrlem9.3 ⊢ φ ∧ g ∈ B ∧ h ∈ B → x g u ∧ x h v → u = v
4 eluni2 ⊢ x u ∈ ⋃ B ↔ ∃ g ∈ B x u ∈ g
5 df-br ⊢ x F u ↔ x u ∈ F
6 1 2 frrlem5 ⊢ F = ⋃ B
7 6 eleq2i ⊢ x u ∈ F ↔ x u ∈ ⋃ B
8 5 7 bitri ⊢ x F u ↔ x u ∈ ⋃ B
9 df-br ⊢ x g u ↔ x u ∈ g
10 9 rexbii ⊢ ∃ g ∈ B x g u ↔ ∃ g ∈ B x u ∈ g
11 4 8 10 3bitr4i ⊢ x F u ↔ ∃ g ∈ B x g u
12 eluni2 ⊢ x v ∈ ⋃ B ↔ ∃ h ∈ B x v ∈ h
13 df-br ⊢ x F v ↔ x v ∈ F
14 6 eleq2i ⊢ x v ∈ F ↔ x v ∈ ⋃ B
15 13 14 bitri ⊢ x F v ↔ x v ∈ ⋃ B
16 df-br ⊢ x h v ↔ x v ∈ h
17 16 rexbii ⊢ ∃ h ∈ B x h v ↔ ∃ h ∈ B x v ∈ h
18 12 15 17 3bitr4i ⊢ x F v ↔ ∃ h ∈ B x h v
19 11 18 anbi12i ⊢ x F u ∧ x F v ↔ ∃ g ∈ B x g u ∧ ∃ h ∈ B x h v
20 reeanv ⊢ ∃ g ∈ B ∃ h ∈ B x g u ∧ x h v ↔ ∃ g ∈ B x g u ∧ ∃ h ∈ B x h v
21 19 20 bitr4i ⊢ x F u ∧ x F v ↔ ∃ g ∈ B ∃ h ∈ B x g u ∧ x h v
22 3 rexlimdvva ⊢ φ → ∃ g ∈ B ∃ h ∈ B x g u ∧ x h v → u = v
23 21 22 biimtrid ⊢ φ → x F u ∧ x F v → u = v
24 23 alrimiv ⊢ φ → ∀ v x F u ∧ x F v → u = v
25 24 alrimivv ⊢ φ → ∀ x ∀ u ∀ v x F u ∧ x F v → u = v
26 1 2 frrlem6 ⊢ Rel ⁡ F
27 dffun2 ⊢ Fun ⁡ F ↔ Rel ⁡ F ∧ ∀ x ∀ u ∀ v x F u ∧ x F v → u = v
28 26 27 mpbiran ⊢ Fun ⁡ F ↔ ∀ x ∀ u ∀ v x F u ∧ x F v → u = v
29 25 28 sylibr ⊢ φ → Fun ⁡ F