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

Metamath Proof Explorer

Definition df-lim

Description: Define the limit ordinal predicate, which is true for a nonempty ordinal that is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of BellMachover p. 471 and Exercise 1 of TakeutiZaring p. 42. See dflim2 , dflim3 , and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994)

		Ref	Expression
	Assertion	df-lim	⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	wlim	⊢ Lim 𝐴
2	0	word	⊢ Ord 𝐴
3		c0	⊢ ∅
4	0 3	wne	⊢ 𝐴 ≠ ∅
5	0	cuni	⊢ ∪ 𝐴
6	0 5	wceq	⊢ 𝐴 = ∪ 𝐴
7	2 4 6	w3a	⊢ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 )
8	1 7	wb	⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) )