bnj518

Description: Technical lemma for bnj852 . 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	bnj518.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
	bnj518.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj518.3	$⊢ τ \leftrightarrow (φ \land ψ \land n \in ω \land p \in n)$
Assertion	bnj518	$⊢ (R FrSe A \land τ) \to \forall y \in f (p) pred (y, A, R) \in V$

Proof

Step	Hyp	Ref	Expression
1		bnj518.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
2		bnj518.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj518.3	$⊢ τ \leftrightarrow (φ \land ψ \land n \in ω \land p \in n)$
4		bnj334	$⊢ (φ \land ψ \land n \in ω \land p \in n) \leftrightarrow (n \in ω \land φ \land ψ \land p \in n)$
5	3 4	bitri	$⊢ τ \leftrightarrow (n \in ω \land φ \land ψ \land p \in n)$
6		df-bnj17	$⊢ (n \in ω \land φ \land ψ \land p \in n) \leftrightarrow ((n \in ω \land φ \land ψ) \land p \in n)$
7	1 2	bnj517	$⊢ (n \in ω \land φ \land ψ) \to \forall p \in n f (p) \subseteq A$
8	7	r19.21bi	$⊢ ((n \in ω \land φ \land ψ) \land p \in n) \to f (p) \subseteq A$
9	6 8	sylbi	$⊢ (n \in ω \land φ \land ψ \land p \in n) \to f (p) \subseteq A$
10	5 9	sylbi	$⊢ τ \to f (p) \subseteq A$
11		ssel	$⊢ f (p) \subseteq A \to (y \in f (p) \to y \in A)$
12		bnj93	$⊢ (R FrSe A \land y \in A) \to pred (y, A, R) \in V$
13	12	ex	$⊢ R FrSe A \to (y \in A \to pred (y, A, R) \in V)$
14	11 13	sylan9r	$⊢ (R FrSe A \land f (p) \subseteq A) \to (y \in f (p) \to pred (y, A, R) \in V)$
15	14	ralrimiv	$⊢ (R FrSe A \land f (p) \subseteq A) \to \forall y \in f (p) pred (y, A, R) \in V$
16	10 15	sylan2	$⊢ (R FrSe A \land τ) \to \forall y \in f (p) pred (y, A, R) \in V$

Metamath Proof Explorer

Theorem bnj518

Proof