Theorem fin4i

Description: Infer that a set is IV-infinite. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	fin4i	⊢ ( ( 𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴 ) → ¬ 𝐴 ∈ FinIV )

Proof

Step	Hyp	Ref	Expression
1		isfin4	⊢ ( 𝐴 ∈ FinIV → ( 𝐴 ∈ FinIV ↔ ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ) )
2	1	ibi	⊢ ( 𝐴 ∈ FinIV → ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) )
3		relen	⊢ Rel ≈
4	3	brrelex1i	⊢ ( 𝑋 ≈ 𝐴 → 𝑋 ∈ V )
5	4	adantl	⊢ ( ( 𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴 ) → 𝑋 ∈ V )
6		psseq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⊊ 𝐴 ↔ 𝑋 ⊊ 𝐴 ) )
7		breq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≈ 𝐴 ↔ 𝑋 ≈ 𝐴 ) )
8	6 7	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ↔ ( 𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴 ) ) )
9	8	spcegv	⊢ ( 𝑋 ∈ V → ( ( 𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴 ) → ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ) )
10	5 9	mpcom	⊢ ( ( 𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴 ) → ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) )
11	2 10	nsyl3	⊢ ( ( 𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴 ) → ¬ 𝐴 ∈ FinIV )