unisucg

Description: A transitive class is equal to the union of its successor, closed form. Combines Theorem 4E of Enderton p. 72 and Exercise 6 of Enderton p. 73. (Contributed by NM, 30-Aug-1993) Generalize from unisuc . (Revised by BJ, 28-Dec-2024)

		Ref	Expression
	Assertion	unisucg	$⊢ A \in V \to (Tr A \leftrightarrow ⋃ suc A = A)$

Proof

Step	Hyp	Ref	Expression
1		ssequn1	$⊢ ⋃ A \subseteq A \leftrightarrow ⋃ A \cup A = A$
2	1	a1i	$⊢ A \in V \to (⋃ A \subseteq A \leftrightarrow ⋃ A \cup A = A)$
3		df-tr	$⊢ Tr A \leftrightarrow ⋃ A \subseteq A$
4	3	a1i	$⊢ A \in V \to (Tr A \leftrightarrow ⋃ A \subseteq A)$
5		unisucs	$⊢ A \in V \to ⋃ suc A = ⋃ A \cup A$
6	5	eqeq1d	$⊢ A \in V \to (⋃ suc A = A \leftrightarrow ⋃ A \cup A = A)$
7	2 4 6	3bitr4d	$⊢ A \in V \to (Tr A \leftrightarrow ⋃ suc A = A)$

Metamath Proof Explorer

Theorem unisucg

Proof