bnj966

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

Proof

Step	Hyp	Ref	Expression
1		bnj966.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
2		bnj966.10	$⊢ D = ω ∖ \{\emptyset\}$
3		bnj966.12	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
4		bnj966.13	$⊢ G = f \cup \{⟨n, C⟩\}$
5		bnj966.44	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to C \in V$
6		bnj966.53	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to G Fn p$
7	6	bnj930	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to Fun G$
8	7	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 n = suc i)) \to Fun G$
9		opex	$⊢ ⟨n, C⟩ \in V$
10	9	snid	$⊢ ⟨n, C⟩ \in \{⟨n, C⟩\}$
11		elun2	$⊢ ⟨n, C⟩ \in \{⟨n, C⟩\} \to ⟨n, C⟩ \in (f \cup \{⟨n, C⟩\})$
12	10 11	ax-mp	$⊢ ⟨n, C⟩ \in (f \cup \{⟨n, C⟩\})$
13	12 4	eleqtrri	$⊢ ⟨n, C⟩ \in G$
14		funopfv	$⊢ Fun G \to (⟨n, C⟩ \in G \to G (n) = C)$
15	8 13 14	mpisyl	$⊢ ((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 n = suc i)) \to G (n) = C$
16		simp22	$⊢ ((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 n = suc i)) \to n = suc m$
17		simp33	$⊢ ((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 n = suc i)) \to n = suc i$
18		bnj551	$⊢ (n = suc m \land n = suc i) \to m = i$
19	16 17 18	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 n = suc i)) \to m = i$
20		suceq	$⊢ m = i \to suc m = suc i$
21	20	eqeq2d	$⊢ m = i \to (n = suc m \leftrightarrow n = suc i)$
22	21	biimpac	$⊢ (n = suc m \land m = i) \to n = suc i$
23	22	fveq2d	$⊢ (n = suc m \land m = i) \to G (n) = G (suc i)$
24		fveq2	$⊢ m = i \to f (m) = f (i)$
25	24	bnj1113	$⊢ m = i \to ⋃_{y \in f (m)} pred (y, A, R) = ⋃_{y \in f (i)} pred (y, A, R)$
26	3 25	syl5eq	$⊢ m = i \to C = ⋃_{y \in f (i)} pred (y, A, R)$
27	26	adantl	$⊢ (n = suc m \land m = i) \to C = ⋃_{y \in f (i)} pred (y, A, R)$
28	23 27	eqeq12d	$⊢ (n = suc m \land m = i) \to (G (n) = C \leftrightarrow G (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
29	16 19 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 n = suc i)) \to (G (n) = C \leftrightarrow G (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
30	15 29	mpbid	$⊢ ((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 n = suc i)) \to G (suc i) = ⋃_{y \in f (i)} pred (y, A, R)$
31	5	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 n = suc i)) \to C \in V$
32	1	bnj1235	$⊢ χ \to f Fn n$
33	32	3ad2ant1	$⊢ (χ \land n = suc m \land p = suc n) \to f Fn n$
34	33	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 n = suc i)) \to f Fn n$
35		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 n = suc i)) \to p = suc n$
36	31 34 35 17	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 n = suc i)) \to (C \in V \land f Fn n \land p = suc n \land n = suc i)$
37	2	bnj923	$⊢ n \in D \to n \in ω$
38	1 37	bnj769	$⊢ χ \to n \in ω$
39	38	3ad2ant1	$⊢ (χ \land n = suc m \land p = suc n) \to n \in ω$
40		simp3	$⊢ (i \in ω \land suc i \in p \land n = suc i) \to n = suc i$
41	39 40	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 n = suc i)) \to (n \in ω \land n = suc i)$
42		vex	$⊢ i \in V$
43	42	bnj216	$⊢ n = suc i \to i \in n$
44	43	adantl	$⊢ (n \in ω \land n = suc i) \to i \in n$
45	41 44	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 n = suc i)) \to i \in n$
46		bnj658	$⊢ (C \in V \land f Fn n \land p = suc n \land n = suc i) \to (C \in V \land f Fn n \land p = suc n)$
47	46	anim1i	$⊢ ((C \in V \land f Fn n \land p = suc n \land n = suc i) \land i \in n) \to ((C \in V \land f Fn n \land p = suc n) \land i \in n)$
48		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)$
49	47 48	sylibr	$⊢ ((C \in V \land f Fn n \land p = suc n \land n = suc i) \land i \in n) \to (C \in V \land f Fn n \land p = suc n \land i \in n)$
50	4	bnj945	$⊢ (C \in V \land f Fn n \land p = suc n \land i \in n) \to G (i) = f (i)$
51	49 50	syl	$⊢ ((C \in V \land f Fn n \land p = suc n \land n = suc i) \land i \in n) \to G (i) = f (i)$
52	36 45 51	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 n = suc i)) \to G (i) = f (i)$
53	3 4	bnj958	$⊢ G (i) = f (i) \to \forall y G (i) = f (i)$
54	53	bnj956	$⊢ G (i) = f (i) \to ⋃_{y \in G (i)} pred (y, A, R) = ⋃_{y \in f (i)} pred (y, A, R)$
55	54	eqeq2d	$⊢ G (i) = f (i) \to (G (suc i) = ⋃_{y \in G (i)} pred (y, A, R) \leftrightarrow G (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
56	52 55	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 n = suc i)) \to (G (suc i) = ⋃_{y \in G (i)} pred (y, A, R) \leftrightarrow G (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
57	30 56	mpbird	$⊢ ((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 n = suc i)) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$

Metamath Proof Explorer

Theorem bnj966

Proof