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

Metamath Proof Explorer

Definition df-fin5

Description: A set is V-finite iff it behaves finitely under |_| . Definition V of Levy58 p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014)

		Ref	Expression
	Assertion	df-fin5	⊢ Fin^V = { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) }

Step	Hyp	Ref	Expression
0		cfin5	⊢ Fin^V
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3		c0	⊢ ∅
4	2 3	wceq	⊢ 𝑥 = ∅
5		csdm	⊢ ≺
6	2 2	cdju	⊢ ( 𝑥 ⊔ 𝑥 )
7	2 6 5	wbr	⊢ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 )
8	4 7	wo	⊢ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) )
9	8 1	cab	⊢ { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) }
10	0 9	wceq	⊢ Fin^V = { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) }