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	bilanri	$⊢ (A \in V \land ⟨A, y⟩ \in F) \to A F y$
6		breldmg	$⊢ (A \in V \land y \in V \land A F y) \to A \in dom F$
7	1 3 5 6	syl3anc	$⊢ (A \in V \land ⟨A, y⟩ \in F) \to A \in dom F$
8		simpl	$⊢ (A \in dom F \land \exists! y ⟨A, y⟩ \in F) \to A \in dom F$
9		velsn	$⊢ x \in \{A\} \leftrightarrow x = A$
10		breq1	$⊢ A = x \to (A F y \leftrightarrow x F y)$
11	4 10	bitr3id	$⊢ A = x \to (⟨A, y⟩ \in F \leftrightarrow x F y)$
12	11	eqcoms	$⊢ x = A \to (⟨A, y⟩ \in F \leftrightarrow x F y)$
13	12	eubidv	$⊢ x = A \to (\exists! y ⟨A, y⟩ \in F \leftrightarrow \exists! y x F y)$
14	13	biimpd	$⊢ x = A \to (\exists! y ⟨A, y⟩ \in F \to \exists! y x F y)$
15	9 14	sylbi	$⊢ x \in \{A\} \to (\exists! y ⟨A, y⟩ \in F \to \exists! y x F y)$
16	15	com12	$⊢ \exists! y ⟨A, y⟩ \in F \to (x \in \{A\} \to \exists! y x F y)$
17	16	adantl	$⊢ (A \in dom F \land \exists! y ⟨A, y⟩ \in F) \to (x \in \{A\} \to \exists! y x F y)$
18	17	ralrimiv	$⊢ (A \in dom F \land \exists! y ⟨A, y⟩ \in F) \to \forall x \in \{A\} \exists! y x F y$
19		fnres	$⊢ ({F ↾}_{\{A\}}) Fn \{A\} \leftrightarrow \forall x \in \{A\} \exists! y x F y$
20		fnfun	$⊢ ({F ↾}_{\{A\}}) Fn \{A\} \to Fun ({F ↾}_{\{A\}})$
21	19 20	sylbir	$⊢ \forall x \in \{A\} \exists! y x F y \to Fun ({F ↾}_{\{A\}})$
22	18 21	syl	$⊢ (A \in dom F \land \exists! y ⟨A, y⟩ \in F) \to Fun ({F ↾}_{\{A\}})$
23	8 22	jca	$⊢ (A \in dom F \land \exists! y ⟨A, y⟩ \in F) \to (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
24	23	ex	$⊢ A \in dom F \to (\exists! y ⟨A, y⟩ \in F \to (A \in dom F \land Fun ({F ↾}_{\{A\}})))$
25	7 24	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\}})))$
26	25	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\}}))$
27		df-dfat	$⊢ F defAt A \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
28		afvfundmfveq	$⊢ F defAt A \to (F''' A) = F (A)$
29	27 28	sylbir	$⊢ (A \in dom F \land Fun ({F ↾}_{\{A\}})) \to (F''' A) = F (A)$
30	26 29	syl	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to (F''' A) = F (A)$
31		tz6.12	$⊢ (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to F (A) = y$
32	31	adantl	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to F (A) = y$
33	30 32	eqtrd	$⊢ (A \in V \land (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F)) \to (F''' A) = y$
34	33	ex	$⊢ A \in V \to ((⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (F''' A) = y)$
35		eu2ndop1stv	$⊢ \exists! y ⟨A, y⟩ \in F \to A \in V$
36	35	pm2.24d	$⊢ \exists! y ⟨A, y⟩ \in F \to (\neg A \in V \to (F''' A) = y)$
37	36	adantl	$⊢ (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (\neg A \in V \to (F''' A) = y)$
38	37	com12	$⊢ \neg A \in V \to ((⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to (F''' A) = y)$
39	34 38	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