tz6.12i-afv2

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

		Ref	Expression
	Assertion	tz6.12i-afv2	$⊢ B \in ran F \to ((F'''' A) = B \to A F B)$

Step	Hyp	Ref	Expression
1		eleq1	$⊢ (F'''' A) = y \to ((F'''' A) \in ran F \leftrightarrow y \in ran F)$
2		dfatafv2rnb	$⊢ F defAt A \leftrightarrow (F'''' A) \in ran F$
3		dfdfat2	$⊢ F defAt A \leftrightarrow (A \in dom F \land \exists! y A F y)$
4	3	simprbi	$⊢ F defAt A \to \exists! y A F y$
5	2 4	sylbir	$⊢ (F'''' A) \in ran F \to \exists! y A F y$
6		tz6.12c-afv2	$⊢ \exists! y A F y \to ((F'''' A) = y \leftrightarrow A F y)$
7	5 6	syl	$⊢ (F'''' A) \in ran F \to ((F'''' A) = y \leftrightarrow A F y)$
8	7	biimpcd	$⊢ (F'''' A) = y \to ((F'''' A) \in ran F \to A F y)$
9	1 8	sylbird	$⊢ (F'''' A) = y \to (y \in ran F \to A F y)$
10	9	eqcoms	$⊢ y = (F'''' A) \to (y \in ran F \to A F y)$
11		eleq1	$⊢ y = (F'''' A) \to (y \in ran F \leftrightarrow (F'''' A) \in ran F)$
12		breq2	$⊢ y = (F'''' A) \to (A F y \leftrightarrow A F (F'''' A))$
13	10 11 12	3imtr3d	$⊢ y = (F'''' A) \to ((F'''' A) \in ran F \to A F (F'''' A))$
14	13	vtocleg	$⊢ (F'''' A) \in ran F \to ((F'''' A) \in ran F \to A F (F'''' A))$
15	14	pm2.43i	$⊢ (F'''' A) \in ran F \to A F (F'''' A)$
16	15	a1i	$⊢ (F'''' A) = B \to ((F'''' A) \in ran F \to A F (F'''' A))$
17		eleq1	$⊢ (F'''' A) = B \to ((F'''' A) \in ran F \leftrightarrow B \in ran F)$
18		breq2	$⊢ (F'''' A) = B \to (A F (F'''' A) \leftrightarrow A F B)$
19	16 17 18	3imtr3d	$⊢ (F'''' A) = B \to (B \in ran F \to A F B)$
20	19	com12	$⊢ B \in ran F \to ((F'''' A) = B \to A F B)$

Metamath Proof Explorer