bnj1034

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

Proof

Step	Hyp	Ref	Expression
1		bnj1034.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1034.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1034.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj1034.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
5		bnj1034.5	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
6		bnj1034.7	$⊢ ζ \leftrightarrow (i \in n \land z \in f (i))$
7		bnj1034.8	$⊢ D = ω ∖ \{\emptyset\}$
8		bnj1034.9	$⊢ K = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
9		bnj1034.10	$⊢ \exists f \exists n \exists i (θ \land τ \land χ \land ζ) \to z \in B$
10		biid	$⊢ z \in trCl (X, A, R) \leftrightarrow z \in trCl (X, A, R)$
11	1 2 3 4 5 10 6 7 8 9	bnj1033	$⊢ (θ \land τ) \to trCl (X, A, R) \subseteq B$

Metamath Proof Explorer

Theorem bnj1034

Proof