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

Metamath Proof Explorer

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 ↔ ( 𝐴 = ∅ ∨ 𝐴 ≺ ( 𝐴 ⊔ 𝐴 ) ) )