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	⊢ ( 𝐴 ∈ 𝑉 → ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑦 = 𝐴 → ( TC ‘ 𝑦 ) = ( TC ‘ 𝐴 ) )
2		sseq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥 ) )
3	2	anbi1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) ↔ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) ) )
4	3	abbidv	⊢ ( 𝑦 = 𝐴 → { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } = { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
5	4	inteqd	⊢ ( 𝑦 = 𝐴 → ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
6	1 5	eqeq12d	⊢ ( 𝑦 = 𝐴 → ( ( TC ‘ 𝑦 ) = ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } ↔ ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) )
7		vex	⊢ 𝑦 ∈ V
8	7	tz9.1c	⊢ ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V
9		df-tc	⊢ TC = ( 𝑦 ∈ V ↦ ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
10	9	fvmpt2	⊢ ( ( 𝑦 ∈ V ∧ ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V ) → ( TC ‘ 𝑦 ) = ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
11	7 8 10	mp2an	⊢ ( TC ‘ 𝑦 ) = ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) }
12	6 11	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )