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 ∈ Fin → A -1 ∈ Fin

Proof

Step Hyp Ref Expression
1 cnveq ⊢ x = ∅ → x -1 = ∅ -1
2 1 eleq1d ⊢ x = ∅ → x -1 ∈ Fin ↔ ∅ -1 ∈ Fin
3 cnveq ⊢ x = y → x -1 = y -1
4 3 eleq1d ⊢ x = y → x -1 ∈ Fin ↔ y -1 ∈ Fin
5 cnveq ⊢ x = y ∪ z → x -1 = y ∪ z -1
6 5 eleq1d ⊢ x = y ∪ z → x -1 ∈ Fin ↔ y ∪ z -1 ∈ Fin
7 cnveq ⊢ x = A → x -1 = A -1
8 7 eleq1d ⊢ x = A → x -1 ∈ Fin ↔ A -1 ∈ Fin
9 cnv0 ⊢ ∅ -1 = ∅
10 0fi ⊢ ∅ ∈ Fin
11 9 10 eqeltri ⊢ ∅ -1 ∈ Fin
12 cnvun ⊢ y ∪ z -1 = y -1 ∪ z -1
13 elvv ⊢ z ∈ V × V ↔ ∃ u ∃ v z = u v
14 sneq ⊢ z = u v → z = u v
15 cnveq ⊢ z = u v → z -1 = u v -1
16 vex ⊢ u ∈ V
17 vex ⊢ v ∈ V
18 16 17 cnvsn ⊢ u v -1 = v u
19 15 18 eqtrdi ⊢ z = u v → z -1 = v u
20 14 19 syl ⊢ z = u v → z -1 = v u
21 snfi ⊢ v u ∈ Fin
22 20 21 eqeltrdi ⊢ z = u v → z -1 ∈ Fin
23 22 exlimivv ⊢ ∃ u ∃ v z = u v → z -1 ∈ Fin
24 13 23 sylbi ⊢ z ∈ V × V → z -1 ∈ Fin
25 dfdm4 ⊢ dom ⁡ z = ran ⁡ z -1
26 dmsnn0 ⊢ z ∈ V × V ↔ dom ⁡ z ≠ ∅
27 26 biimpri ⊢ dom ⁡ z ≠ ∅ → z ∈ V × V
28 27 necon1bi ⊢ ¬ z ∈ V × V → dom ⁡ z = ∅
29 25 28 eqtr3id ⊢ ¬ z ∈ V × V → ran ⁡ z -1 = ∅
30 relcnv ⊢ Rel ⁡ z -1
31 relrn0 ⊢ Rel ⁡ z -1 → z -1 = ∅ ↔ ran ⁡ z -1 = ∅
32 30 31 ax-mp ⊢ z -1 = ∅ ↔ ran ⁡ z -1 = ∅
33 29 32 sylibr ⊢ ¬ z ∈ V × V → z -1 = ∅
34 33 10 eqeltrdi ⊢ ¬ z ∈ V × V → z -1 ∈ Fin
35 24 34 pm2.61i ⊢ z -1 ∈ Fin
36 unfi ⊢ y -1 ∈ Fin ∧ z -1 ∈ Fin → y -1 ∪ z -1 ∈ Fin
37 35 36 mpan2 ⊢ y -1 ∈ Fin → y -1 ∪ z -1 ∈ Fin
38 12 37 eqeltrid ⊢ y -1 ∈ Fin → y ∪ z -1 ∈ Fin
39 38 a1i ⊢ y ∈ Fin → y -1 ∈ Fin → y ∪ z -1 ∈ Fin
40 2 4 6 8 11 39 findcard2 ⊢ A ∈ Fin → A -1 ∈ Fin