Metamath Proof Explorer

Theorem tcidm

Description: The transitive closure function is idempotent. (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Assertion tcidm ⊢ TC ⁡ TC ⁡ A = TC ⁡ A

Proof

Step Hyp Ref Expression
1 ssid ⊢ TC ⁡ A ⊆ TC ⁡ A
2 tctr ⊢ Tr ⁡ TC ⁡ A
3 fvex ⊢ TC ⁡ A ∈ V
4 tcmin ⊢ TC ⁡ A ∈ V → TC ⁡ A ⊆ TC ⁡ A ∧ Tr ⁡ TC ⁡ A → TC ⁡ TC ⁡ A ⊆ TC ⁡ A
5 3 4 ax-mp ⊢ TC ⁡ A ⊆ TC ⁡ A ∧ Tr ⁡ TC ⁡ A → TC ⁡ TC ⁡ A ⊆ TC ⁡ A
6 1 2 5 mp2an ⊢ TC ⁡ TC ⁡ A ⊆ TC ⁡ A
7 tcid ⊢ TC ⁡ A ∈ V → TC ⁡ A ⊆ TC ⁡ TC ⁡ A
8 3 7 ax-mp ⊢ TC ⁡ A ⊆ TC ⁡ TC ⁡ A
9 6 8 eqssi ⊢ TC ⁡ TC ⁡ A = TC ⁡ A