Theorem frrlem11

Description: Lemma for 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 ordering or Infinity. To begin with, we establish the functionhood 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		funres	⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝑆 ) )
7	5 6	syl	⊢ ( 𝜑 → Fun ( 𝐹 ↾ 𝑆 ) )
8		dmres	⊢ dom ( 𝐹 ↾ 𝑆 ) = ( 𝑆 ∩ dom 𝐹 )
9		df-fn	⊢ ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ↔ ( Fun ( 𝐹 ↾ 𝑆 ) ∧ dom ( 𝐹 ↾ 𝑆 ) = ( 𝑆 ∩ dom 𝐹 ) ) )
10	8 9	mpbiran2	⊢ ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ↔ Fun ( 𝐹 ↾ 𝑆 ) )
11	7 10	sylibr	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) )
12		vex	⊢ 𝑧 ∈ V
13		ovex	⊢ ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∈ V
14	12 13	fnsn	⊢ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 }
15	11 14	jctir	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ∧ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } ) )
16		eldifn	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ dom 𝐹 )
17		elinel2	⊢ ( 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) → 𝑧 ∈ dom 𝐹 )
18	16 17	nsyl	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) )
19		disjsn	⊢ ( ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ ( 𝑆 ∩ dom 𝐹 ) )
20	18 19	sylibr	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ )
21		fnun	⊢ ( ( ( ( 𝐹 ↾ 𝑆 ) Fn ( 𝑆 ∩ dom 𝐹 ) ∧ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } Fn { 𝑧 } ) ∧ ( ( 𝑆 ∩ dom 𝐹 ) ∩ { 𝑧 } ) = ∅ ) → ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
22	15 20 21	syl2an	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
23	4	fneq1i	⊢ ( 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ↔ ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
24	22 23	sylibr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )