fundmen

Description: A function is equinumerous to its domain. Exercise 4 of Suppes p. 98. (Contributed by NM, 28-Jul-2004) (Revised by Mario Carneiro, 15-Nov-2014)

		Ref	Expression
	Hypothesis	fundmen.1	$⊢ F \in V$
	Assertion	fundmen	$⊢ Fun F \to dom F \approx F$

Proof

Step	Hyp	Ref	Expression
1		fundmen.1	$⊢ F \in V$
2	1	dmex	$⊢ dom F \in V$
3	2	a1i	$⊢ Fun F \to dom F \in V$
4	1	a1i	$⊢ Fun F \to F \in V$
5		funfvop	$⊢ (Fun F \land x \in dom F) \to ⟨x, F (x)⟩ \in F$
6	5	ex	$⊢ Fun F \to (x \in dom F \to ⟨x, F (x)⟩ \in F)$
7		funrel	$⊢ Fun F \to Rel F$
8		elreldm	$⊢ (Rel F \land y \in F) \to ⋂ ⋂ y \in dom F$
9	8	ex	$⊢ Rel F \to (y \in F \to ⋂ ⋂ y \in dom F)$
10	7 9	syl	$⊢ Fun F \to (y \in F \to ⋂ ⋂ y \in dom F)$
11		df-rel	$⊢ Rel F \leftrightarrow F \subseteq V \times V$
12	7 11	sylib	$⊢ Fun F \to F \subseteq V \times V$
13	12	sselda	$⊢ (Fun F \land y \in F) \to y \in (V \times V)$
14		elvv	$⊢ y \in (V \times V) \leftrightarrow \exists z \exists w y = ⟨z, w⟩$
15	13 14	sylib	$⊢ (Fun F \land y \in F) \to \exists z \exists w y = ⟨z, w⟩$
16		inteq	$⊢ y = ⟨z, w⟩ \to ⋂ y = ⋂ ⟨z, w⟩$
17	16	inteqd	$⊢ y = ⟨z, w⟩ \to ⋂ ⋂ y = ⋂ ⋂ ⟨z, w⟩$
18		vex	$⊢ z \in V$
19		vex	$⊢ w \in V$
20	18 19	op1stb	$⊢ ⋂ ⋂ ⟨z, w⟩ = z$
21	17 20	eqtrdi	$⊢ y = ⟨z, w⟩ \to ⋂ ⋂ y = z$
22		eqeq1	$⊢ x = ⋂ ⋂ y \to (x = z \leftrightarrow ⋂ ⋂ y = z)$
23	21 22	imbitrrid	$⊢ x = ⋂ ⋂ y \to (y = ⟨z, w⟩ \to x = z)$
24		opeq1	$⊢ x = z \to ⟨x, w⟩ = ⟨z, w⟩$
25	23 24	syl6	$⊢ x = ⋂ ⋂ y \to (y = ⟨z, w⟩ \to ⟨x, w⟩ = ⟨z, w⟩)$
26	25	imp	$⊢ (x = ⋂ ⋂ y \land y = ⟨z, w⟩) \to ⟨x, w⟩ = ⟨z, w⟩$
27		eqeq2	$⊢ ⟨x, w⟩ = ⟨z, w⟩ \to (y = ⟨x, w⟩ \leftrightarrow y = ⟨z, w⟩)$
28	27	biimprcd	$⊢ y = ⟨z, w⟩ \to (⟨x, w⟩ = ⟨z, w⟩ \to y = ⟨x, w⟩)$
29	28	adantl	$⊢ (x = ⋂ ⋂ y \land y = ⟨z, w⟩) \to (⟨x, w⟩ = ⟨z, w⟩ \to y = ⟨x, w⟩)$
30	26 29	mpd	$⊢ (x = ⋂ ⋂ y \land y = ⟨z, w⟩) \to y = ⟨x, w⟩$
31	30	ancoms	$⊢ (y = ⟨z, w⟩ \land x = ⋂ ⋂ y) \to y = ⟨x, w⟩$
32	31	adantl	$⊢ ((Fun F \land y \in F) \land (y = ⟨z, w⟩ \land x = ⋂ ⋂ y)) \to y = ⟨x, w⟩$
33	30	eleq1d	$⊢ (x = ⋂ ⋂ y \land y = ⟨z, w⟩) \to (y \in F \leftrightarrow ⟨x, w⟩ \in F)$
34	33	adantl	$⊢ (Fun F \land (x = ⋂ ⋂ y \land y = ⟨z, w⟩)) \to (y \in F \leftrightarrow ⟨x, w⟩ \in F)$
35		funopfv	$⊢ Fun F \to (⟨x, w⟩ \in F \to F (x) = w)$
36	35	adantr	$⊢ (Fun F \land (x = ⋂ ⋂ y \land y = ⟨z, w⟩)) \to (⟨x, w⟩ \in F \to F (x) = w)$
37	34 36	sylbid	$⊢ (Fun F \land (x = ⋂ ⋂ y \land y = ⟨z, w⟩)) \to (y \in F \to F (x) = w)$
38	37	exp32	$⊢ Fun F \to (x = ⋂ ⋂ y \to (y = ⟨z, w⟩ \to (y \in F \to F (x) = w)))$
39	38	com24	$⊢ Fun F \to (y \in F \to (y = ⟨z, w⟩ \to (x = ⋂ ⋂ y \to F (x) = w)))$
40	39	imp43	$⊢ ((Fun F \land y \in F) \land (y = ⟨z, w⟩ \land x = ⋂ ⋂ y)) \to F (x) = w$
41	40	opeq2d	$⊢ ((Fun F \land y \in F) \land (y = ⟨z, w⟩ \land x = ⋂ ⋂ y)) \to ⟨x, F (x)⟩ = ⟨x, w⟩$
42	32 41	eqtr4d	$⊢ ((Fun F \land y \in F) \land (y = ⟨z, w⟩ \land x = ⋂ ⋂ y)) \to y = ⟨x, F (x)⟩$
43	42	exp32	$⊢ (Fun F \land y \in F) \to (y = ⟨z, w⟩ \to (x = ⋂ ⋂ y \to y = ⟨x, F (x)⟩))$
44	43	exlimdvv	$⊢ (Fun F \land y \in F) \to (\exists z \exists w y = ⟨z, w⟩ \to (x = ⋂ ⋂ y \to y = ⟨x, F (x)⟩))$
45	15 44	mpd	$⊢ (Fun F \land y \in F) \to (x = ⋂ ⋂ y \to y = ⟨x, F (x)⟩)$
46	45	adantrl	$⊢ (Fun F \land (x \in dom F \land y \in F)) \to (x = ⋂ ⋂ y \to y = ⟨x, F (x)⟩)$
47		inteq	$⊢ y = ⟨x, F (x)⟩ \to ⋂ y = ⋂ ⟨x, F (x)⟩$
48	47	inteqd	$⊢ y = ⟨x, F (x)⟩ \to ⋂ ⋂ y = ⋂ ⋂ ⟨x, F (x)⟩$
49		vex	$⊢ x \in V$
50		fvex	$⊢ F (x) \in V$
51	49 50	op1stb	$⊢ ⋂ ⋂ ⟨x, F (x)⟩ = x$
52	48 51	eqtr2di	$⊢ y = ⟨x, F (x)⟩ \to x = ⋂ ⋂ y$
53	46 52	impbid1	$⊢ (Fun F \land (x \in dom F \land y \in F)) \to (x = ⋂ ⋂ y \leftrightarrow y = ⟨x, F (x)⟩)$
54	53	ex	$⊢ Fun F \to ((x \in dom F \land y \in F) \to (x = ⋂ ⋂ y \leftrightarrow y = ⟨x, F (x)⟩))$
55	3 4 6 10 54	en3d	$⊢ Fun F \to dom F \approx F$

Metamath Proof Explorer

Theorem fundmen

Proof