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 ⊢ A ∈ V
Assertion tcsni ⊢ TC ⁡ A = TC ⁡ A ∪ A

Proof

Step Hyp Ref Expression
1 tc2.1 ⊢ A ∈ V
2 1 snss ⊢ A ∈ x ↔ A ⊆ x
3 2 anbi1i ⊢ A ∈ x ∧ Tr ⁡ x ↔ A ⊆ x ∧ Tr ⁡ x
4 3 abbii ⊢ x | A ∈ x ∧ Tr ⁡ x = x | A ⊆ x ∧ Tr ⁡ x
5 4 inteqi ⊢ ⋂ x | A ∈ x ∧ Tr ⁡ x = ⋂ x | A ⊆ x ∧ Tr ⁡ x
6 1 tc2 ⊢ TC ⁡ A ∪ A = ⋂ x | A ∈ x ∧ Tr ⁡ x
7 snex ⊢ A ∈ V
8 tcvalg ⊢ A ∈ V → TC ⁡ A = ⋂ x | A ⊆ x ∧ Tr ⁡ x
9 7 8 ax-mp ⊢ TC ⁡ A = ⋂ x | A ⊆ x ∧ Tr ⁡ x
10 5 6 9 3eqtr4ri ⊢ TC ⁡ A = TC ⁡ A ∪ A