Metamath Proof Explorer

Theorem mofeu

Description: The uniqueness of a function into a set with at most one element. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypotheses mofeu.1 
|- G = ( A X. B )
mofeu.2 
|- ( ph -> ( B = (/) -> A = (/) ) )
mofeu.3 
|- ( ph -> E* x x e. B )
Assertion mofeu 
|- ( ph -> ( F : A --> B <-> F = G ) )

Proof

Step Hyp Ref Expression
1 mofeu.1 
 |-  G = ( A X. B )
2 mofeu.2 
 |-  ( ph -> ( B = (/) -> A = (/) ) )
3 mofeu.3 
 |-  ( ph -> E* x x e. B )
4 2 imp 
 |-  ( ( ph /\ B = (/) ) -> A = (/) )
5 f00 
 |-  ( F : A --> (/) <-> ( F = (/) /\ A = (/) ) )
6 5 rbaib 
 |-  ( A = (/) -> ( F : A --> (/) <-> F = (/) ) )
7 4 6 syl 
 |-  ( ( ph /\ B = (/) ) -> ( F : A --> (/) <-> F = (/) ) )
8 feq3 
 |-  ( B = (/) -> ( F : A --> B <-> F : A --> (/) ) )
9 8 adantl 
 |-  ( ( ph /\ B = (/) ) -> ( F : A --> B <-> F : A --> (/) ) )
10 xpeq2 
 |-  ( B = (/) -> ( A X. B ) = ( A X. (/) ) )
11 xp0 
 |-  ( A X. (/) ) = (/)
12 10 11 eqtrdi 
 |-  ( B = (/) -> ( A X. B ) = (/) )
13 1 12 syl5eq 
 |-  ( B = (/) -> G = (/) )
14 13 adantl 
 |-  ( ( ph /\ B = (/) ) -> G = (/) )
15 14 eqeq2d 
 |-  ( ( ph /\ B = (/) ) -> ( F = G <-> F = (/) ) )
16 7 9 15 3bitr4d 
 |-  ( ( ph /\ B = (/) ) -> ( F : A --> B <-> F = G ) )
17 19.42v 
 |-  ( E. y ( ph /\ B = { y } ) <-> ( ph /\ E. y B = { y } ) )
18 fconst2g 
 |-  ( y e. _V -> ( F : A --> { y } <-> F = ( A X. { y } ) ) )
19 18 elv 
 |-  ( F : A --> { y } <-> F = ( A X. { y } ) )
20 feq3 
 |-  ( B = { y } -> ( F : A --> B <-> F : A --> { y } ) )
21 xpeq2 
 |-  ( B = { y } -> ( A X. B ) = ( A X. { y } ) )
22 21 eqeq2d 
 |-  ( B = { y } -> ( F = ( A X. B ) <-> F = ( A X. { y } ) ) )
23 20 22 bibi12d 
 |-  ( B = { y } -> ( ( F : A --> B <-> F = ( A X. B ) ) <-> ( F : A --> { y } <-> F = ( A X. { y } ) ) ) )
24 19 23 mpbiri 
 |-  ( B = { y } -> ( F : A --> B <-> F = ( A X. B ) ) )
25 1 eqeq2i 
 |-  ( F = G <-> F = ( A X. B ) )
26 24 25 bitr4di 
 |-  ( B = { y } -> ( F : A --> B <-> F = G ) )
27 26 adantl 
 |-  ( ( ph /\ B = { y } ) -> ( F : A --> B <-> F = G ) )
28 27 exlimiv 
 |-  ( E. y ( ph /\ B = { y } ) -> ( F : A --> B <-> F = G ) )
29 17 28 sylbir 
 |-  ( ( ph /\ E. y B = { y } ) -> ( F : A --> B <-> F = G ) )
30 mo0sn 
 |-  ( E* x x e. B <-> ( B = (/) \/ E. y B = { y } ) )
31 3 30 sylib 
 |-  ( ph -> ( B = (/) \/ E. y B = { y } ) )
32 16 29 31 mpjaodan 
 |-  ( ph -> ( F : A --> B <-> F = G ) )