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

Metamath Proof Explorer

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 ∨ 𝐴 ≺ ( 𝐴 × 𝐴 ) ) )