bnj981

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj981.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj981.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj981.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj981.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
	bnj981.5	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
Assertion	bnj981	$⊢ Z \in trCl (X, A, R) \to \exists f \exists n \exists i (χ \land i \in n \land Z \in f (i))$

Proof

Step	Hyp	Ref	Expression
1		bnj981.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj981.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj981.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj981.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
5		bnj981.5	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
6		nfv	$⊢ Ⅎ y Z \in trCl (X, A, R)$
7		nfcv	$⊢ \underline{Ⅎ} y ω$
8		nfv	$⊢ Ⅎ y suc i \in n$
9		nfiu1	$⊢ \underline{Ⅎ} y ⋃_{y \in f (i)} pred (y, A, R)$
10	9	nfeq2	$⊢ Ⅎ y f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)$
11	8 10	nfim	$⊢ Ⅎ y (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
12	7 11	nfralw	$⊢ Ⅎ y \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
13	2 12	nfxfr	$⊢ Ⅎ y ψ$
14	13	nf5ri	$⊢ ψ \to \forall y ψ$
15	14 5	bnj1096	$⊢ χ \to \forall y χ$
16	15	nf5i	$⊢ Ⅎ y χ$
17		nfv	$⊢ Ⅎ y i \in n$
18		nfv	$⊢ Ⅎ y Z \in f (i)$
19	16 17 18	nf3an	$⊢ Ⅎ y (χ \land i \in n \land Z \in f (i))$
20	19	nfex	$⊢ Ⅎ y \exists i (χ \land i \in n \land Z \in f (i))$
21	20	nfex	$⊢ Ⅎ y \exists n \exists i (χ \land i \in n \land Z \in f (i))$
22	21	nfex	$⊢ Ⅎ y \exists f \exists n \exists i (χ \land i \in n \land Z \in f (i))$
23	6 22	nfim	$⊢ Ⅎ y (Z \in trCl (X, A, R) \to \exists f \exists n \exists i (χ \land i \in n \land Z \in f (i)))$
24		eleq1	$⊢ y = Z \to (y \in trCl (X, A, R) \leftrightarrow Z \in trCl (X, A, R))$
25		eleq1	$⊢ y = Z \to (y \in f (i) \leftrightarrow Z \in f (i))$
26	25	3anbi3d	$⊢ y = Z \to ((χ \land i \in n \land y \in f (i)) \leftrightarrow (χ \land i \in n \land Z \in f (i)))$
27	26	3exbidv	$⊢ y = Z \to (\exists f \exists n \exists i (χ \land i \in n \land y \in f (i)) \leftrightarrow \exists f \exists n \exists i (χ \land i \in n \land Z \in f (i)))$
28	24 27	imbi12d	$⊢ y = Z \to ((y \in trCl (X, A, R) \to \exists f \exists n \exists i (χ \land i \in n \land y \in f (i))) \leftrightarrow (Z \in trCl (X, A, R) \to \exists f \exists n \exists i (χ \land i \in n \land Z \in f (i))))$
29	1 2 3 4 5	bnj917	$⊢ y \in trCl (X, A, R) \to \exists f \exists n \exists i (χ \land i \in n \land y \in f (i))$
30	23 28 29	vtoclg1f	$⊢ Z \in trCl (X, A, R) \to (Z \in trCl (X, A, R) \to \exists f \exists n \exists i (χ \land i \in n \land Z \in f (i)))$
31	30	pm2.43i	$⊢ Z \in trCl (X, A, R) \to \exists f \exists n \exists i (χ \land i \in n \land Z \in f (i))$

Metamath Proof Explorer

Theorem bnj981

Proof