Theorem tz6.12c-afv2

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

	Ref	Expression
Assertion	tz6.12c-afv2	$$⊢\exists !yAFy\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=y\leftrightarrow AFy\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfeu1	$$⊢Ⅎy\exists !yAFy$$
2		nfv	$$⊢ℲyAF\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)$$
3		euex	$$⊢\exists !yAFy\to \exists yAFy$$
4		tz6.12-1-afv2	$$⊢\left(AFy\wedge \exists !yAFy\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=y$$
5	4	expcom	$$⊢\exists !yAFy\to \left(AFy\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=y\right)$$
6		breq2	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=y\to \left(AF\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\leftrightarrow AFy\right)$$
7	6	biimprd	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=y\to \left(AFy\to AF\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\right)$$
8	5 7	syli	$$⊢\exists !yAFy\to \left(AFy\to AF\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\right)$$
9	1 2 3 8	exlimimdd	$$⊢\exists !yAFy\to AF\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)$$
10	9 6	syl5ibcom	$$⊢\exists !yAFy\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=y\to AFy\right)$$
11	10 5	impbid	$$⊢\exists !yAFy\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=y\leftrightarrow AFy\right)$$