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

Metamath Proof Explorer

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 ‘ 𝐴 ) ∪ { 𝐴 } )