Metamath Proof Explorer

Theorem bnj1147

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	bnj1147	$⊢ trCl (X, A, R) \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		biid	$⊢ f (\emptyset) = pred (X, A, R) \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		biid	$⊢ \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		eqid	$⊢ ω ∖ \{\emptyset\} = ω ∖ \{\emptyset\}$
4		eqid	$⊢ \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} = \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}$
5		biid	$⊢ (n \in (ω ∖ \{\emptyset\}) \land f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))) \leftrightarrow (n \in (ω ∖ \{\emptyset\}) \land f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))$
6		biid	$⊢ ((i \neq \emptyset \land i \in n \land (n \in (ω ∖ \{\emptyset\}) \land f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))) \land (j \in n \land i = suc j)) \leftrightarrow ((i \neq \emptyset \land i \in n \land (n \in (ω ∖ \{\emptyset\}) \land f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))) \land (j \in n \land i = suc j))$
7	1 2 3 4 5 6	bnj1145	$⊢ trCl (X, A, R) \subseteq A$