Metamath Proof Explorer


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 syl5ibr ( 𝑥 = 𝑦 → ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → 𝑥 = 𝑧 ) )
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 𝐹𝐹 )