Theorem isfin5

Description: Definition of a V-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	isfin5	⊢ ( 𝐴 ∈ FinV ↔ ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-fin5	⊢ FinV = { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) }
2	1	eleq2i	⊢ ( 𝐴 ∈ FinV ↔ 𝐴 ∈ { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) } )
3		id	⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
4		0ex	⊢ ∅ ∈ V
5	3 4	eqeltrdi	⊢ ( 𝐴 = ∅ → 𝐴 ∈ V )
6		relsdom	⊢ Rel ≺
7	6	brrelex1i	⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) → 𝐴 ∈ V )
8	5 7	jaoi	⊢ ( ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) → 𝐴 ∈ V )
9		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ∅ ↔ 𝐴 = ∅ ) )
10		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
11		djueq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐴 ) → ( 𝑥 ⊔ 𝑥 ) = ( 𝐴 ⊔ 𝐴 ) )
12	11	anidms	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊔ 𝑥 ) = ( 𝐴 ⊔ 𝐴 ) )
13	10 12	breq12d	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ↔ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) )
14	9 13	orbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) ↔ ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) ) )
15	8 14	elab3	⊢ ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) } ↔ ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) )
16	2 15	bitri	⊢ ( 𝐴 ∈ FinV ↔ ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) )