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 ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinV ↔ ¬ ( 𝐴 ≠ ∅ ∧ 𝐴 ≈ ( 𝐴 ⊔ 𝐴 ) ) ) )

Proof

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