bnj969

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	bnj969.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj969.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj969.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj969.10	$⊢ D = ω ∖ \{\emptyset\}$
	bnj969.12	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
	bnj969.14	$⊢ τ \leftrightarrow (f Fn n \land φ \land ψ)$
	bnj969.15	$⊢ σ \leftrightarrow (n \in D \land p = suc n \land m \in n)$
Assertion	bnj969	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to C \in V$

Proof

Step	Hyp	Ref	Expression
1		bnj969.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj969.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj969.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj969.10	$⊢ D = ω ∖ \{\emptyset\}$
5		bnj969.12	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
6		bnj969.14	$⊢ τ \leftrightarrow (f Fn n \land φ \land ψ)$
7		bnj969.15	$⊢ σ \leftrightarrow (n \in D \land p = suc n \land m \in n)$
8		simpl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to (R FrSe A \land X \in A)$
9		bnj667	$⊢ (n \in D \land f Fn n \land φ \land ψ) \to (f Fn n \land φ \land ψ)$
10	9 3 6	3imtr4i	$⊢ χ \to τ$
11	10	3ad2ant1	$⊢ (χ \land n = suc m \land p = suc n) \to τ$
12	11	adantl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to τ$
13	3	bnj1232	$⊢ χ \to n \in D$
14		vex	$⊢ m \in V$
15	14	bnj216	$⊢ n = suc m \to m \in n$
16		id	$⊢ p = suc n \to p = suc n$
17	13 15 16	3anim123i	$⊢ (χ \land n = suc m \land p = suc n) \to (n \in D \land m \in n \land p = suc n)$
18		3ancomb	$⊢ (n \in D \land p = suc n \land m \in n) \leftrightarrow (n \in D \land m \in n \land p = suc n)$
19	7 18	bitri	$⊢ σ \leftrightarrow (n \in D \land m \in n \land p = suc n)$
20	17 19	sylibr	$⊢ (χ \land n = suc m \land p = suc n) \to σ$
21	20	adantl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to σ$
22	8 12 21	jca32	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to ((R FrSe A \land X \in A) \land (τ \land σ))$
23		bnj256	$⊢ (R FrSe A \land X \in A \land τ \land σ) \leftrightarrow ((R FrSe A \land X \in A) \land (τ \land σ))$
24	22 23	sylibr	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to (R FrSe A \land X \in A \land τ \land σ)$
25	4 6 7 1 2	bnj938	$⊢ (R FrSe A \land X \in A \land τ \land σ) \to ⋃_{y \in f (m)} pred (y, A, R) \in V$
26	5 25	eqeltrid	$⊢ (R FrSe A \land X \in A \land τ \land σ) \to C \in V$
27	24 26	syl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to C \in V$

Metamath Proof Explorer

Theorem bnj969

Proof