Metamath Proof Explorer

Theorem tctr

Description: Defining property of the transitive closure function: it is transitive. (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Assertion tctr ⊢ Tr ⁡ TC ⁡ A

Proof

Step Hyp Ref Expression
1 trint ⊢ ∀ y ∈ x | A ⊆ x ∧ Tr ⁡ x Tr ⁡ y → Tr ⁡ ⋂ x | A ⊆ x ∧ Tr ⁡ x
2 vex ⊢ y ∈ V
3 sseq2 ⊢ x = y → A ⊆ x ↔ A ⊆ y
4 treq ⊢ x = y → Tr ⁡ x ↔ Tr ⁡ y
5 3 4 anbi12d ⊢ x = y → A ⊆ x ∧ Tr ⁡ x ↔ A ⊆ y ∧ Tr ⁡ y
6 2 5 elab ⊢ y ∈ x | A ⊆ x ∧ Tr ⁡ x ↔ A ⊆ y ∧ Tr ⁡ y
7 6 simprbi ⊢ y ∈ x | A ⊆ x ∧ Tr ⁡ x → Tr ⁡ y
8 1 7 mprg ⊢ Tr ⁡ ⋂ x | A ⊆ x ∧ Tr ⁡ x
9 tcvalg ⊢ A ∈ V → TC ⁡ A = ⋂ x | A ⊆ x ∧ Tr ⁡ x
10 treq ⊢ TC ⁡ A = ⋂ x | A ⊆ x ∧ Tr ⁡ x → Tr ⁡ TC ⁡ A ↔ Tr ⁡ ⋂ x | A ⊆ x ∧ Tr ⁡ x
11 9 10 syl ⊢ A ∈ V → Tr ⁡ TC ⁡ A ↔ Tr ⁡ ⋂ x | A ⊆ x ∧ Tr ⁡ x
12 8 11 mpbiri ⊢ A ∈ V → Tr ⁡ TC ⁡ A
13 tr0 ⊢ Tr ⁡ ∅
14 fvprc ⊢ ¬ A ∈ V → TC ⁡ A = ∅
15 treq ⊢ TC ⁡ A = ∅ → Tr ⁡ TC ⁡ A ↔ Tr ⁡ ∅
16 14 15 syl ⊢ ¬ A ∈ V → Tr ⁡ TC ⁡ A ↔ Tr ⁡ ∅
17 13 16 mpbiri ⊢ ¬ A ∈ V → Tr ⁡ TC ⁡ A
18 12 17 pm2.61i ⊢ Tr ⁡ TC ⁡ A