ttcmin

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

		Ref	Expression
	Assertion	ttcmin	Could not format assertion : No typesetting found for \|- ( ( A C_ B /\ Tr B ) -> TC+ A C_ B ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		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 \|-
2		ssel2	$⊢ (A \subseteq B \land x \in A) \to x \in B$
3		rdgfun	$⊢ Fun rec ((y \in V ⟼ ⋃ y), \{x\})$
4		funiunfv	$⊢ Fun rec ((y \in V ⟼ ⋃ y), \{x\}) \to ⋃_{z \in ω} rec ((y \in V ⟼ ⋃ y), \{x\}) (z) = ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω]$
5	3 4	ax-mp	$⊢ ⋃_{z \in ω} rec ((y \in V ⟼ ⋃ y), \{x\}) (z) = ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω]$
6		fveq2	$⊢ z = \emptyset \to rec ((y \in V ⟼ ⋃ y), \{x\}) (z) = rec ((y \in V ⟼ ⋃ y), \{x\}) (\emptyset)$
7	6	sseq1d	$⊢ z = \emptyset \to (rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \subseteq B \leftrightarrow rec ((y \in V ⟼ ⋃ y), \{x\}) (\emptyset) \subseteq B)$
8		fveq2	$⊢ z = w \to rec ((y \in V ⟼ ⋃ y), \{x\}) (z) = rec ((y \in V ⟼ ⋃ y), \{x\}) (w)$
9	8	sseq1d	$⊢ z = w \to (rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \subseteq B \leftrightarrow rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq B)$
10		fveq2	$⊢ z = suc w \to rec ((y \in V ⟼ ⋃ y), \{x\}) (z) = rec ((y \in V ⟼ ⋃ y), \{x\}) (suc w)$
11	10	sseq1d	$⊢ z = suc w \to (rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \subseteq B \leftrightarrow rec ((y \in V ⟼ ⋃ y), \{x\}) (suc w) \subseteq B)$
12		vsnex	$⊢ \{x\} \in V$
13	12	rdg0	$⊢ rec ((y \in V ⟼ ⋃ y), \{x\}) (\emptyset) = \{x\}$
14		snssi	$⊢ x \in B \to \{x\} \subseteq B$
15	13 14	eqsstrid	$⊢ x \in B \to rec ((y \in V ⟼ ⋃ y), \{x\}) (\emptyset) \subseteq B$
16	15	adantr	$⊢ (x \in B \land Tr B) \to rec ((y \in V ⟼ ⋃ y), \{x\}) (\emptyset) \subseteq B$
17		nnon	$⊢ w \in ω \to w \in On$
18		fvex	$⊢ rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \in V$
19	18	uniex	$⊢ ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \in V$
20		eqid	$⊢ rec ((y \in V ⟼ ⋃ y), \{x\}) = rec ((y \in V ⟼ ⋃ y), \{x\})$
21		unieq	$⊢ z = y \to ⋃ z = ⋃ y$
22		unieq	$⊢ z = rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \to ⋃ z = ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (w)$
23	20 21 22	rdgsucmpt2	$⊢ (w \in On \land ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \in V) \to rec ((y \in V ⟼ ⋃ y), \{x\}) (suc w) = ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (w)$
24	17 19 23	sylancl	$⊢ w \in ω \to rec ((y \in V ⟼ ⋃ y), \{x\}) (suc w) = ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (w)$
25	24	3ad2ant1	$⊢ (w \in ω \land (x \in B \land Tr B) \land rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq B) \to rec ((y \in V ⟼ ⋃ y), \{x\}) (suc w) = ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (w)$
26		uniss	$⊢ rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq B \to ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq ⋃ B$
27	26	3ad2ant3	$⊢ (w \in ω \land (x \in B \land Tr B) \land rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq B) \to ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq ⋃ B$
28		simp2r	$⊢ (w \in ω \land (x \in B \land Tr B) \land rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq B) \to Tr B$
29		df-tr	$⊢ Tr B \leftrightarrow ⋃ B \subseteq B$
30	28 29	sylib	$⊢ (w \in ω \land (x \in B \land Tr B) \land rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq B) \to ⋃ B \subseteq B$
31	27 30	sstrd	$⊢ (w \in ω \land (x \in B \land Tr B) \land rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq B) \to ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq B$
32	25 31	eqsstrd	$⊢ (w \in ω \land (x \in B \land Tr B) \land rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq B) \to rec ((y \in V ⟼ ⋃ y), \{x\}) (suc w) \subseteq B$
33	32	3exp	$⊢ w \in ω \to ((x \in B \land Tr B) \to (rec ((y \in V ⟼ ⋃ y), \{x\}) (w) \subseteq B \to rec ((y \in V ⟼ ⋃ y), \{x\}) (suc w) \subseteq B))$
34	7 9 11 16 33	finds2	$⊢ z \in ω \to ((x \in B \land Tr B) \to rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \subseteq B)$
35	34	impcom	$⊢ ((x \in B \land Tr B) \land z \in ω) \to rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \subseteq B$
36	35	iunssd	$⊢ (x \in B \land Tr B) \to ⋃_{z \in ω} rec ((y \in V ⟼ ⋃ y), \{x\}) (z) \subseteq B$
37	5 36	eqsstrrid	$⊢ (x \in B \land Tr B) \to ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \subseteq B$
38	2 37	sylan	$⊢ ((A \subseteq B \land x \in A) \land Tr B) \to ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \subseteq B$
39	38	an32s	$⊢ ((A \subseteq B \land Tr B) \land x \in A) \to ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \subseteq B$
40	39	iunssd	$⊢ (A \subseteq B \land Tr B) \to ⋃_{x \in A} ⋃ rec ((y \in V ⟼ ⋃ y), \{x\}) [ω] \subseteq B$
41	1 40	eqsstrid	Could not format ( ( A C_ B /\ Tr B ) -> TC+ A C_ B ) : No typesetting found for \|- ( ( A C_ B /\ Tr B ) -> TC+ A C_ B ) with typecode \|-

Metamath Proof Explorer

Theorem ttcmin

Proof