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	$⊢ (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (F'''' A) = y$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in V \land ⟨A, y⟩ \in F) \to A \in V$
2		vex	$⊢ y \in V$
3	2	a1i	$⊢ (A \in V \land ⟨A, y⟩ \in F) \to y \in V$
4		df-br	$⊢ A F y \leftrightarrow ⟨A, y⟩ \in F$
5	4	biimpri	$⊢ ⟨A, y⟩ \in F \to A F y$
6	5	adantl	$⊢ (A \in V \land ⟨A, y⟩ \in F) \to A F y$
7		breldmg	$⊢ (A \in V \land y \in V \land A F y) \to A \in dom F$
8	1 3 6 7	syl3anc	$⊢ (A \in V \land ⟨A, y⟩ \in F) \to A \in dom F$
9		simpl	$⊢ (A \in dom F \land \exists! y ⟨A, y⟩ \in F) \to A \in dom F$
10		velsn	$⊢ x \in \{A\} \leftrightarrow x = A$
11		breq1	$⊢ A = x \to (A F y \leftrightarrow x F y)$
12	4 11	bitr3id	$⊢ A = x \to (⟨A, y⟩ \in F \leftrightarrow x F y)$
13	12	eqcoms	$⊢ x = A \to (⟨A, y⟩ \in F \leftrightarrow x F y)$
14	13	eubidv	$⊢ x = A \to (\exists! y ⟨A, y⟩ \in F \leftrightarrow \exists! y x F y)$
15	14	biimpd	$⊢ x = A \to (\exists! y ⟨A, y⟩ \in F \to \exists! y x F y)$
16	10 15	sylbi	$⊢ x \in \{A\} \to (\exists! y ⟨A, y⟩ \in F \to \exists! y x F y)$
17	16	com12	$⊢ \exists! y ⟨A, y⟩ \in F \to (x \in \{A\} \to \exists! y x F y)$
18	17	adantl	$⊢ (A \in dom F \land \exists! y ⟨A, y⟩ \in F) \to (x \in \{A\} \to \exists! y x F y)$
19	18	ralrimiv	$⊢ (A \in dom F \land \exists! y ⟨A, y⟩ \in F) \to \forall x \in \{A\} \exists! y x F y$
20		fnres	$⊢ ({F ↾}_{\{A\}}) Fn \{A\} \leftrightarrow \forall x \in \{A\} \exists! y x F y$
21		fnfun	$⊢ ({F ↾}_{\{A\}}) Fn \{A\} \to Fun ({F ↾}_{\{A\}})$
22	20 21	sylbir	$⊢ \forall x \in \{A\} \exists! y x F y \to Fun ({F ↾}_{\{A\}})$
23	19 22	syl	$⊢ (A \in dom F \land \exists! y ⟨A, y⟩ \in F) \to Fun ({F ↾}_{\{A\}})$
24	9 23	jca	$⊢ (A \in dom F \land \exists! y ⟨A, y⟩ \in F) \to (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
25	24	ex	$⊢ A \in dom F \to (\exists! y ⟨A, y⟩ \in F \to (A \in dom F \land Fun ({F ↾}_{\{A\}})))$
26	8 25	syl	$⊢ (A \in V \land ⟨A, y⟩ \in F) \to (\exists! y ⟨A, y⟩ \in F \to (A \in dom F \land Fun ({F ↾}_{\{A\}})))$
27	26	impr	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
28		df-dfat	$⊢ F defAt A \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
29	27 28	sylibr	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to F defAt A$
30		dfatafv2iota	$⊢ F defAt A \to (F'''' A) = (ι y \| A F y)$
31	29 30	syl	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to (F'''' A) = (ι y \| A F y)$
32	4	bicomi	$⊢ ⟨A, y⟩ \in F \leftrightarrow A F y$
33	32	eubii	$⊢ \exists! y ⟨A, y⟩ \in F \leftrightarrow \exists! y A F y$
34	33	biimpi	$⊢ \exists! y ⟨A, y⟩ \in F \to \exists! y A F y$
35	5 34	anim12i	$⊢ (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (A F y \land \exists! y A F y)$
36	35	adantl	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to (A F y \land \exists! y A F y)$
37		iota1	$⊢ \exists! y A F y \to (A F y \leftrightarrow (ι y \| A F y) = y)$
38	37	biimpac	$⊢ (A F y \land \exists! y A F y) \to (ι y \| A F y) = y$
39	36 38	syl	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to (ι y \| A F y) = y$
40	31 39	eqtrd	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to (F'''' A) = y$
41	40	ex	$⊢ A \in V \to ((⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (F'''' A) = y)$
42		eu2ndop1stv	$⊢ \exists! y ⟨A, y⟩ \in F \to A \in V$
43	42	pm2.24d	$⊢ \exists! y ⟨A, y⟩ \in F \to (\neg A \in V \to (F'''' A) = y)$
44	43	adantl	$⊢ (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (\neg A \in V \to (F'''' A) = y)$
45	44	com12	$⊢ \neg A \in V \to ((⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (F'''' A) = y)$
46	41 45	pm2.61i	$⊢ (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (F'''' A) = y$

Metamath Proof Explorer

Theorem tz6.12-afv2

Proof