tcwf

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

		Ref	Expression
	Assertion	tcwf	$⊢ A \in ⋃ R_{1} [On] \to TC (A) \in ⋃ R_{1} [On]$

Step	Hyp	Ref	Expression
1		r1elssi	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq ⋃ R_{1} [On]$
2		dftr3	$⊢ Tr ⋃ R_{1} [On] \leftrightarrow \forall x \in ⋃ R_{1} [On] x \subseteq ⋃ R_{1} [On]$
3		r1elssi	$⊢ x \in ⋃ R_{1} [On] \to x \subseteq ⋃ R_{1} [On]$
4	2 3	mprgbir	$⊢ Tr ⋃ R_{1} [On]$
5		tcmin	$⊢ A \in ⋃ R_{1} [On] \to ((A \subseteq ⋃ R_{1} [On] \land Tr ⋃ R_{1} [On]) \to TC (A) \subseteq ⋃ R_{1} [On])$
6	4 5	mpan2i	$⊢ A \in ⋃ R_{1} [On] \to (A \subseteq ⋃ R_{1} [On] \to TC (A) \subseteq ⋃ R_{1} [On])$
7	1 6	mpd	$⊢ A \in ⋃ R_{1} [On] \to TC (A) \subseteq ⋃ R_{1} [On]$
8		fvex	$⊢ TC (A) \in V$
9	8	r1elss	$⊢ TC (A) \in ⋃ R_{1} [On] \leftrightarrow TC (A) \subseteq ⋃ R_{1} [On]$
10	7 9	sylibr	$⊢ A \in ⋃ R_{1} [On] \to TC (A) \in ⋃ R_{1} [On]$

Metamath Proof Explorer