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

Metamath Proof Explorer

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 )