Theorem tz6.12-afv

Description: Function value. Theorem 6.12(1) of TakeutiZaring p. 27, analogous to tz6.12 . (Contributed by Alexander van der Vekens, 29-Nov-2017)

	Ref	Expression
Assertion	tz6.12-afv	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 ''' 𝐴 ) = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ V ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → 𝐴 ∈ V )
2		vex	⊢ 𝑦 ∈ V
3	2	a1i	⊢ ( ( 𝐴 ∈ V ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → 𝑦 ∈ V )
4		df-br	⊢ ( 𝐴 𝐹 𝑦 ↔ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 )
5	4	biimpri	⊢ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → 𝐴 𝐹 𝑦 )
6	5	adantl	⊢ ( ( 𝐴 ∈ V ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → 𝐴 𝐹 𝑦 )
7		breldmg	⊢ ( ( 𝐴 ∈ V ∧ 𝑦 ∈ V ∧ 𝐴 𝐹 𝑦 ) → 𝐴 ∈ dom 𝐹 )
8	1 3 6 7	syl3anc	⊢ ( ( 𝐴 ∈ V ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → 𝐴 ∈ dom 𝐹 )
9		simpl	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → 𝐴 ∈ dom 𝐹 )
10		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
11		breq1	⊢ ( 𝐴 = 𝑥 → ( 𝐴 𝐹 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
12	4 11	syl5bbr	⊢ ( 𝐴 = 𝑥 → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ↔ 𝑥 𝐹 𝑦 ) )
13	12	eqcoms	⊢ ( 𝑥 = 𝐴 → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ↔ 𝑥 𝐹 𝑦 ) )
14	13	eubidv	⊢ ( 𝑥 = 𝐴 → ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ↔ ∃! 𝑦 𝑥 𝐹 𝑦 ) )
15	14	biimpd	⊢ ( 𝑥 = 𝐴 → ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → ∃! 𝑦 𝑥 𝐹 𝑦 ) )
16	10 15	sylbi	⊢ ( 𝑥 ∈ { 𝐴 } → ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → ∃! 𝑦 𝑥 𝐹 𝑦 ) )
17	16	com12	⊢ ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → ( 𝑥 ∈ { 𝐴 } → ∃! 𝑦 𝑥 𝐹 𝑦 ) )
18	17	adantl	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝑥 ∈ { 𝐴 } → ∃! 𝑦 𝑥 𝐹 𝑦 ) )
19	18	ralrimiv	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ∀ 𝑥 ∈ { 𝐴 } ∃! 𝑦 𝑥 𝐹 𝑦 )
20		fnres	⊢ ( ( 𝐹 ↾ { 𝐴 } ) Fn { 𝐴 } ↔ ∀ 𝑥 ∈ { 𝐴 } ∃! 𝑦 𝑥 𝐹 𝑦 )
21		fnfun	⊢ ( ( 𝐹 ↾ { 𝐴 } ) Fn { 𝐴 } → Fun ( 𝐹 ↾ { 𝐴 } ) )
22	20 21	sylbir	⊢ ( ∀ 𝑥 ∈ { 𝐴 } ∃! 𝑦 𝑥 𝐹 𝑦 → Fun ( 𝐹 ↾ { 𝐴 } ) )
23	19 22	syl	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → Fun ( 𝐹 ↾ { 𝐴 } ) )
24	9 23	jca	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
25	24	ex	⊢ ( 𝐴 ∈ dom 𝐹 → ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ) )
26	8 25	syl	⊢ ( ( 𝐴 ∈ V ∧ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ) )
27	26	impr	⊢ ( ( 𝐴 ∈ V ∧ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ) → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
28		df-dfat	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
29		afvfundmfveq	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
30	28 29	sylbir	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
31	27 30	syl	⊢ ( ( 𝐴 ∈ V ∧ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ) → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
32		tz6.12	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 ‘ 𝐴 ) = 𝑦 )
33	32	adantl	⊢ ( ( 𝐴 ∈ V ∧ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ) → ( 𝐹 ‘ 𝐴 ) = 𝑦 )
34	31 33	eqtrd	⊢ ( ( 𝐴 ∈ V ∧ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ) → ( 𝐹 ''' 𝐴 ) = 𝑦 )
35	34	ex	⊢ ( 𝐴 ∈ V → ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 ''' 𝐴 ) = 𝑦 ) )
36		eu2ndop1stv	⊢ ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → 𝐴 ∈ V )
37	36	pm2.24d	⊢ ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → ( ¬ 𝐴 ∈ V → ( 𝐹 ''' 𝐴 ) = 𝑦 ) )
38	37	adantl	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( ¬ 𝐴 ∈ V → ( 𝐹 ''' 𝐴 ) = 𝑦 ) )
39	38	com12	⊢ ( ¬ 𝐴 ∈ V → ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 ''' 𝐴 ) = 𝑦 ) )
40	35 39	pm2.61i	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 ''' 𝐴 ) = 𝑦 )