bnj1021

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	bnj1021.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj1021.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj1021.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj1021.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
	bnj1021.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
	bnj1021.6	$⊢ η \leftrightarrow (i \in n \land y \in f (i))$
	bnj1021.13	$⊢ D = ω ∖ \{\emptyset\}$
	bnj1021.14	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
Assertion	bnj1021	$⊢ \exists f \exists n \exists i \exists m (θ \to (θ \land χ \land η \land \exists p τ))$

Proof

Step	Hyp	Ref	Expression
1		bnj1021.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1021.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1021.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj1021.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
5		bnj1021.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
6		bnj1021.6	$⊢ η \leftrightarrow (i \in n \land y \in f (i))$
7		bnj1021.13	$⊢ D = ω ∖ \{\emptyset\}$
8		bnj1021.14	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
9	1 2 3 4 5 6 7 8	bnj996	$⊢ \exists f \exists n \exists i \exists m \exists p (θ \to (χ \land τ \land η))$
10		anclb	$⊢ (θ \to (χ \land τ \land η)) \leftrightarrow (θ \to (θ \land (χ \land τ \land η)))$
11		bnj252	$⊢ (θ \land χ \land τ \land η) \leftrightarrow (θ \land (χ \land τ \land η))$
12	11	imbi2i	$⊢ (θ \to (θ \land χ \land τ \land η)) \leftrightarrow (θ \to (θ \land (χ \land τ \land η)))$
13	10 12	bitr4i	$⊢ (θ \to (χ \land τ \land η)) \leftrightarrow (θ \to (θ \land χ \land τ \land η))$
14	13	2exbii	$⊢ \exists m \exists p (θ \to (χ \land τ \land η)) \leftrightarrow \exists m \exists p (θ \to (θ \land χ \land τ \land η))$
15	14	3exbii	$⊢ \exists f \exists n \exists i \exists m \exists p (θ \to (χ \land τ \land η)) \leftrightarrow \exists f \exists n \exists i \exists m \exists p (θ \to (θ \land χ \land τ \land η))$
16	9 15	mpbi	$⊢ \exists f \exists n \exists i \exists m \exists p (θ \to (θ \land χ \land τ \land η))$
17		19.37v	$⊢ \exists p (θ \to (θ \land χ \land τ \land η)) \leftrightarrow (θ \to \exists p (θ \land χ \land τ \land η))$
18		bnj1019	$⊢ \exists p (θ \land χ \land τ \land η) \leftrightarrow (θ \land χ \land η \land \exists p τ)$
19	18	imbi2i	$⊢ (θ \to \exists p (θ \land χ \land τ \land η)) \leftrightarrow (θ \to (θ \land χ \land η \land \exists p τ))$
20	17 19	bitri	$⊢ \exists p (θ \to (θ \land χ \land τ \land η)) \leftrightarrow (θ \to (θ \land χ \land η \land \exists p τ))$
21	20	2exbii	$⊢ \exists i \exists m \exists p (θ \to (θ \land χ \land τ \land η)) \leftrightarrow \exists i \exists m (θ \to (θ \land χ \land η \land \exists p τ))$
22	21	2exbii	$⊢ \exists f \exists n \exists i \exists m \exists p (θ \to (θ \land χ \land τ \land η)) \leftrightarrow \exists f \exists n \exists i \exists m (θ \to (θ \land χ \land η \land \exists p τ))$
23	16 22	mpbi	$⊢ \exists f \exists n \exists i \exists m (θ \to (θ \land χ \land η \land \exists p τ))$

Metamath Proof Explorer

Theorem bnj1021

Proof