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

Metamath Proof Explorer

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