Theorem tc00

Description: The transitive closure is empty iff its argument is. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015)

	Ref	Expression
Assertion	tc00	⊢ ( 𝐴 ∈ 𝑉 → ( ( TC ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		tcid	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( TC ‘ 𝐴 ) )
2		sseq0	⊢ ( ( 𝐴 ⊆ ( TC ‘ 𝐴 ) ∧ ( TC ‘ 𝐴 ) = ∅ ) → 𝐴 = ∅ )
3	2	ex	⊢ ( 𝐴 ⊆ ( TC ‘ 𝐴 ) → ( ( TC ‘ 𝐴 ) = ∅ → 𝐴 = ∅ ) )
4	1 3	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ( TC ‘ 𝐴 ) = ∅ → 𝐴 = ∅ ) )
5		fveq2	⊢ ( 𝐴 = ∅ → ( TC ‘ 𝐴 ) = ( TC ‘ ∅ ) )
6		tc0	⊢ ( TC ‘ ∅ ) = ∅
7	5 6	eqtrdi	⊢ ( 𝐴 = ∅ → ( TC ‘ 𝐴 ) = ∅ )
8	4 7	impbid1	⊢ ( 𝐴 ∈ 𝑉 → ( ( TC ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )