bnj967

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

Proof

Step	Hyp	Ref	Expression
1		bnj967.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
2		bnj967.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
3		bnj967.10	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj967.12	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
5		bnj967.13	$⊢ G = f \cup \{⟨n, C⟩\}$
6		bnj967.44	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to C \in V$
7	6	3adant3	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to C \in V$
8	2	bnj1235	$⊢ χ \to f Fn n$
9	8	3ad2ant1	$⊢ (χ \land n = suc m \land p = suc n) \to f Fn n$
10	9	3ad2ant2	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to f Fn n$
11		simp23	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to p = suc n$
12		simp3	$⊢ (i \in ω \land suc i \in p \land suc i \in n) \to suc i \in n$
13	12	3ad2ant3	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to suc i \in n$
14	7 10 11 13	bnj951	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to (C \in V \land f Fn n \land p = suc n \land suc i \in n)$
15	3	bnj923	$⊢ n \in D \to n \in ω$
16	2 15	bnj769	$⊢ χ \to n \in ω$
17	16	3ad2ant1	$⊢ (χ \land n = suc m \land p = suc n) \to n \in ω$
18	17 12	bnj240	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to (n \in ω \land suc i \in n)$
19		nnord	$⊢ n \in ω \to Ord n$
20		ordtr	$⊢ Ord n \to Tr n$
21	19 20	syl	$⊢ n \in ω \to Tr n$
22		trsuc	$⊢ (Tr n \land suc i \in n) \to i \in n$
23	21 22	sylan	$⊢ (n \in ω \land suc i \in n) \to i \in n$
24	18 23	syl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to i \in n$
25		bnj658	$⊢ (C \in V \land f Fn n \land p = suc n \land suc i \in n) \to (C \in V \land f Fn n \land p = suc n)$
26	25	anim1i	$⊢ ((C \in V \land f Fn n \land p = suc n \land suc i \in n) \land i \in n) \to ((C \in V \land f Fn n \land p = suc n) \land i \in n)$
27		df-bnj17	$⊢ (C \in V \land f Fn n \land p = suc n \land i \in n) \leftrightarrow ((C \in V \land f Fn n \land p = suc n) \land i \in n)$
28	26 27	sylibr	$⊢ ((C \in V \land f Fn n \land p = suc n \land suc i \in n) \land i \in n) \to (C \in V \land f Fn n \land p = suc n \land i \in n)$
29	14 24 28	syl2anc	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to (C \in V \land f Fn n \land p = suc n \land i \in n)$
30	5	bnj945	$⊢ (C \in V \land f Fn n \land p = suc n \land i \in n) \to G (i) = f (i)$
31	29 30	syl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to G (i) = f (i)$
32	5	bnj945	$⊢ (C \in V \land f Fn n \land p = suc n \land suc i \in n) \to G (suc i) = f (suc i)$
33	14 32	syl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to G (suc i) = f (suc i)$
34		3simpb	$⊢ (i \in ω \land suc i \in p \land suc i \in n) \to (i \in ω \land suc i \in n)$
35	34	3ad2ant3	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to (i \in ω \land suc i \in n)$
36	2	bnj1254	$⊢ χ \to ψ$
37	36	3ad2ant1	$⊢ (χ \land n = suc m \land p = suc n) \to ψ$
38	37	3ad2ant2	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to ψ$
39	31 33 35 38	bnj951	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to (G (i) = f (i) \land G (suc i) = f (suc i) \land (i \in ω \land suc i \in n) \land ψ)$
40	4 5	bnj958	$⊢ G (i) = f (i) \to \forall y G (i) = f (i)$
41	1 40	bnj953	$⊢ (G (i) = f (i) \land G (suc i) = f (suc i) \land (i \in ω \land suc i \in n) \land ψ) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
42	39 41	syl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p \land suc i \in n)) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$

Metamath Proof Explorer

Theorem bnj967

Proof