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⁡xTr⁡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