fv3

Description: Alternate definition of the value of a function. Definition 6.11 of TakeutiZaring p. 26. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	fv3	$⊢ F (A) = \{x \| (\exists y (x \in y \land A F y) \land \exists! y A F y)\}$

Proof

Step	Hyp	Ref	Expression
1		elfv	$⊢ x \in F (A) \leftrightarrow \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z))$
2		biimpr	$⊢ (A F y \leftrightarrow y = z) \to (y = z \to A F y)$
3	2	alimi	$⊢ \forall y (A F y \leftrightarrow y = z) \to \forall y (y = z \to A F y)$
4		breq2	$⊢ y = z \to (A F y \leftrightarrow A F z)$
5	4	equsalvw	$⊢ \forall y (y = z \to A F y) \leftrightarrow A F z$
6	3 5	sylib	$⊢ \forall y (A F y \leftrightarrow y = z) \to A F z$
7	6	anim2i	$⊢ (x \in z \land \forall y (A F y \leftrightarrow y = z)) \to (x \in z \land A F z)$
8	7	eximi	$⊢ \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z)) \to \exists z (x \in z \land A F z)$
9		elequ2	$⊢ z = y \to (x \in z \leftrightarrow x \in y)$
10		breq2	$⊢ z = y \to (A F z \leftrightarrow A F y)$
11	9 10	anbi12d	$⊢ z = y \to ((x \in z \land A F z) \leftrightarrow (x \in y \land A F y))$
12	11	cbvexvw	$⊢ \exists z (x \in z \land A F z) \leftrightarrow \exists y (x \in y \land A F y)$
13	8 12	sylib	$⊢ \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z)) \to \exists y (x \in y \land A F y)$
14		exsimpr	$⊢ \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z)) \to \exists z \forall y (A F y \leftrightarrow y = z)$
15		eu6	$⊢ \exists! y A F y \leftrightarrow \exists z \forall y (A F y \leftrightarrow y = z)$
16	14 15	sylibr	$⊢ \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z)) \to \exists! y A F y$
17	13 16	jca	$⊢ \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z)) \to (\exists y (x \in y \land A F y) \land \exists! y A F y)$
18		nfeu1	$⊢ Ⅎ y \exists! y A F y$
19		nfv	$⊢ Ⅎ y x \in z$
20		nfa1	$⊢ Ⅎ y \forall y (A F y \leftrightarrow y = z)$
21	19 20	nfan	$⊢ Ⅎ y (x \in z \land \forall y (A F y \leftrightarrow y = z))$
22	21	nfex	$⊢ Ⅎ y \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z))$
23	18 22	nfim	$⊢ Ⅎ y (\exists! y A F y \to \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z)))$
24		biimp	$⊢ (A F y \leftrightarrow y = z) \to (A F y \to y = z)$
25		ax9	$⊢ y = z \to (x \in y \to x \in z)$
26	24 25	syl6	$⊢ (A F y \leftrightarrow y = z) \to (A F y \to (x \in y \to x \in z))$
27	26	impcomd	$⊢ (A F y \leftrightarrow y = z) \to ((x \in y \land A F y) \to x \in z)$
28	27	sps	$⊢ \forall y (A F y \leftrightarrow y = z) \to ((x \in y \land A F y) \to x \in z)$
29	28	anc2ri	$⊢ \forall y (A F y \leftrightarrow y = z) \to ((x \in y \land A F y) \to (x \in z \land \forall y (A F y \leftrightarrow y = z)))$
30	29	com12	$⊢ (x \in y \land A F y) \to (\forall y (A F y \leftrightarrow y = z) \to (x \in z \land \forall y (A F y \leftrightarrow y = z)))$
31	30	eximdv	$⊢ (x \in y \land A F y) \to (\exists z \forall y (A F y \leftrightarrow y = z) \to \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z)))$
32	15 31	syl5bi	$⊢ (x \in y \land A F y) \to (\exists! y A F y \to \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z)))$
33	23 32	exlimi	$⊢ \exists y (x \in y \land A F y) \to (\exists! y A F y \to \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z)))$
34	33	imp	$⊢ (\exists y (x \in y \land A F y) \land \exists! y A F y) \to \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z))$
35	17 34	impbii	$⊢ \exists z (x \in z \land \forall y (A F y \leftrightarrow y = z)) \leftrightarrow (\exists y (x \in y \land A F y) \land \exists! y A F y)$
36	1 35	bitri	$⊢ x \in F (A) \leftrightarrow (\exists y (x \in y \land A F y) \land \exists! y A F y)$
37	36	abbi2i	$⊢ F (A) = \{x \| (\exists y (x \in y \land A F y) \land \exists! y A F y)\}$

Metamath Proof Explorer

Theorem fv3

Proof