ttctr

Description: The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026)

		Ref	Expression
	Assertion	ttctr	Could not format assertion : No typesetting found for \|- Tr TC+ A with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		rdgfun	$⊢ Fun rec ((y \in V ⟼ ⋃ y), \{x\})$
2		eluniima	$⊢ Fun rec ((y \in V ⟼ ⋃ y), \{x\}) \to (v \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \leftrightarrow \exists z \in ω v \in rec ((y \in V ⟼ ⋃ y), \{x\}) (z))$
3	1 2	ax-mp	$⊢ v \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \leftrightarrow \exists z \in ω v \in rec ((y \in V ⟼ ⋃ y), \{x\}) (z)$
4		peano2	$⊢ z \in ω \to suc z \in ω$
5		elunii	$⊢ (u \in v \land v \in rec ((y \in V ⟼ ⋃ y), \{x\}) (z)) \to u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (z)$
6		nnon	$⊢ z \in ω \to z \in On$
7		fvex	$⊢ rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \in V$
8	7	uniex	$⊢ ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \in V$
9		eqid	$⊢ rec ((y \in V ⟼ ⋃ y), \{x\}) = rec ((y \in V ⟼ ⋃ y), \{x\})$
10		unieq	$⊢ w = y \to ⋃ w = ⋃ y$
11		unieq	$⊢ w = rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \to ⋃ w = ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (z)$
12	9 10 11	rdgsucmpt2	$⊢ (z \in On \land ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \in V) \to rec ((y \in V ⟼ ⋃ y), \{x\}) (suc z) = ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (z)$
13	6 8 12	sylancl	$⊢ z \in ω \to rec ((y \in V ⟼ ⋃ y), \{x\}) (suc z) = ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (z)$
14	13	eleq2d	$⊢ z \in ω \to (u \in rec ((y \in V ⟼ ⋃ y), \{x\}) (suc z) \leftrightarrow u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (z))$
15	14	biimpar	$⊢ (z \in ω \land u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (z)) \to u \in rec ((y \in V ⟼ ⋃ y), \{x\}) (suc z)$
16	5 15	sylan2	$⊢ (z \in ω \land (u \in v \land v \in rec ((y \in V ⟼ ⋃ y), \{x\}) (z))) \to u \in rec ((y \in V ⟼ ⋃ y), \{x\}) (suc z)$
17		fveq2	$⊢ w = suc z \to rec ((y \in V ⟼ ⋃ y), \{x\}) (w) = rec ((y \in V ⟼ ⋃ y), \{x\}) (suc z)$
18	17	eleq2d	$⊢ w = suc z \to (u \in rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \leftrightarrow u \in rec ((y \in V ⟼ ⋃ y), \{x\}) (suc z))$
19	18	rspcev	$⊢ (suc z \in ω \land u \in rec ((y \in V ⟼ ⋃ y), \{x\}) (suc z)) \to \exists w \in ω u \in rec ((y \in V ⟼ ⋃ y), \{x\}) (w)$
20	4 16 19	syl2an2r	$⊢ (z \in ω \land (u \in v \land v \in rec ((y \in V ⟼ ⋃ y), \{x\}) (z))) \to \exists w \in ω u \in rec ((y \in V ⟼ ⋃ y), \{x\}) (w)$
21		eluniima	$⊢ Fun rec ((y \in V ⟼ ⋃ y), \{x\}) \to (u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \leftrightarrow \exists w \in ω u \in rec ((y \in V ⟼ ⋃ y), \{x\}) (w))$
22	1 21	ax-mp	$⊢ u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \leftrightarrow \exists w \in ω u \in rec ((y \in V ⟼ ⋃ y), \{x\}) (w)$
23	20 22	sylibr	$⊢ (z \in ω \land (u \in v \land v \in rec ((y \in V ⟼ ⋃ y), \{x\}) (z))) \to u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω]$
24	23	an12s	$⊢ (u \in v \land (z \in ω \land v \in rec ((y \in V ⟼ ⋃ y), \{x\}) (z))) \to u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω]$
25	24	rexlimdvaa	$⊢ u \in v \to (\exists z \in ω v \in rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \to u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω])$
26	3 25	biimtrid	$⊢ u \in v \to (v \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \to u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω])$
27	26	reximdv	$⊢ u \in v \to (\exists x \in A v \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \to \exists x \in A u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω])$
28		eliun	$⊢ v \in ⋃_{x \in A} ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \leftrightarrow \exists x \in A v \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω]$
29		eliun	$⊢ u \in ⋃_{x \in A} ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \leftrightarrow \exists x \in A u \in ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω]$
30	27 28 29	3imtr4g	$⊢ u \in v \to (v \in ⋃_{x \in A} ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \to u \in ⋃_{x \in A} ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω])$
31		df-ttc	Could not format TC+ A = U_ x e. A U. ( rec ( ( y e. _V \|-> U. y ) , { x } ) " _om ) : No typesetting found for \|- TC+ A = U_ x e. A U. ( rec ( ( y e. _V \|-> U. y ) , { x } ) " _om ) with typecode \|-
32	31	eleq2i	Could not format ( v e. TC+ A <-> v e. U_ x e. A U. ( rec ( ( y e. _V \|-> U. y ) , { x } ) " _om ) ) : No typesetting found for \|- ( v e. TC+ A <-> v e. U_ x e. A U. ( rec ( ( y e. _V \|-> U. y ) , { x } ) " _om ) ) with typecode \|-
33	31	eleq2i	Could not format ( u e. TC+ A <-> u e. U_ x e. A U. ( rec ( ( y e. _V \|-> U. y ) , { x } ) " _om ) ) : No typesetting found for \|- ( u e. TC+ A <-> u e. U_ x e. A U. ( rec ( ( y e. _V \|-> U. y ) , { x } ) " _om ) ) with typecode \|-
34	30 32 33	3imtr4g	Could not format ( u e. v -> ( v e. TC+ A -> u e. TC+ A ) ) : No typesetting found for \|- ( u e. v -> ( v e. TC+ A -> u e. TC+ A ) ) with typecode \|-
35	34	imp	Could not format ( ( u e. v /\ v e. TC+ A ) -> u e. TC+ A ) : No typesetting found for \|- ( ( u e. v /\ v e. TC+ A ) -> u e. TC+ A ) with typecode \|-
36	35	gen2	Could not format A. u A. v ( ( u e. v /\ v e. TC+ A ) -> u e. TC+ A ) : No typesetting found for \|- A. u A. v ( ( u e. v /\ v e. TC+ A ) -> u e. TC+ A ) with typecode \|-
37		dftr2	Could not format ( Tr TC+ A <-> A. u A. v ( ( u e. v /\ v e. TC+ A ) -> u e. TC+ A ) ) : No typesetting found for \|- ( Tr TC+ A <-> A. u A. v ( ( u e. v /\ v e. TC+ A ) -> u e. TC+ A ) ) with typecode \|-
38	36 37	mpbir	Could not format Tr TC+ A : No typesetting found for \|- Tr TC+ A with typecode \|-

Metamath Proof Explorer

Theorem ttctr

Proof