Theorem isfi

Description: Express " A is finite." Definition 10.29 of TakeutiZaring p. 91 (whose " Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008)

	Ref	Expression
Assertion	isfi	⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		df-fin	⊢ Fin = { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 }
2	1	eleq2i	⊢ ( 𝐴 ∈ Fin ↔ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 } )
3		relen	⊢ Rel ≈
4	3	brrelex1i	⊢ ( 𝐴 ≈ 𝑥 → 𝐴 ∈ V )
5	4	rexlimivw	⊢ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → 𝐴 ∈ V )
6		breq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≈ 𝑥 ↔ 𝐴 ≈ 𝑥 ) )
7	6	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ) )
8	5 7	elab3	⊢ ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 } ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
9	2 8	bitri	⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )