tz6.12-afv

		Ref	Expression
	Assertion	tz6.12-afv	$⊢ (⟨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		afvfundmfveq	$⊢ F defAt A \to (F''' A) = F (A)$
30	28 29	sylbir	$⊢ (A \in dom F \land Fun ({F ↾}_{\{A\}})) \to (F''' A) = F (A)$
31	27 30	syl	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to (F''' A) = F (A)$
32		tz6.12	$⊢ (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to F (A) = y$
33	32	adantl	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to F (A) = y$
34	31 33	eqtrd	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to (F''' A) = y$
35	34	ex	$⊢ A \in V \to ((⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (F''' A) = y)$
36		eu2ndop1stv	$⊢ \exists! y ⟨A, y⟩ \in F \to A \in V$
37	36	pm2.24d	$⊢ \exists! y ⟨A, y⟩ \in F \to (\neg A \in V \to (F''' A) = y)$
38	37	adantl	$⊢ (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (\neg A \in V \to (F''' A) = y)$
39	38	com12	$⊢ \neg A \in V \to ((⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (F''' A) = y)$
40	35 39	pm2.61i	$⊢ (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (F''' A) = y$

Metamath Proof Explorer

Theorem tz6.12-afv

Proof