Theorem tz6.12-afv2

Description: Function value (Theorem 6.12(1) of TakeutiZaring p. 27), analogous to tz6.12 . (Contributed by AV, 5-Sep-2022)

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

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	bitr3id	⊢ ( 𝐴 = 𝑥 → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ↔ 𝑥 𝐹 𝑦 ) )
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	27 28	sylibr	⊢ ( ( 𝐴 ∈ V ∧ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ) → 𝐹 defAt 𝐴 )
30		dfatafv2iota	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 ) )
31	29 30	syl	⊢ ( ( 𝐴 ∈ V ∧ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ) → ( 𝐹 '''' 𝐴 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 ) )
32	4	bicomi	⊢ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ↔ 𝐴 𝐹 𝑦 )
33	32	eubii	⊢ ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ↔ ∃! 𝑦 𝐴 𝐹 𝑦 )
34	33	biimpi	⊢ ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → ∃! 𝑦 𝐴 𝐹 𝑦 )
35	5 34	anim12i	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐴 𝐹 𝑦 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) )
36	35	adantl	⊢ ( ( 𝐴 ∈ V ∧ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ) → ( 𝐴 𝐹 𝑦 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) )
37		iota1	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ( 𝐴 𝐹 𝑦 ↔ ( ℩ 𝑦 𝐴 𝐹 𝑦 ) = 𝑦 ) )
38	37	biimpac	⊢ ( ( 𝐴 𝐹 𝑦 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) → ( ℩ 𝑦 𝐴 𝐹 𝑦 ) = 𝑦 )
39	36 38	syl	⊢ ( ( 𝐴 ∈ V ∧ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ) → ( ℩ 𝑦 𝐴 𝐹 𝑦 ) = 𝑦 )
40	31 39	eqtrd	⊢ ( ( 𝐴 ∈ V ∧ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ) → ( 𝐹 '''' 𝐴 ) = 𝑦 )
41	40	ex	⊢ ( 𝐴 ∈ V → ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 '''' 𝐴 ) = 𝑦 ) )
42		eu2ndop1stv	⊢ ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → 𝐴 ∈ V )
43	42	pm2.24d	⊢ ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 → ( ¬ 𝐴 ∈ V → ( 𝐹 '''' 𝐴 ) = 𝑦 ) )
44	43	adantl	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( ¬ 𝐴 ∈ V → ( 𝐹 '''' 𝐴 ) = 𝑦 ) )
45	44	com12	⊢ ( ¬ 𝐴 ∈ V → ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 '''' 𝐴 ) = 𝑦 ) )
46	41 45	pm2.61i	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 '''' 𝐴 ) = 𝑦 )