Theorem setrec2lem2

Description: Lemma for setrec2 . The functional part of F is a function. (Contributed by Emmett Weisz, 6-Mar-2021) (New usage is discouraged.)

	Ref	Expression
Assertion	setrec2lem2	⊢ Fun ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } )
2		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
3		eqeq2	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 = 𝑧 ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
4	3	imbi2d	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 → 𝑦 = 𝑧 ) ↔ ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
5	4	albidv	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( ∀ 𝑦 ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 → 𝑦 = 𝑧 ) ↔ ∀ 𝑦 ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ) )
6	2 5	spcev	⊢ ( ∀ 𝑦 ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∀ 𝑦 ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 → 𝑦 = 𝑧 ) )
7		vex	⊢ 𝑦 ∈ V
8	7	brresi	⊢ ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 ↔ ( 𝑥 ∈ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ∧ 𝑥 𝐹 𝑦 ) )
9		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ↔ ∃! 𝑦 𝑥 𝐹 𝑦 )
10		tz6.12-1	⊢ ( ( 𝑥 𝐹 𝑦 ∧ ∃! 𝑦 𝑥 𝐹 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = 𝑦 )
11	10	ancoms	⊢ ( ( ∃! 𝑦 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = 𝑦 )
12	9 11	sylanb	⊢ ( ( 𝑥 ∈ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ∧ 𝑥 𝐹 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = 𝑦 )
13	12	eqcomd	⊢ ( ( 𝑥 ∈ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ∧ 𝑥 𝐹 𝑦 ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
14	8 13	sylbi	⊢ ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
15	6 14	mpg	⊢ ∃ 𝑧 ∀ 𝑦 ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 → 𝑦 = 𝑧 )
16	15	ax-gen	⊢ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 → 𝑦 = 𝑧 )
17		nfcv	⊢ Ⅎ 𝑥 𝐹
18		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 }
19	17 18	nfres	⊢ Ⅎ 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } )
20		nfcv	⊢ Ⅎ 𝑦 𝐹
21		nfeu1	⊢ Ⅎ 𝑦 ∃! 𝑦 𝑥 𝐹 𝑦
22	21	nfab	⊢ Ⅎ 𝑦 { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 }
23	20 22	nfres	⊢ Ⅎ 𝑦 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } )
24		nfcv	⊢ Ⅎ 𝑧 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } )
25	19 23 24	dffun3f	⊢ ( Fun ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) ↔ ( Rel ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) 𝑦 → 𝑦 = 𝑧 ) ) )
26	1 16 25	mpbir2an	⊢ Fun ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } )