frrlem11

Description: Lemma for well-founded recursion. For the next several theorems we will be aiming to prove that dom F = A . To do this, we set up a function C that supposedly contains an element of A that is not in dom F and we show that the element must be in dom F . Our choice of what to restrict F to depends on if we assume partial orders or the axiom of infinity. To begin with, we establish the functionality of C . (Contributed by Scott Fenton, 7-Dec-2022)

	Ref	Expression
Hypotheses	frrlem11.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
	frrlem11.2	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
	frrlem11.3	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
	frrlem11.4	⊢ 𝐶 = ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
Assertion	frrlem11	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )

Proof

Step	Hyp	Ref	Expression
1		frrlem11.1	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2		frrlem11.2	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
3		frrlem11.3	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
4		frrlem11.4	⊢ 𝐶 = ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
5	1 2 3	frrlem9	⊢ ( 𝜑 → Fun 𝐹 )
6	5	funresd	⊢ ( 𝜑 → Fun ( 𝐹 ↾ 𝑆 ) )
7		dmres	⊢ dom ( 𝐹 ↾ 𝑆 ) = ( 𝑆 ∩ dom 𝐹 )
8		df-fn	⊢ ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ↔ ( Fun ( 𝐹 ↾ 𝑆 ) ∧ dom ( 𝐹 ↾ 𝑆 ) = ( 𝑆 ∩ dom 𝐹 ) ) )
9	7 8	mpbiran2	⊢ ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ↔ Fun ( 𝐹 ↾ 𝑆 ) )
10	6 9	sylibr	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) )
11		vex	⊢ 𝑧 ∈ V
12		ovex	⊢ ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∈ V
13	11 12	fnsn	⊢ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 }
14	10 13	jctir	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ∧ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } ) )
15		eldifn	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ dom 𝐹 )
16		elinel2	⊢ ( 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) → 𝑧 ∈ dom 𝐹 )
17	15 16	nsyl	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) )
18		disjsn	⊢ ( ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) )
19	17 18	sylibr	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ )
20		fnun	⊢ ( ( ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ∧ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } ) ∧ ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ ) → ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
21	14 19 20	syl2an	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
22	4	fneq1i	⊢ ( 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ↔ ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
23	21 22	sylibr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )

Metamath Proof Explorer

Theorem frrlem11

Proof