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