dfttc2g

Description: A shorter expression for the transitive closure of a set. (Contributed by Matthew House, 6-Apr-2026)

		Ref	Expression
	Assertion	dfttc2g	Could not format assertion : No typesetting found for \|- ( A e. V -> TC+ A = U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		rdg0g	$⊢ A \in V \to rec ((x \in V ⟼ ⋃ x), A) (\emptyset) = A$
2		rdgfnon	$⊢ rec ((x \in V ⟼ ⋃ x), A) Fn On$
3		omsson	$⊢ ω \subseteq On$
4		peano1	$⊢ \emptyset \in ω$
5		fnfvima	$⊢ (rec ((x \in V ⟼ ⋃ x), A) Fn On \land ω \subseteq On \land \emptyset \in ω) \to rec ((x \in V ⟼ ⋃ x), A) (\emptyset) \in rec ((x \in V ⟼ ⋃ x), A) [ω]$
6	2 3 4 5	mp3an	$⊢ rec ((x \in V ⟼ ⋃ x), A) (\emptyset) \in rec ((x \in V ⟼ ⋃ x), A) [ω]$
7	1 6	eqeltrrdi	$⊢ A \in V \to A \in rec ((x \in V ⟼ ⋃ x), A) [ω]$
8		elssuni	$⊢ A \in rec ((x \in V ⟼ ⋃ x), A) [ω] \to A \subseteq ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω]$
9	7 8	syl	$⊢ A \in V \to A \subseteq ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω]$
10		peano2	$⊢ z \in ω \to suc z \in ω$
11		elunii	$⊢ (w \in y \land y \in rec ((x \in V ⟼ ⋃ x), A) (z)) \to w \in ⋃ rec ((x \in V ⟼ ⋃ x), A) (z)$
12		nnon	$⊢ z \in ω \to z \in On$
13		fvex	$⊢ rec ((x \in V ⟼ ⋃ x), A) (z) \in V$
14	13	uniex	$⊢ ⋃ rec ((x \in V ⟼ ⋃ x), A) (z) \in V$
15		eqid	$⊢ rec ((x \in V ⟼ ⋃ x), A) = rec ((x \in V ⟼ ⋃ x), A)$
16		unieq	$⊢ y = x \to ⋃ y = ⋃ x$
17		unieq	$⊢ y = rec ((x \in V ⟼ ⋃ x), A) (z) \to ⋃ y = ⋃ rec ((x \in V ⟼ ⋃ x), A) (z)$
18	15 16 17	rdgsucmpt2	$⊢ (z \in On \land ⋃ rec ((x \in V ⟼ ⋃ x), A) (z) \in V) \to rec ((x \in V ⟼ ⋃ x), A) (suc z) = ⋃ rec ((x \in V ⟼ ⋃ x), A) (z)$
19	12 14 18	sylancl	$⊢ z \in ω \to rec ((x \in V ⟼ ⋃ x), A) (suc z) = ⋃ rec ((x \in V ⟼ ⋃ x), A) (z)$
20	19	eleq2d	$⊢ z \in ω \to (w \in rec ((x \in V ⟼ ⋃ x), A) (suc z) \leftrightarrow w \in ⋃ rec ((x \in V ⟼ ⋃ x), A) (z))$
21	20	biimpar	$⊢ (z \in ω \land w \in ⋃ rec ((x \in V ⟼ ⋃ x), A) (z)) \to w \in rec ((x \in V ⟼ ⋃ x), A) (suc z)$
22	11 21	sylan2	$⊢ (z \in ω \land (w \in y \land y \in rec ((x \in V ⟼ ⋃ x), A) (z))) \to w \in rec ((x \in V ⟼ ⋃ x), A) (suc z)$
23		fveq2	$⊢ y = suc z \to rec ((x \in V ⟼ ⋃ x), A) (y) = rec ((x \in V ⟼ ⋃ x), A) (suc z)$
24	23	eleq2d	$⊢ y = suc z \to (w \in rec ((x \in V ⟼ ⋃ x), A) (y) \leftrightarrow w \in rec ((x \in V ⟼ ⋃ x), A) (suc z))$
25	24	rspcev	$⊢ (suc z \in ω \land w \in rec ((x \in V ⟼ ⋃ x), A) (suc z)) \to \exists y \in ω w \in rec ((x \in V ⟼ ⋃ x), A) (y)$
26	10 22 25	syl2an2r	$⊢ (z \in ω \land (w \in y \land y \in rec ((x \in V ⟼ ⋃ x), A) (z))) \to \exists y \in ω w \in rec ((x \in V ⟼ ⋃ x), A) (y)$
27	26	an12s	$⊢ (w \in y \land (z \in ω \land y \in rec ((x \in V ⟼ ⋃ x), A) (z))) \to \exists y \in ω w \in rec ((x \in V ⟼ ⋃ x), A) (y)$
28	27	rexlimdvaa	$⊢ w \in y \to (\exists z \in ω y \in rec ((x \in V ⟼ ⋃ x), A) (z) \to \exists y \in ω w \in rec ((x \in V ⟼ ⋃ x), A) (y))$
29		rdgfun	$⊢ Fun rec ((x \in V ⟼ ⋃ x), A)$
30		eluniima	$⊢ Fun rec ((x \in V ⟼ ⋃ x), A) \to (y \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω] \leftrightarrow \exists z \in ω y \in rec ((x \in V ⟼ ⋃ x), A) (z))$
31	29 30	ax-mp	$⊢ y \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω] \leftrightarrow \exists z \in ω y \in rec ((x \in V ⟼ ⋃ x), A) (z)$
32		eluniima	$⊢ Fun rec ((x \in V ⟼ ⋃ x), A) \to (w \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω] \leftrightarrow \exists y \in ω w \in rec ((x \in V ⟼ ⋃ x), A) (y))$
33	29 32	ax-mp	$⊢ w \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω] \leftrightarrow \exists y \in ω w \in rec ((x \in V ⟼ ⋃ x), A) (y)$
34	28 31 33	3imtr4g	$⊢ w \in y \to (y \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω] \to w \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω])$
35	34	imp	$⊢ (w \in y \land y \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω]) \to w \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω]$
36	35	gen2	$⊢ \forall w \forall y ((w \in y \land y \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω]) \to w \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω])$
37		dftr2	$⊢ Tr ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω] \leftrightarrow \forall w \forall y ((w \in y \land y \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω]) \to w \in ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω])$
38	36 37	mpbir	$⊢ Tr ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω]$
39		ttcmin	Could not format ( ( A C_ U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) /\ Tr U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) ) -> TC+ A C_ U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) ) : No typesetting found for \|- ( ( A C_ U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) /\ Tr U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) ) -> TC+ A C_ U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) ) with typecode \|-
40	9 38 39	sylancl	Could not format ( A e. V -> TC+ A C_ U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) ) : No typesetting found for \|- ( A e. V -> TC+ A C_ U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) ) with typecode \|-
41		funiunfv	$⊢ Fun rec ((x \in V ⟼ ⋃ x), A) \to ⋃_{y \in ω} rec ((x \in V ⟼ ⋃ x), A) (y) = ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω]$
42	29 41	ax-mp	$⊢ ⋃_{y \in ω} rec ((x \in V ⟼ ⋃ x), A) (y) = ⋃ rec ((x \in V ⟼ ⋃ x), A) [ω]$
43		fveq2	$⊢ y = \emptyset \to rec ((x \in V ⟼ ⋃ x), A) (y) = rec ((x \in V ⟼ ⋃ x), A) (\emptyset)$
44	43	sseq1d	Could not format ( y = (/) -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A <-> ( rec ( ( x e. _V \|-> U. x ) , A ) ` (/) ) C_ TC+ A ) ) : No typesetting found for \|- ( y = (/) -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A <-> ( rec ( ( x e. _V \|-> U. x ) , A ) ` (/) ) C_ TC+ A ) ) with typecode \|-
45		fveq2	$⊢ y = z \to rec ((x \in V ⟼ ⋃ x), A) (y) = rec ((x \in V ⟼ ⋃ x), A) (z)$
46	45	sseq1d	Could not format ( y = z -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A <-> ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A ) ) : No typesetting found for \|- ( y = z -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A <-> ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A ) ) with typecode \|-
47	23	sseq1d	Could not format ( y = suc z -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A <-> ( rec ( ( x e. _V \|-> U. x ) , A ) ` suc z ) C_ TC+ A ) ) : No typesetting found for \|- ( y = suc z -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A <-> ( rec ( ( x e. _V \|-> U. x ) , A ) ` suc z ) C_ TC+ A ) ) with typecode \|-
48		ttcid	Could not format A C_ TC+ A : No typesetting found for \|- A C_ TC+ A with typecode \|-
49	1 48	eqsstrdi	Could not format ( A e. V -> ( rec ( ( x e. _V \|-> U. x ) , A ) ` (/) ) C_ TC+ A ) : No typesetting found for \|- ( A e. V -> ( rec ( ( x e. _V \|-> U. x ) , A ) ` (/) ) C_ TC+ A ) with typecode \|-
50		uniss	Could not format ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A -> U. ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ U. TC+ A ) : No typesetting found for \|- ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A -> U. ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ U. TC+ A ) with typecode \|-
51		ttctr3	Could not format U. TC+ A C_ TC+ A : No typesetting found for \|- U. TC+ A C_ TC+ A with typecode \|-
52	50 51	sstrdi	Could not format ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A -> U. ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A ) : No typesetting found for \|- ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A -> U. ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A ) with typecode \|-
53	19	sseq1d	Could not format ( z e. _om -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` suc z ) C_ TC+ A <-> U. ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A ) ) : No typesetting found for \|- ( z e. _om -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` suc z ) C_ TC+ A <-> U. ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A ) ) with typecode \|-
54	52 53	imbitrrid	Could not format ( z e. _om -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A -> ( rec ( ( x e. _V \|-> U. x ) , A ) ` suc z ) C_ TC+ A ) ) : No typesetting found for \|- ( z e. _om -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A -> ( rec ( ( x e. _V \|-> U. x ) , A ) ` suc z ) C_ TC+ A ) ) with typecode \|-
55	54	a1d	Could not format ( z e. _om -> ( A e. V -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A -> ( rec ( ( x e. _V \|-> U. x ) , A ) ` suc z ) C_ TC+ A ) ) ) : No typesetting found for \|- ( z e. _om -> ( A e. V -> ( ( rec ( ( x e. _V \|-> U. x ) , A ) ` z ) C_ TC+ A -> ( rec ( ( x e. _V \|-> U. x ) , A ) ` suc z ) C_ TC+ A ) ) ) with typecode \|-
56	44 46 47 49 55	finds2	Could not format ( y e. _om -> ( A e. V -> ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A ) ) : No typesetting found for \|- ( y e. _om -> ( A e. V -> ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A ) ) with typecode \|-
57	56	impcom	Could not format ( ( A e. V /\ y e. _om ) -> ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A ) : No typesetting found for \|- ( ( A e. V /\ y e. _om ) -> ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A ) with typecode \|-
58	57	iunssd	Could not format ( A e. V -> U_ y e. _om ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A ) : No typesetting found for \|- ( A e. V -> U_ y e. _om ( rec ( ( x e. _V \|-> U. x ) , A ) ` y ) C_ TC+ A ) with typecode \|-
59	42 58	eqsstrrid	Could not format ( A e. V -> U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) C_ TC+ A ) : No typesetting found for \|- ( A e. V -> U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) C_ TC+ A ) with typecode \|-
60	40 59	eqssd	Could not format ( A e. V -> TC+ A = U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) ) : No typesetting found for \|- ( A e. V -> TC+ A = U. ( rec ( ( x e. _V \|-> U. x ) , A ) " _om ) ) with typecode \|-

Metamath Proof Explorer

Theorem dfttc2g

Proof