Theorem isfin4

Description: Definition of a IV-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	isfin4	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIV ↔ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝐴 ∧ 𝑦 ≈ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psseq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 ⊊ 𝑥 ↔ 𝑦 ⊊ 𝐴 ) )
2		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 ≈ 𝑥 ↔ 𝑦 ≈ 𝐴 ) )
3	1 2	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 ) ↔ ( 𝑦 ⊊ 𝐴 ∧ 𝑦 ≈ 𝐴 ) ) )
4	3	exbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 ) ↔ ∃ 𝑦 ( 𝑦 ⊊ 𝐴 ∧ 𝑦 ≈ 𝐴 ) ) )
5	4	notbid	⊢ ( 𝑥 = 𝐴 → ( ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 ) ↔ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝐴 ∧ 𝑦 ≈ 𝐴 ) ) )
6		df-fin4	⊢ FinIV = { 𝑥 ∣ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 ) }
7	5 6	elab2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIV ↔ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝐴 ∧ 𝑦 ≈ 𝐴 ) ) )