Theorem wfrlem13

Description: Lemma for well-founded recursion. From here through wfrlem16 , we aim to prove that dom F = A . We do this by supposing that there is an element z of A that is not in dom F . We then define C by extending dom F with the appropriate value at z . We then show that z cannot be an R minimal element of ( A \ dom F ) , meaning that ( A \ dom F ) must be empty, so dom F = A . Here, we show that C is a function extending the domain of F by one. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	wfrlem13.1	⊢ 𝑅 We 𝐴
	wfrlem13.2	⊢ 𝑅 Se 𝐴
	wfrlem13.3	⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
	wfrlem13.4	⊢ 𝐶 = ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
Assertion	wfrlem13	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) )

Proof

Step	Hyp	Ref	Expression
1		wfrlem13.1	⊢ 𝑅 We 𝐴
2		wfrlem13.2	⊢ 𝑅 Se 𝐴
3		wfrlem13.3	⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
4		wfrlem13.4	⊢ 𝐶 = ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
5	1 2 3	wfrfun	⊢ Fun 𝐹
6		vex	⊢ 𝑧 ∈ V
7		fvex	⊢ ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ∈ V
8	6 7	funsn	⊢ Fun { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ }
9	5 8	pm3.2i	⊢ ( Fun 𝐹 ∧ Fun { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
10	7	dmsnop	⊢ dom { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } = { 𝑧 }
11	10	ineq2i	⊢ ( dom 𝐹 ∩ dom { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( dom 𝐹 ∩ { 𝑧 } )
12		eldifn	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ¬ 𝑧 ∈ dom 𝐹 )
13		disjsn	⊢ ( ( dom 𝐹 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ dom 𝐹 )
14	12 13	sylibr	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( dom 𝐹 ∩ { 𝑧 } ) = ∅ )
15	11 14	syl5eq	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( dom 𝐹 ∩ dom { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ∅ )
16		funun	⊢ ( ( ( Fun 𝐹 ∧ Fun { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ∧ ( dom 𝐹 ∩ dom { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ∅ ) → Fun ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) )
17	9 15 16	sylancr	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → Fun ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) )
18		dmun	⊢ dom ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( dom 𝐹 ∪ dom { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
19	10	uneq2i	⊢ ( dom 𝐹 ∪ dom { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( dom 𝐹 ∪ { 𝑧 } )
20	18 19	eqtri	⊢ dom ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( dom 𝐹 ∪ { 𝑧 } )
21	4	fneq1i	⊢ ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ↔ ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) Fn ( dom 𝐹 ∪ { 𝑧 } ) )
22		df-fn	⊢ ( ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) Fn ( dom 𝐹 ∪ { 𝑧 } ) ↔ ( Fun ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ∧ dom ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( dom 𝐹 ∪ { 𝑧 } ) ) )
23	21 22	bitri	⊢ ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ↔ ( Fun ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ∧ dom ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( dom 𝐹 ∪ { 𝑧 } ) ) )
24	17 20 23	sylanblrc	⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) )