bnj1033

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

Proof

Step	Hyp	Ref	Expression
1		bnj1033.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1033.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1033.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj1033.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
5		bnj1033.5	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
6		bnj1033.6	$⊢ η \leftrightarrow z \in trCl (X, A, R)$
7		bnj1033.7	$⊢ ζ \leftrightarrow (i \in n \land z \in f (i))$
8		bnj1033.8	$⊢ D = ω ∖ \{\emptyset\}$
9		bnj1033.9	$⊢ K = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
10		bnj1033.10	$⊢ \exists f \exists n \exists i (θ \land τ \land χ \land ζ) \to z \in B$
11	1 2 8 9 3	bnj983	$⊢ z \in trCl (X, A, R) \leftrightarrow \exists f \exists n \exists i (χ \land i \in n \land z \in f (i))$
12		19.42v	$⊢ \exists i ((θ \land τ) \land (χ \land i \in n \land z \in f (i))) \leftrightarrow ((θ \land τ) \land \exists i (χ \land i \in n \land z \in f (i)))$
13		df-3an	$⊢ (θ \land τ \land (χ \land i \in n \land z \in f (i))) \leftrightarrow ((θ \land τ) \land (χ \land i \in n \land z \in f (i)))$
14	13	exbii	$⊢ \exists i (θ \land τ \land (χ \land i \in n \land z \in f (i))) \leftrightarrow \exists i ((θ \land τ) \land (χ \land i \in n \land z \in f (i)))$
15		df-3an	$⊢ (θ \land τ \land \exists i (χ \land i \in n \land z \in f (i))) \leftrightarrow ((θ \land τ) \land \exists i (χ \land i \in n \land z \in f (i)))$
16	12 14 15	3bitr4i	$⊢ \exists i (θ \land τ \land (χ \land i \in n \land z \in f (i))) \leftrightarrow (θ \land τ \land \exists i (χ \land i \in n \land z \in f (i)))$
17	16	exbii	$⊢ \exists n \exists i (θ \land τ \land (χ \land i \in n \land z \in f (i))) \leftrightarrow \exists n (θ \land τ \land \exists i (χ \land i \in n \land z \in f (i)))$
18		19.42v	$⊢ \exists n ((θ \land τ) \land \exists i (χ \land i \in n \land z \in f (i))) \leftrightarrow ((θ \land τ) \land \exists n \exists i (χ \land i \in n \land z \in f (i)))$
19	15	exbii	$⊢ \exists n (θ \land τ \land \exists i (χ \land i \in n \land z \in f (i))) \leftrightarrow \exists n ((θ \land τ) \land \exists i (χ \land i \in n \land z \in f (i)))$
20		df-3an	$⊢ (θ \land τ \land \exists n \exists i (χ \land i \in n \land z \in f (i))) \leftrightarrow ((θ \land τ) \land \exists n \exists i (χ \land i \in n \land z \in f (i)))$
21	18 19 20	3bitr4i	$⊢ \exists n (θ \land τ \land \exists i (χ \land i \in n \land z \in f (i))) \leftrightarrow (θ \land τ \land \exists n \exists i (χ \land i \in n \land z \in f (i)))$
22	17 21	bitri	$⊢ \exists n \exists i (θ \land τ \land (χ \land i \in n \land z \in f (i))) \leftrightarrow (θ \land τ \land \exists n \exists i (χ \land i \in n \land z \in f (i)))$
23	22	exbii	$⊢ \exists f \exists n \exists i (θ \land τ \land (χ \land i \in n \land z \in f (i))) \leftrightarrow \exists f (θ \land τ \land \exists n \exists i (χ \land i \in n \land z \in f (i)))$
24		19.42v	$⊢ \exists f ((θ \land τ) \land \exists n \exists i (χ \land i \in n \land z \in f (i))) \leftrightarrow ((θ \land τ) \land \exists f \exists n \exists i (χ \land i \in n \land z \in f (i)))$
25	20	exbii	$⊢ \exists f (θ \land τ \land \exists n \exists i (χ \land i \in n \land z \in f (i))) \leftrightarrow \exists f ((θ \land τ) \land \exists n \exists i (χ \land i \in n \land z \in f (i)))$
26		df-3an	$⊢ (θ \land τ \land \exists f \exists n \exists i (χ \land i \in n \land z \in f (i))) \leftrightarrow ((θ \land τ) \land \exists f \exists n \exists i (χ \land i \in n \land z \in f (i)))$
27	24 25 26	3bitr4i	$⊢ \exists f (θ \land τ \land \exists n \exists i (χ \land i \in n \land z \in f (i))) \leftrightarrow (θ \land τ \land \exists f \exists n \exists i (χ \land i \in n \land z \in f (i)))$
28	23 27	bitri	$⊢ \exists f \exists n \exists i (θ \land τ \land (χ \land i \in n \land z \in f (i))) \leftrightarrow (θ \land τ \land \exists f \exists n \exists i (χ \land i \in n \land z \in f (i)))$
29		bnj255	$⊢ (θ \land τ \land χ \land ζ) \leftrightarrow (θ \land τ \land (χ \land ζ))$
30	7	anbi2i	$⊢ (χ \land ζ) \leftrightarrow (χ \land (i \in n \land z \in f (i)))$
31		3anass	$⊢ (χ \land i \in n \land z \in f (i)) \leftrightarrow (χ \land (i \in n \land z \in f (i)))$
32	30 31	bitr4i	$⊢ (χ \land ζ) \leftrightarrow (χ \land i \in n \land z \in f (i))$
33	32	3anbi3i	$⊢ (θ \land τ \land (χ \land ζ)) \leftrightarrow (θ \land τ \land (χ \land i \in n \land z \in f (i)))$
34	29 33	bitri	$⊢ (θ \land τ \land χ \land ζ) \leftrightarrow (θ \land τ \land (χ \land i \in n \land z \in f (i)))$
35	34	3exbii	$⊢ \exists f \exists n \exists i (θ \land τ \land χ \land ζ) \leftrightarrow \exists f \exists n \exists i (θ \land τ \land (χ \land i \in n \land z \in f (i)))$
36	35 10	sylbir	$⊢ \exists f \exists n \exists i (θ \land τ \land (χ \land i \in n \land z \in f (i))) \to z \in B$
37	28 36	sylbir	$⊢ (θ \land τ \land \exists f \exists n \exists i (χ \land i \in n \land z \in f (i))) \to z \in B$
38	11 37	syl3an3b	$⊢ (θ \land τ \land z \in trCl (X, A, R)) \to z \in B$
39	38	3expia	$⊢ (θ \land τ) \to (z \in trCl (X, A, R) \to z \in B)$
40	39	ssrdv	$⊢ (θ \land τ) \to trCl (X, A, R) \subseteq B$

Metamath Proof Explorer

Theorem bnj1033

Proof