bnj996

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

Proof

Step	Hyp	Ref	Expression
1		bnj996.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj996.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj996.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj996.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
5		bnj996.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
6		bnj996.6	$⊢ η \leftrightarrow (i \in n \land y \in f (i))$
7		bnj996.13	$⊢ D = ω ∖ \{\emptyset\}$
8		bnj996.14	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
9	1 2 7 8 3	bnj917	$⊢ y \in trCl (X, A, R) \to \exists f \exists n \exists i (χ \land i \in n \land y \in f (i))$
10	4 9	bnj771	$⊢ θ \to \exists f \exists n \exists i (χ \land i \in n \land y \in f (i))$
11		3anass	$⊢ (χ \land i \in n \land y \in f (i)) \leftrightarrow (χ \land (i \in n \land y \in f (i)))$
12	6	anbi2i	$⊢ (χ \land η) \leftrightarrow (χ \land (i \in n \land y \in f (i)))$
13	11 12	bitr4i	$⊢ (χ \land i \in n \land y \in f (i)) \leftrightarrow (χ \land η)$
14	13	3exbii	$⊢ \exists f \exists n \exists i (χ \land i \in n \land y \in f (i)) \leftrightarrow \exists f \exists n \exists i (χ \land η)$
15	10 14	sylib	$⊢ θ \to \exists f \exists n \exists i (χ \land η)$
16	3 7 5	bnj986	$⊢ χ \to \exists m \exists p τ$
17	16	ancli	$⊢ χ \to (χ \land \exists m \exists p τ)$
18		19.42vv	$⊢ \exists m \exists p (χ \land τ) \leftrightarrow (χ \land \exists m \exists p τ)$
19	17 18	sylibr	$⊢ χ \to \exists m \exists p (χ \land τ)$
20	19	anim1i	$⊢ (χ \land η) \to (\exists m \exists p (χ \land τ) \land η)$
21		19.41vv	$⊢ \exists m \exists p ((χ \land τ) \land η) \leftrightarrow (\exists m \exists p (χ \land τ) \land η)$
22	20 21	sylibr	$⊢ (χ \land η) \to \exists m \exists p ((χ \land τ) \land η)$
23		df-3an	$⊢ (χ \land τ \land η) \leftrightarrow ((χ \land τ) \land η)$
24	23	2exbii	$⊢ \exists m \exists p (χ \land τ \land η) \leftrightarrow \exists m \exists p ((χ \land τ) \land η)$
25	22 24	sylibr	$⊢ (χ \land η) \to \exists m \exists p (χ \land τ \land η)$
26	25	2eximi	$⊢ \exists n \exists i (χ \land η) \to \exists n \exists i \exists m \exists p (χ \land τ \land η)$
27	15 26	bnj593	$⊢ θ \to \exists f \exists n \exists i \exists m \exists p (χ \land τ \land η)$
28		19.37v	$⊢ \exists p (θ \to (χ \land τ \land η)) \leftrightarrow (θ \to \exists p (χ \land τ \land η))$
29	28	exbii	$⊢ \exists m \exists p (θ \to (χ \land τ \land η)) \leftrightarrow \exists m (θ \to \exists p (χ \land τ \land η))$
30	29	bnj132	$⊢ \exists m \exists p (θ \to (χ \land τ \land η)) \leftrightarrow (θ \to \exists m \exists p (χ \land τ \land η))$
31	30	exbii	$⊢ \exists i \exists m \exists p (θ \to (χ \land τ \land η)) \leftrightarrow \exists i (θ \to \exists m \exists p (χ \land τ \land η))$
32	31	bnj132	$⊢ \exists i \exists m \exists p (θ \to (χ \land τ \land η)) \leftrightarrow (θ \to \exists i \exists m \exists p (χ \land τ \land η))$
33	32	exbii	$⊢ \exists n \exists i \exists m \exists p (θ \to (χ \land τ \land η)) \leftrightarrow \exists n (θ \to \exists i \exists m \exists p (χ \land τ \land η))$
34	33	bnj132	$⊢ \exists n \exists i \exists m \exists p (θ \to (χ \land τ \land η)) \leftrightarrow (θ \to \exists n \exists i \exists m \exists p (χ \land τ \land η))$
35	34	exbii	$⊢ \exists f \exists n \exists i \exists m \exists p (θ \to (χ \land τ \land η)) \leftrightarrow \exists f (θ \to \exists n \exists i \exists m \exists p (χ \land τ \land η))$
36	35	bnj132	$⊢ \exists f \exists n \exists i \exists m \exists p (θ \to (χ \land τ \land η)) \leftrightarrow (θ \to \exists f \exists n \exists i \exists m \exists p (χ \land τ \land η))$
37	27 36	mpbir	$⊢ \exists f \exists n \exists i \exists m \exists p (θ \to (χ \land τ \land η))$

Metamath Proof Explorer

Theorem bnj996

Proof