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