bnj1124

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

	Ref	Expression
Hypotheses	bnj1124.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
	bnj1124.5	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
Assertion	bnj1124	$⊢ (θ \land τ) \to trCl (X, A, R) \subseteq B$

Proof

Step	Hyp	Ref	Expression
1		bnj1124.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
2		bnj1124.5	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
3		biid	$⊢ f (\emptyset) = pred (X, A, R) \leftrightarrow f (\emptyset) = pred (X, A, R)$
4		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))$
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 \in n \land z \in f (i)) \leftrightarrow (i \in n \land z \in f (i))$
7		eqid	$⊢ ω ∖ \{\emptyset\} = ω ∖ \{\emptyset\}$
8		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)))\}$
9		biid	$⊢ ((f \in \{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)))\} \land i \in dom f) \to f (i) \subseteq B) \leftrightarrow ((f \in \{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)))\} \land i \in dom f) \to f (i) \subseteq B)$
10		biid	$⊢ \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} ((f \in \{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)))\} \land i \in dom f) \to f (i) \subseteq B)) \leftrightarrow \forall j \in n (j E i \to \underset{˙}{[} j / i \underset{˙}{]} ((f \in \{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)))\} \land i \in dom f) \to f (i) \subseteq B))$
11		biid	$⊢ \underset{˙}{[} j / i \underset{˙}{]} f (\emptyset) = pred (X, A, R) \leftrightarrow \underset{˙}{[} j / i \underset{˙}{]} f (\emptyset) = pred (X, A, R)$
12		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))$
13		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)))$
14		biid	$⊢ \underset{˙}{[} j / i \underset{˙}{]} θ \leftrightarrow \underset{˙}{[} j / i \underset{˙}{]} θ$
15		biid	$⊢ \underset{˙}{[} j / i \underset{˙}{]} τ \leftrightarrow \underset{˙}{[} j / i \underset{˙}{]} τ$
16		biid	$⊢ \underset{˙}{[} j / i \underset{˙}{]} (i \in n \land z \in f (i)) \leftrightarrow \underset{˙}{[} j / i \underset{˙}{]} (i \in n \land z \in f (i))$
17		biid	$⊢ \underset{˙}{[} j / i \underset{˙}{]} ((f \in \{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)))\} \land i \in dom f) \to f (i) \subseteq B) \leftrightarrow \underset{˙}{[} j / i \underset{˙}{]} ((f \in \{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)))\} \land i \in dom f) \to f (i) \subseteq B)$
18		biid	$⊢ ((j \in n \land j E i) \to \underset{˙}{[} j / i \underset{˙}{]} ((f \in \{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)))\} \land i \in dom f) \to f (i) \subseteq B)) \leftrightarrow ((j \in n \land j E i) \to \underset{˙}{[} j / i \underset{˙}{]} ((f \in \{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)))\} \land i \in dom f) \to f (i) \subseteq B))$
19		biid	$⊢ (i \in n \land ((j \in n \land j E i) \to \underset{˙}{[} j / i \underset{˙}{]} ((f \in \{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)))\} \land i \in dom f) \to f (i) \subseteq B)) \land f \in \{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)))\} \land i \in dom f) \leftrightarrow (i \in n \land ((j \in n \land j E i) \to \underset{˙}{[} j / i \underset{˙}{]} ((f \in \{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)))\} \land i \in dom f) \to f (i) \subseteq B)) \land f \in \{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)))\} \land i \in dom f)$
20	3 4 5 1 2 6 7 8 9 10 11 12 13 14 15 16 17 18 19	bnj1030	$⊢ (θ \land τ) \to trCl (X, A, R) \subseteq B$

Metamath Proof Explorer

Theorem bnj1124

Proof