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

Metamath Proof Explorer

Theorem isfin5-2

Description: Alternate definition of V-finite which emphasizes the idempotent behavior of V-infinite sets. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion isfin5-2 ⊢ A ∈ V → A ∈ FinV ↔ ¬ A ≠ ∅ ∧ A ≈ A ⊔︀ A

Proof

Step Hyp Ref Expression
1 nne ⊢ ¬ A ≠ ∅ ↔ A = ∅
2 1 bicomi ⊢ A = ∅ ↔ ¬ A ≠ ∅
3 2 a1i ⊢ A ∈ V → A = ∅ ↔ ¬ A ≠ ∅
4 djudoml ⊢ A ∈ V ∧ A ∈ V → A ≼ A ⊔︀ A
5 4 anidms ⊢ A ∈ V → A ≼ A ⊔︀ A
6 brsdom ⊢ A ≺ A ⊔︀ A ↔ A ≼ A ⊔︀ A ∧ ¬ A ≈ A ⊔︀ A
7 6 baib ⊢ A ≼ A ⊔︀ A → A ≺ A ⊔︀ A ↔ ¬ A ≈ A ⊔︀ A
8 5 7 syl ⊢ A ∈ V → A ≺ A ⊔︀ A ↔ ¬ A ≈ A ⊔︀ A
9 3 8 orbi12d ⊢ A ∈ V → A = ∅ ∨ A ≺ A ⊔︀ A ↔ ¬ A ≠ ∅ ∨ ¬ A ≈ A ⊔︀ A
10 isfin5 ⊢ A ∈ FinV ↔ A = ∅ ∨ A ≺ A ⊔︀ A
11 ianor ⊢ ¬ A ≠ ∅ ∧ A ≈ A ⊔︀ A ↔ ¬ A ≠ ∅ ∨ ¬ A ≈ A ⊔︀ A
12 9 10 11 3bitr4g ⊢ A ∈ V → A ∈ FinV ↔ ¬ A ≠ ∅ ∧ A ≈ A ⊔︀ A