bnj1121

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	bnj1121.1	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
	bnj1121.2	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
	bnj1121.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj1121.4	$⊢ ζ \leftrightarrow (i \in n \land z \in f (i))$
	bnj1121.5	$⊢ η \leftrightarrow ((f \in K \land i \in dom f) \to f (i) \subseteq B)$
	bnj1121.6	$⊢ (θ \land τ \land χ \land ζ) \to \forall i \in n η$
	bnj1121.7	$⊢ K = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
Assertion	bnj1121	$⊢ (θ \land τ \land χ \land ζ) \to z \in B$

Proof

Step	Hyp	Ref	Expression
1		bnj1121.1	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
2		bnj1121.2	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
3		bnj1121.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj1121.4	$⊢ ζ \leftrightarrow (i \in n \land z \in f (i))$
5		bnj1121.5	$⊢ η \leftrightarrow ((f \in K \land i \in dom f) \to f (i) \subseteq B)$
6		bnj1121.6	$⊢ (θ \land τ \land χ \land ζ) \to \forall i \in n η$
7		bnj1121.7	$⊢ K = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
8		19.8a	$⊢ χ \to \exists n χ$
9	8	bnj707	$⊢ (θ \land τ \land χ \land ζ) \to \exists n χ$
10	3 7	bnj1083	$⊢ f \in K \leftrightarrow \exists n χ$
11	9 10	sylibr	$⊢ (θ \land τ \land χ \land ζ) \to f \in K$
12	4	simplbi	$⊢ ζ \to i \in n$
13	12	bnj708	$⊢ (θ \land τ \land χ \land ζ) \to i \in n$
14	3	bnj1235	$⊢ χ \to f Fn n$
15	14	bnj707	$⊢ (θ \land τ \land χ \land ζ) \to f Fn n$
16	15	fndmd	$⊢ (θ \land τ \land χ \land ζ) \to dom f = n$
17	13 16	eleqtrrd	$⊢ (θ \land τ \land χ \land ζ) \to i \in dom f$
18	6 13	bnj1294	$⊢ (θ \land τ \land χ \land ζ) \to η$
19	18 5	sylib	$⊢ (θ \land τ \land χ \land ζ) \to ((f \in K \land i \in dom f) \to f (i) \subseteq B)$
20	11 17 19	mp2and	$⊢ (θ \land τ \land χ \land ζ) \to f (i) \subseteq B$
21	4	simprbi	$⊢ ζ \to z \in f (i)$
22	21	bnj708	$⊢ (θ \land τ \land χ \land ζ) \to z \in f (i)$
23	20 22	sseldd	$⊢ (θ \land τ \land χ \land ζ) \to z \in B$

Metamath Proof Explorer

Theorem bnj1121

Proof