Metamath Proof Explorer

Theorem bnj1127

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

		Ref	Expression
	Assertion	bnj1127	$⊢ Y \in trCl (X, A, R) \to Y \in 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	$⊢ ((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))) \to f (i) \subseteq A) \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))) \to f (i) \subseteq A)$
7		biid	$⊢ \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} ((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))) \to f (i) \subseteq A)) \leftrightarrow \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} ((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))) \to f (i) \subseteq A))$
8		biid	$⊢ \underset{˙}{[} j / i \underset{˙}{]} f (\emptyset) = pred (X, A, R) \leftrightarrow \underset{˙}{[} j / i \underset{˙}{]} f (\emptyset) = pred (X, A, R)$
9		biid	$⊢ \underset{˙}{[} j / i \underset{˙}{]} \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow \underset{˙}{[} j / i \underset{˙}{]} \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
10		biid	$⊢ \underset{˙}{[} j / i \underset{˙}{]} (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 \underset{˙}{[} j / i \underset{˙}{]} (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)))$
11		biid	$⊢ \underset{˙}{[} j / i \underset{˙}{]} ((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))) \to f (i) \subseteq A) \leftrightarrow \underset{˙}{[} j / i \underset{˙}{]} ((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))) \to f (i) \subseteq A)$
12	1 2 3 4 5 6 7 8 9 10 11	bnj1128	$⊢ Y \in trCl (X, A, R) \to Y \in A$