This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ Fin → ◡ 𝐴 ∈ Fin )

Proof

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