Theorem tcwf

Description: The transitive closure function is well-founded if its argument is. (Contributed by Mario Carneiro, 23-Jun-2013)

	Ref	Expression
Assertion	tcwf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( TC ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		r1elssi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
2		dftr3	⊢ ( Tr ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑥 ∈ ∪ ( 𝑅1 “ On ) 𝑥 ⊆ ∪ ( 𝑅1 “ On ) )
3		r1elssi	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → 𝑥 ⊆ ∪ ( 𝑅1 “ On ) )
4	2 3	mprgbir	⊢ Tr ∪ ( 𝑅1 “ On )
5		tcmin	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ( 𝐴 ⊆ ∪ ( 𝑅1 “ On ) ∧ Tr ∪ ( 𝑅1 “ On ) ) → ( TC ‘ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) ) )
6	4 5	mpan2i	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ⊆ ∪ ( 𝑅1 “ On ) → ( TC ‘ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) ) )
7	1 6	mpd	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( TC ‘ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) )
8		fvex	⊢ ( TC ‘ 𝐴 ) ∈ V
9	8	r1elss	⊢ ( ( TC ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) ↔ ( TC ‘ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) )
10	7 9	sylibr	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( TC ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) )