Metamath Proof Explorer


Theorem fsn

Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003)

Ref Expression
Hypotheses fsn.1 A V
fsn.2 B V
Assertion fsn F : A B F = A B

Proof

Step Hyp Ref Expression
1 fsn.1 A V
2 fsn.2 B V
3 opelf F : A B x y F x A y B
4 velsn x A x = A
5 velsn y B y = B
6 4 5 anbi12i x A y B x = A y = B
7 3 6 sylib F : A B x y F x = A y = B
8 7 ex F : A B x y F x = A y = B
9 1 snid A A
10 feu F : A B A A ∃! y B A y F
11 9 10 mpan2 F : A B ∃! y B A y F
12 5 anbi1i y B A y F y = B A y F
13 opeq2 y = B A y = A B
14 13 eleq1d y = B A y F A B F
15 14 pm5.32i y = B A y F y = B A B F
16 15 biancomi y = B A y F A B F y = B
17 12 16 bitr2i A B F y = B y B A y F
18 17 eubii ∃! y A B F y = B ∃! y y B A y F
19 2 eueqi ∃! y y = B
20 19 biantru A B F A B F ∃! y y = B
21 euanv ∃! y A B F y = B A B F ∃! y y = B
22 20 21 bitr4i A B F ∃! y A B F y = B
23 df-reu ∃! y B A y F ∃! y y B A y F
24 18 22 23 3bitr4i A B F ∃! y B A y F
25 11 24 sylibr F : A B A B F
26 opeq12 x = A y = B x y = A B
27 26 eleq1d x = A y = B x y F A B F
28 25 27 syl5ibrcom F : A B x = A y = B x y F
29 8 28 impbid F : A B x y F x = A y = B
30 opex x y V
31 30 elsn x y A B x y = A B
32 1 2 opth2 x y = A B x = A y = B
33 31 32 bitr2i x = A y = B x y A B
34 29 33 syl6bb F : A B x y F x y A B
35 34 alrimivv F : A B x y x y F x y A B
36 frel F : A B Rel F
37 1 2 relsnop Rel A B
38 eqrel Rel F Rel A B F = A B x y x y F x y A B
39 36 37 38 sylancl F : A B F = A B x y x y F x y A B
40 35 39 mpbird F : A B F = A B
41 1 2 f1osn A B : A 1-1 onto B
42 f1oeq1 F = A B F : A 1-1 onto B A B : A 1-1 onto B
43 41 42 mpbiri F = A B F : A 1-1 onto B
44 f1of F : A 1-1 onto B F : A B
45 43 44 syl F = A B F : A B
46 40 45 impbii F : A B F = A B