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 )