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