Theorem isfin6

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

	Ref	Expression
Assertion	isfin6	⊢ ( 𝐴 ∈ FinVI ↔ ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-fin6	⊢ FinVI = { 𝑥 ∣ ( 𝑥 ≺ 2o ∨ 𝑥 ≺ ( 𝑥 × 𝑥 ) ) }
2	1	eleq2i	⊢ ( 𝐴 ∈ FinVI ↔ 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ≺ 2o ∨ 𝑥 ≺ ( 𝑥 × 𝑥 ) ) } )
3		relsdom	⊢ Rel ≺
4	3	brrelex1i	⊢ ( 𝐴 ≺ 2o → 𝐴 ∈ V )
5	3	brrelex1i	⊢ ( 𝐴 ≺ ( 𝐴 × 𝐴 ) → 𝐴 ∈ V )
6	4 5	jaoi	⊢ ( ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) → 𝐴 ∈ V )
7		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≺ 2o ↔ 𝐴 ≺ 2o ) )
8		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
9	8	sqxpeqd	⊢ ( 𝑥 = 𝐴 → ( 𝑥 × 𝑥 ) = ( 𝐴 × 𝐴 ) )
10	8 9	breq12d	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≺ ( 𝑥 × 𝑥 ) ↔ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )
11	7 10	orbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≺ 2o ∨ 𝑥 ≺ ( 𝑥 × 𝑥 ) ) ↔ ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) ) )
12	6 11	elab3	⊢ ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ≺ 2o ∨ 𝑥 ≺ ( 𝑥 × 𝑥 ) ) } ↔ ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )
13	2 12	bitri	⊢ ( 𝐴 ∈ FinVI ↔ ( 𝐴 ≺ 2o ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )