Theorem tcsni

Description: The transitive closure of a singleton. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015)

	Ref	Expression
Hypothesis	tc2.1	⊢ 𝐴 ∈ V
Assertion	tcsni	⊢ ( TC ‘ { 𝐴 } ) = ( ( TC ‘ 𝐴 ) ∪ { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		tc2.1	⊢ 𝐴 ∈ V
2	1	snss	⊢ ( 𝐴 ∈ 𝑥 ↔ { 𝐴 } ⊆ 𝑥 )
3	2	anbi1i	⊢ ( ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) ↔ ( { 𝐴 } ⊆ 𝑥 ∧ Tr 𝑥 ) )
4	3	abbii	⊢ { 𝑥 ∣ ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) } = { 𝑥 ∣ ( { 𝐴 } ⊆ 𝑥 ∧ Tr 𝑥 ) }
5	4	inteqi	⊢ ∩ { 𝑥 ∣ ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) } = ∩ { 𝑥 ∣ ( { 𝐴 } ⊆ 𝑥 ∧ Tr 𝑥 ) }
6	1	tc2	⊢ ( ( TC ‘ 𝐴 ) ∪ { 𝐴 } ) = ∩ { 𝑥 ∣ ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) }
7		snex	⊢ { 𝐴 } ∈ V
8		tcvalg	⊢ ( { 𝐴 } ∈ V → ( TC ‘ { 𝐴 } ) = ∩ { 𝑥 ∣ ( { 𝐴 } ⊆ 𝑥 ∧ Tr 𝑥 ) } )
9	7 8	ax-mp	⊢ ( TC ‘ { 𝐴 } ) = ∩ { 𝑥 ∣ ( { 𝐴 } ⊆ 𝑥 ∧ Tr 𝑥 ) }
10	5 6 9	3eqtr4ri	⊢ ( TC ‘ { 𝐴 } ) = ( ( TC ‘ 𝐴 ) ∪ { 𝐴 } )