Metamath Proof Explorer

Theorem funen1cnv

Description: If a function is equinumerous to ordinal 1, then its converse is also a function. (Contributed by BTernaryTau, 8-Oct-2023)

Ref Expression
Assertion funen1cnv 
|- ( ( Fun F /\ F ~~ 1o ) -> Fun `' F )

Proof

Step Hyp Ref Expression
1 en1 
 |-  ( F ~~ 1o <-> E. p F = { p } )
2 funrel 
 |-  ( Fun { p } -> Rel { p } )
3 vsnid 
 |-  p e. { p }
4 elrel 
 |-  ( ( Rel { p } /\ p e. { p } ) -> E. x E. y p = <. x , y >. )
5 2 3 4 sylancl 
 |-  ( Fun { p } -> E. x E. y p = <. x , y >. )
6 sneq 
 |-  ( p = <. x , y >. -> { p } = { <. x , y >. } )
7 6 2eximi 
 |-  ( E. x E. y p = <. x , y >. -> E. x E. y { p } = { <. x , y >. } )
8 5 7 syl 
 |-  ( Fun { p } -> E. x E. y { p } = { <. x , y >. } )
9 funcnvsn 
 |-  Fun `' { <. x , y >. }
10 9 gen2 
 |-  A. x A. y Fun `' { <. x , y >. }
11 19.29r2 
 |-  ( ( E. x E. y { p } = { <. x , y >. } /\ A. x A. y Fun `' { <. x , y >. } ) -> E. x E. y ( { p } = { <. x , y >. } /\ Fun `' { <. x , y >. } ) )
12 cnveq 
 |-  ( { p } = { <. x , y >. } -> `' { p } = `' { <. x , y >. } )
13 12 funeqd 
 |-  ( { p } = { <. x , y >. } -> ( Fun `' { p } <-> Fun `' { <. x , y >. } ) )
14 13 biimpar 
 |-  ( ( { p } = { <. x , y >. } /\ Fun `' { <. x , y >. } ) -> Fun `' { p } )
15 14 exlimivv 
 |-  ( E. x E. y ( { p } = { <. x , y >. } /\ Fun `' { <. x , y >. } ) -> Fun `' { p } )
16 11 15 syl 
 |-  ( ( E. x E. y { p } = { <. x , y >. } /\ A. x A. y Fun `' { <. x , y >. } ) -> Fun `' { p } )
17 8 10 16 sylancl 
 |-  ( Fun { p } -> Fun `' { p } )
18 17 ax-gen 
 |-  A. p ( Fun { p } -> Fun `' { p } )
19 19.29r 
 |-  ( ( E. p F = { p } /\ A. p ( Fun { p } -> Fun `' { p } ) ) -> E. p ( F = { p } /\ ( Fun { p } -> Fun `' { p } ) ) )
20 funeq 
 |-  ( F = { p } -> ( Fun F <-> Fun { p } ) )
21 cnveq 
 |-  ( F = { p } -> `' F = `' { p } )
22 21 funeqd 
 |-  ( F = { p } -> ( Fun `' F <-> Fun `' { p } ) )
23 20 22 imbi12d 
 |-  ( F = { p } -> ( ( Fun F -> Fun `' F ) <-> ( Fun { p } -> Fun `' { p } ) ) )
24 23 biimpar 
 |-  ( ( F = { p } /\ ( Fun { p } -> Fun `' { p } ) ) -> ( Fun F -> Fun `' F ) )
25 24 exlimiv 
 |-  ( E. p ( F = { p } /\ ( Fun { p } -> Fun `' { p } ) ) -> ( Fun F -> Fun `' F ) )
26 19 25 syl 
 |-  ( ( E. p F = { p } /\ A. p ( Fun { p } -> Fun `' { p } ) ) -> ( Fun F -> Fun `' F ) )
27 18 26 mpan2 
 |-  ( E. p F = { p } -> ( Fun F -> Fun `' F ) )
28 1 27 sylbi 
 |-  ( F ~~ 1o -> ( Fun F -> Fun `' F ) )
29 28 impcom 
 |-  ( ( Fun F /\ F ~~ 1o ) -> Fun `' F )