bnj964

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	bnj964.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj964.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj964.5	No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
	bnj964.8	No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
	bnj964.12	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
	bnj964.13	$⊢ G = f \cup \{⟨n, C⟩\}$
	bnj964.96	$⊢ ((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)$
	bnj964.165	$⊢ ((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)$
Assertion	bnj964	Could not format assertion : No typesetting found for \|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj964.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
2		bnj964.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
3		bnj964.5	Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
4		bnj964.8	Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
5		bnj964.12	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
6		bnj964.13	$⊢ G = f \cup \{⟨n, C⟩\}$
7		bnj964.96	$⊢ ((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)$
8		bnj964.165	$⊢ ((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)$
9		nfv	$⊢ Ⅎ i (R FrSe A \land X \in A)$
10	1	bnj1095	$⊢ ψ \to \forall i ψ$
11	10 2	bnj1096	$⊢ χ \to \forall i χ$
12	11	nf5i	$⊢ Ⅎ i χ$
13		nfv	$⊢ Ⅎ i n = suc m$
14		nfv	$⊢ Ⅎ i p = suc n$
15	12 13 14	nf3an	$⊢ Ⅎ i (χ \land n = suc m \land p = suc n)$
16	9 15	nfan	$⊢ Ⅎ i ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n))$
17		bnj255	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p) \leftrightarrow ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p))$
18		bnj645	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p) \to suc i \in p$
19		simp3	$⊢ (χ \land n = suc m \land p = suc n) \to p = suc n$
20	19	bnj706	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p) \to p = suc n$
21		eleq2	$⊢ p = suc n \to (suc i \in p \leftrightarrow suc i \in suc n)$
22	21	biimpac	$⊢ (suc i \in p \land p = suc n) \to suc i \in suc n$
23		elsuci	$⊢ suc i \in suc n \to (suc i \in n \lor suc i = n)$
24		eqcom	$⊢ suc i = n \leftrightarrow n = suc i$
25	24	orbi2i	$⊢ (suc i \in n \lor suc i = n) \leftrightarrow (suc i \in n \lor n = suc i)$
26	23 25	sylib	$⊢ suc i \in suc n \to (suc i \in n \lor n = suc i)$
27	22 26	syl	$⊢ (suc i \in p \land p = suc n) \to (suc i \in n \lor n = suc i)$
28	18 20 27	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) \to (suc i \in n \lor n = suc i)$
29		df-3an	$⊢ (i \in ω \land suc i \in p \land suc i \in n) \leftrightarrow ((i \in ω \land suc i \in p) \land suc i \in n)$
30	29	3anbi3i	$⊢ ((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)) \leftrightarrow ((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))$
31		bnj255	$⊢ ((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) \leftrightarrow ((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))$
32	30 31	bitr4i	$⊢ ((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)) \leftrightarrow ((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)$
33		bnj345	$⊢ ((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) \leftrightarrow (suc i \in n \land (R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p))$
34		bnj252	$⊢ (suc i \in n \land (R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p)) \leftrightarrow (suc i \in n \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p)))$
35	32 33 34	3bitri	$⊢ ((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)) \leftrightarrow (suc i \in n \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p)))$
36	17	anbi2i	$⊢ (suc i \in n \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p)) \leftrightarrow (suc i \in n \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p)))$
37	35 36	bitr4i	$⊢ ((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)) \leftrightarrow (suc i \in n \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p))$
38	37 7	sylbir	$⊢ (suc i \in n \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p)) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
39	38	ex	$⊢ suc i \in n \to (((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R))$
40		df-3an	$⊢ (i \in ω \land suc i \in p \land n = suc i) \leftrightarrow ((i \in ω \land suc i \in p) \land n = suc i)$
41	40	3anbi3i	$⊢ ((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)) \leftrightarrow ((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))$
42		bnj255	$⊢ ((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) \leftrightarrow ((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))$
43	41 42	bitr4i	$⊢ ((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)) \leftrightarrow ((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)$
44		bnj345	$⊢ ((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) \leftrightarrow (n = suc i \land (R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p))$
45		bnj252	$⊢ (n = suc i \land (R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p)) \leftrightarrow (n = suc i \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p)))$
46	43 44 45	3bitri	$⊢ ((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)) \leftrightarrow (n = suc i \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p)))$
47	17	anbi2i	$⊢ (n = suc i \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p)) \leftrightarrow (n = suc i \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p)))$
48	46 47	bitr4i	$⊢ ((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)) \leftrightarrow (n = suc i \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p))$
49	48 8	sylbir	$⊢ (n = suc i \land ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p)) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
50	49	ex	$⊢ n = suc i \to (((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R))$
51	39 50	jaoi	$⊢ (suc i \in n \lor n = suc i) \to (((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R))$
52	28 51	mpcom	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land i \in ω \land suc i \in p) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
53	17 52	sylbir	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n) \land (i \in ω \land suc i \in p)) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R)$
54	53	3expia	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to ((i \in ω \land suc i \in p) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R))$
55	16 54	alrimi	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to \forall i ((i \in ω \land suc i \in p) \to G (suc i) = ⋃_{y \in G (i)} pred (y, A, R))$
56		vex	$⊢ p \in V$
57	1 3 56	bnj539	Could not format ( ps' <-> A. i e. _om ( suc i e. p -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps' <-> A. i e. _om ( suc i e. p -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode \|-
58	57 4 5 6	bnj965	Could not format ( ps" <-> A. i e. _om ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps" <-> A. i e. _om ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode \|-
59	58	bnj115	Could not format ( ps" <-> A. i ( ( i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps" <-> A. i ( ( i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode \|-
60	55 59	sylibr	Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) : No typesetting found for \|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) with typecode \|-

Metamath Proof Explorer

Theorem bnj964

Proof