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	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
	frrlem9.2	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
	frrlem9.3	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
Assertion	frrlem9	⊢ ( 𝜑 → Fun 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		frrlem9.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2		frrlem9.2	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
3		frrlem9.3	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
4		eluni2	⊢ ( ⟨ 𝑥 , 𝑢 ⟩ ∈ ∪ 𝐵 ↔ ∃ 𝑔 ∈ 𝐵 ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 )
5		df-br	⊢ ( 𝑥 𝐹 𝑢 ↔ ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝐹 )
6	1 2	frrlem5	⊢ 𝐹 = ∪ 𝐵
7	6	eleq2i	⊢ ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑢 ⟩ ∈ ∪ 𝐵 )
8	5 7	bitri	⊢ ( 𝑥 𝐹 𝑢 ↔ ⟨ 𝑥 , 𝑢 ⟩ ∈ ∪ 𝐵 )
9		df-br	⊢ ( 𝑥 𝑔 𝑢 ↔ ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 )
10	9	rexbii	⊢ ( ∃ 𝑔 ∈ 𝐵 𝑥 𝑔 𝑢 ↔ ∃ 𝑔 ∈ 𝐵 ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 )
11	4 8 10	3bitr4i	⊢ ( 𝑥 𝐹 𝑢 ↔ ∃ 𝑔 ∈ 𝐵 𝑥 𝑔 𝑢 )
12		eluni2	⊢ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ ∪ 𝐵 ↔ ∃ ℎ ∈ 𝐵 ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ )
13		df-br	⊢ ( 𝑥 𝐹 𝑣 ↔ ⟨ 𝑥 , 𝑣 ⟩ ∈ 𝐹 )
14	6	eleq2i	⊢ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑣 ⟩ ∈ ∪ 𝐵 )
15	13 14	bitri	⊢ ( 𝑥 𝐹 𝑣 ↔ ⟨ 𝑥 , 𝑣 ⟩ ∈ ∪ 𝐵 )
16		df-br	⊢ ( 𝑥 ℎ 𝑣 ↔ ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ )
17	16	rexbii	⊢ ( ∃ ℎ ∈ 𝐵 𝑥 ℎ 𝑣 ↔ ∃ ℎ ∈ 𝐵 ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ )
18	12 15 17	3bitr4i	⊢ ( 𝑥 𝐹 𝑣 ↔ ∃ ℎ ∈ 𝐵 𝑥 ℎ 𝑣 )
19	11 18	anbi12i	⊢ ( ( 𝑥 𝐹 𝑢 ∧ 𝑥 𝐹 𝑣 ) ↔ ( ∃ 𝑔 ∈ 𝐵 𝑥 𝑔 𝑢 ∧ ∃ ℎ ∈ 𝐵 𝑥 ℎ 𝑣 ) )
20		reeanv	⊢ ( ∃ 𝑔 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ↔ ( ∃ 𝑔 ∈ 𝐵 𝑥 𝑔 𝑢 ∧ ∃ ℎ ∈ 𝐵 𝑥 ℎ 𝑣 ) )
21	19 20	bitr4i	⊢ ( ( 𝑥 𝐹 𝑢 ∧ 𝑥 𝐹 𝑣 ) ↔ ∃ 𝑔 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) )
22	3	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑔 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
23	21 22	syl5bi	⊢ ( 𝜑 → ( ( 𝑥 𝐹 𝑢 ∧ 𝑥 𝐹 𝑣 ) → 𝑢 = 𝑣 ) )
24	23	alrimiv	⊢ ( 𝜑 → ∀ 𝑣 ( ( 𝑥 𝐹 𝑢 ∧ 𝑥 𝐹 𝑣 ) → 𝑢 = 𝑣 ) )
25	24	alrimivv	⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑢 ∀ 𝑣 ( ( 𝑥 𝐹 𝑢 ∧ 𝑥 𝐹 𝑣 ) → 𝑢 = 𝑣 ) )
26	1 2	frrlem6	⊢ Rel 𝐹
27		dffun2	⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∀ 𝑢 ∀ 𝑣 ( ( 𝑥 𝐹 𝑢 ∧ 𝑥 𝐹 𝑣 ) → 𝑢 = 𝑣 ) ) )
28	26 27	mpbiran	⊢ ( Fun 𝐹 ↔ ∀ 𝑥 ∀ 𝑢 ∀ 𝑣 ( ( 𝑥 𝐹 𝑢 ∧ 𝑥 𝐹 𝑣 ) → 𝑢 = 𝑣 ) )
29	25 28	sylibr	⊢ ( 𝜑 → Fun 𝐹 )