Theorem 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	⊢ 𝐹 ∈ V
Assertion	fundmen	⊢ ( Fun 𝐹 → dom 𝐹 ≈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fundmen.1	⊢ 𝐹 ∈ V
2	1	dmex	⊢ dom 𝐹 ∈ V
3	2	a1i	⊢ ( Fun 𝐹 → dom 𝐹 ∈ V )
4	1	a1i	⊢ ( Fun 𝐹 → 𝐹 ∈ V )
5		funfvop	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
6	5	ex	⊢ ( Fun 𝐹 → ( 𝑥 ∈ dom 𝐹 → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 ) )
7		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
8		elreldm	⊢ ( ( Rel 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ∩ ∩ 𝑦 ∈ dom 𝐹 )
9	8	ex	⊢ ( Rel 𝐹 → ( 𝑦 ∈ 𝐹 → ∩ ∩ 𝑦 ∈ dom 𝐹 ) )
10	7 9	syl	⊢ ( Fun 𝐹 → ( 𝑦 ∈ 𝐹 → ∩ ∩ 𝑦 ∈ dom 𝐹 ) )
11		df-rel	⊢ ( Rel 𝐹 ↔ 𝐹 ⊆ ( V × V ) )
12	7 11	sylib	⊢ ( Fun 𝐹 → 𝐹 ⊆ ( V × V ) )
13	12	sselda	⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ∈ ( V × V ) )
14		elvv	⊢ ( 𝑦 ∈ ( V × V ) ↔ ∃ 𝑧 ∃ 𝑤 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ )
15	13 14	sylib	⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ∃ 𝑧 ∃ 𝑤 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ )
16		inteq	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ∩ 𝑦 = ∩ ⟨ 𝑧 , 𝑤 ⟩ )
17	16	inteqd	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ∩ ∩ 𝑦 = ∩ ∩ ⟨ 𝑧 , 𝑤 ⟩ )
18		vex	⊢ 𝑧 ∈ V
19		vex	⊢ 𝑤 ∈ V
20	18 19	op1stb	⊢ ∩ ∩ ⟨ 𝑧 , 𝑤 ⟩ = 𝑧
21	17 20	eqtrdi	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ∩ ∩ 𝑦 = 𝑧 )
22		eqeq1	⊢ ( 𝑥 = ∩ ∩ 𝑦 → ( 𝑥 = 𝑧 ↔ ∩ ∩ 𝑦 = 𝑧 ) )
23	21 22	imbitrrid	⊢ ( 𝑥 = ∩ ∩ 𝑦 → ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → 𝑥 = 𝑧 ) )
24		opeq1	⊢ ( 𝑥 = 𝑧 → ⟨ 𝑥 , 𝑤 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
25	23 24	syl6	⊢ ( 𝑥 = ∩ ∩ 𝑦 → ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ⟨ 𝑥 , 𝑤 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ) )
26	25	imp	⊢ ( ( 𝑥 = ∩ ∩ 𝑦 ∧ 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ) → ⟨ 𝑥 , 𝑤 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
27		eqeq2	⊢ ( ⟨ 𝑥 , 𝑤 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑦 = ⟨ 𝑥 , 𝑤 ⟩ ↔ 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ) )
28	27	biimprcd	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( ⟨ 𝑥 , 𝑤 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ → 𝑦 = ⟨ 𝑥 , 𝑤 ⟩ ) )
29	28	adantl	⊢ ( ( 𝑥 = ∩ ∩ 𝑦 ∧ 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ) → ( ⟨ 𝑥 , 𝑤 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ → 𝑦 = ⟨ 𝑥 , 𝑤 ⟩ ) )
30	26 29	mpd	⊢ ( ( 𝑥 = ∩ ∩ 𝑦 ∧ 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ) → 𝑦 = ⟨ 𝑥 , 𝑤 ⟩ )
31	30	ancoms	⊢ ( ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑥 = ∩ ∩ 𝑦 ) → 𝑦 = ⟨ 𝑥 , 𝑤 ⟩ )
32	31	adantl	⊢ ( ( ( Fun 𝐹 ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑥 = ∩ ∩ 𝑦 ) ) → 𝑦 = ⟨ 𝑥 , 𝑤 ⟩ )
33	30	eleq1d	⊢ ( ( 𝑥 = ∩ ∩ 𝑦 ∧ 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ) → ( 𝑦 ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑤 ⟩ ∈ 𝐹 ) )
34	33	adantl	⊢ ( ( Fun 𝐹 ∧ ( 𝑥 = ∩ ∩ 𝑦 ∧ 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ) ) → ( 𝑦 ∈ 𝐹 ↔ ⟨ 𝑥 , 𝑤 ⟩ ∈ 𝐹 ) )
35		funopfv	⊢ ( Fun 𝐹 → ( ⟨ 𝑥 , 𝑤 ⟩ ∈ 𝐹 → ( 𝐹 ‘ 𝑥 ) = 𝑤 ) )
36	35	adantr	⊢ ( ( Fun 𝐹 ∧ ( 𝑥 = ∩ ∩ 𝑦 ∧ 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ) ) → ( ⟨ 𝑥 , 𝑤 ⟩ ∈ 𝐹 → ( 𝐹 ‘ 𝑥 ) = 𝑤 ) )
37	34 36	sylbid	⊢ ( ( Fun 𝐹 ∧ ( 𝑥 = ∩ ∩ 𝑦 ∧ 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ) ) → ( 𝑦 ∈ 𝐹 → ( 𝐹 ‘ 𝑥 ) = 𝑤 ) )
38	37	exp32	⊢ ( Fun 𝐹 → ( 𝑥 = ∩ ∩ 𝑦 → ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑦 ∈ 𝐹 → ( 𝐹 ‘ 𝑥 ) = 𝑤 ) ) ) )
39	38	com24	⊢ ( Fun 𝐹 → ( 𝑦 ∈ 𝐹 → ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑥 = ∩ ∩ 𝑦 → ( 𝐹 ‘ 𝑥 ) = 𝑤 ) ) ) )
40	39	imp43	⊢ ( ( ( Fun 𝐹 ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑥 = ∩ ∩ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑤 )
41	40	opeq2d	⊢ ( ( ( Fun 𝐹 ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑥 = ∩ ∩ 𝑦 ) ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ = ⟨ 𝑥 , 𝑤 ⟩ )
42	32 41	eqtr4d	⊢ ( ( ( Fun 𝐹 ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑥 = ∩ ∩ 𝑦 ) ) → 𝑦 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
43	42	exp32	⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑥 = ∩ ∩ 𝑦 → 𝑦 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ) )
44	43	exlimdvv	⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( ∃ 𝑧 ∃ 𝑤 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑥 = ∩ ∩ 𝑦 → 𝑦 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ) )
45	15 44	mpd	⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 = ∩ ∩ 𝑦 → 𝑦 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
46	45	adantrl	⊢ ( ( Fun 𝐹 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 = ∩ ∩ 𝑦 → 𝑦 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
47		inteq	⊢ ( 𝑦 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ → ∩ 𝑦 = ∩ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
48	47	inteqd	⊢ ( 𝑦 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ → ∩ ∩ 𝑦 = ∩ ∩ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
49		vex	⊢ 𝑥 ∈ V
50		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
51	49 50	op1stb	⊢ ∩ ∩ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ = 𝑥
52	48 51	eqtr2di	⊢ ( 𝑦 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ → 𝑥 = ∩ ∩ 𝑦 )
53	46 52	impbid1	⊢ ( ( Fun 𝐹 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 = ∩ ∩ 𝑦 ↔ 𝑦 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
54	53	ex	⊢ ( Fun 𝐹 → ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 = ∩ ∩ 𝑦 ↔ 𝑦 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ) )
55	3 4 6 10 54	en3d	⊢ ( Fun 𝐹 → dom 𝐹 ≈ 𝐹 )