Metamath Proof Explorer

Theorem cnvfi

Description: If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014) Avoid ax-pow . (Revised by BTernaryTau, 9-Sep-2024)

Ref Expression
Assertion cnvfi 
|- ( A e. Fin -> `' A e. Fin )

Proof

Step Hyp Ref Expression
1 cnveq 
 |-  ( x = (/) -> `' x = `' (/) )
2 1 eleq1d 
 |-  ( x = (/) -> ( `' x e. Fin <-> `' (/) e. Fin ) )
3 cnveq 
 |-  ( x = y -> `' x = `' y )
4 3 eleq1d 
 |-  ( x = y -> ( `' x e. Fin <-> `' y e. Fin ) )
5 cnveq 
 |-  ( x = ( y u. { z } ) -> `' x = `' ( y u. { z } ) )
6 5 eleq1d 
 |-  ( x = ( y u. { z } ) -> ( `' x e. Fin <-> `' ( y u. { z } ) e. Fin ) )
7 cnveq 
 |-  ( x = A -> `' x = `' A )
8 7 eleq1d 
 |-  ( x = A -> ( `' x e. Fin <-> `' A e. Fin ) )
9 cnv0 
 |-  `' (/) = (/)
10 0fin 
 |-  (/) e. Fin
11 9 10 eqeltri 
 |-  `' (/) e. Fin
12 cnvun 
 |-  `' ( y u. { z } ) = ( `' y u. `' { z } )
13 elvv 
 |-  ( z e. ( _V X. _V ) <-> E. u E. v z = <. u , v >. )
14 sneq 
 |-  ( z = <. u , v >. -> { z } = { <. u , v >. } )
15 cnveq 
 |-  ( { z } = { <. u , v >. } -> `' { z } = `' { <. u , v >. } )
16 vex 
 |-  u e. _V
17 vex 
 |-  v e. _V
18 16 17 cnvsn 
 |-  `' { <. u , v >. } = { <. v , u >. }
19 15 18 eqtrdi 
 |-  ( { z } = { <. u , v >. } -> `' { z } = { <. v , u >. } )
20 14 19 syl 
 |-  ( z = <. u , v >. -> `' { z } = { <. v , u >. } )
21 snfi 
 |-  { <. v , u >. } e. Fin
22 20 21 eqeltrdi 
 |-  ( z = <. u , v >. -> `' { z } e. Fin )
23 22 exlimivv 
 |-  ( E. u E. v z = <. u , v >. -> `' { z } e. Fin )
24 13 23 sylbi 
 |-  ( z e. ( _V X. _V ) -> `' { z } e. Fin )
25 dfdm4 
 |-  dom { z } = ran `' { z }
26 dmsnn0 
 |-  ( z e. ( _V X. _V ) <-> dom { z } =/= (/) )
27 26 biimpri 
 |-  ( dom { z } =/= (/) -> z e. ( _V X. _V ) )
28 27 necon1bi 
 |-  ( -. z e. ( _V X. _V ) -> dom { z } = (/) )
29 25 28 eqtr3id 
 |-  ( -. z e. ( _V X. _V ) -> ran `' { z } = (/) )
30 relcnv 
 |-  Rel `' { z }
31 relrn0 
 |-  ( Rel `' { z } -> ( `' { z } = (/) <-> ran `' { z } = (/) ) )
32 30 31 ax-mp 
 |-  ( `' { z } = (/) <-> ran `' { z } = (/) )
33 29 32 sylibr 
 |-  ( -. z e. ( _V X. _V ) -> `' { z } = (/) )
34 33 10 eqeltrdi 
 |-  ( -. z e. ( _V X. _V ) -> `' { z } e. Fin )
35 24 34 pm2.61i 
 |-  `' { z } e. Fin
36 unfi 
 |-  ( ( `' y e. Fin /\ `' { z } e. Fin ) -> ( `' y u. `' { z } ) e. Fin )
37 35 36 mpan2 
 |-  ( `' y e. Fin -> ( `' y u. `' { z } ) e. Fin )
38 12 37 eqeltrid 
 |-  ( `' y e. Fin -> `' ( y u. { z } ) e. Fin )
39 38 a1i 
 |-  ( y e. Fin -> ( `' y e. Fin -> `' ( y u. { z } ) e. Fin ) )
40 2 4 6 8 11 39 findcard2 
 |-  ( A e. Fin -> `' A e. Fin )