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

Metamath Proof Explorer

Theorem tcvalg

Description: Value of the transitive closure function. (The fact that this intersection exists is a non-trivial fact that depends on ax-inf ; see tz9.1 .) (Contributed by Mario Carneiro, 23-Jun-2013)

		Ref	Expression
	Assertion	tcvalg	$⊢ A \in V \to TC (A) = ⋂ \{x \| (A \subseteq x \land Tr x)\}$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ y = A \to TC (y) = TC (A)$
2		sseq1	$⊢ y = A \to (y \subseteq x \leftrightarrow A \subseteq x)$
3	2	anbi1d	$⊢ y = A \to ((y \subseteq x \land Tr x) \leftrightarrow (A \subseteq x \land Tr x))$
4	3	abbidv	$⊢ y = A \to \{x \| (y \subseteq x \land Tr x)\} = \{x \| (A \subseteq x \land Tr x)\}$
5	4	inteqd	$⊢ y = A \to ⋂ \{x \| (y \subseteq x \land Tr x)\} = ⋂ \{x \| (A \subseteq x \land Tr x)\}$
6	1 5	eqeq12d	$⊢ y = A \to (TC (y) = ⋂ \{x \| (y \subseteq x \land Tr x)\} \leftrightarrow TC (A) = ⋂ \{x \| (A \subseteq x \land Tr x)\})$
7		vex	$⊢ y \in V$
8	7	tz9.1c	$⊢ ⋂ \{x \| (y \subseteq x \land Tr x)\} \in V$
9		df-tc	$⊢ TC = (y \in V ⟼ ⋂ \{x \| (y \subseteq x \land Tr x)\})$
10	9	fvmpt2	$⊢ (y \in V \land ⋂ \{x \| (y \subseteq x \land Tr x)\} \in V) \to TC (y) = ⋂ \{x \| (y \subseteq x \land Tr x)\}$
11	7 8 10	mp2an	$⊢ TC (y) = ⋂ \{x \| (y \subseteq x \land Tr x)\}$
12	6 11	vtoclg	$⊢ A \in V \to TC (A) = ⋂ \{x \| (A \subseteq x \land Tr x)\}$