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

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 ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 trint ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } Tr 𝑦 → Tr ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
2 vex ⊢ 𝑦 ∈ V
3 sseq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑦 ) )
4 treq ⊢ ( 𝑥 = 𝑦 → ( Tr 𝑥 ↔ Tr 𝑦 ) )
5 3 4 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) ↔ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) ) )
6 2 5 elab ⊢ ( 𝑦 ∈ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ↔ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) )
7 6 simprbi ⊢ ( 𝑦 ∈ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } → Tr 𝑦 )
8 1 7 mprg ⊢ Tr ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) }
9 tcvalg ⊢ ( 𝐴 ∈ V → ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
10 treq ⊢ ( ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } → ( Tr ( TC ‘ 𝐴 ) ↔ Tr ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) )
11 9 10 syl ⊢ ( 𝐴 ∈ V → ( Tr ( TC ‘ 𝐴 ) ↔ Tr ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) )
12 8 11 mpbiri ⊢ ( 𝐴 ∈ V → Tr ( TC ‘ 𝐴 ) )
13 tr0 ⊢ Tr ∅
14 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( TC ‘ 𝐴 ) = ∅ )
15 treq ⊢ ( ( TC ‘ 𝐴 ) = ∅ → ( Tr ( TC ‘ 𝐴 ) ↔ Tr ∅ ) )
16 14 15 syl ⊢ ( ¬ 𝐴 ∈ V → ( Tr ( TC ‘ 𝐴 ) ↔ Tr ∅ ) )
17 13 16 mpbiri ⊢ ( ¬ 𝐴 ∈ V → Tr ( TC ‘ 𝐴 ) )
18 12 17 pm2.61i ⊢ Tr ( TC ‘ 𝐴 )