bnj557

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	bnj557.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj557.16	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
	bnj557.17	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj557.18	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
	bnj557.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
	bnj557.20	$⊢ ζ \leftrightarrow (i \in ω \land suc i \in n \land m = suc i)$
	bnj557.21	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
	bnj557.22	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
	bnj557.23	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
	bnj557.24	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
	bnj557.25	$⊢ G = f \cup \{⟨m, C⟩\}$
	bnj557.28	No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
	bnj557.29	No typesetting found for \|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode \|-
	bnj557.36	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
Assertion	bnj557	$⊢ (R FrSe A \land τ \land η \land ζ) \to G (m) = L$

Proof

Step	Hyp	Ref	Expression
1		bnj557.3	$⊢ D = ω ∖ \{\emptyset\}$
2		bnj557.16	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
3		bnj557.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
4		bnj557.18	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
5		bnj557.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
6		bnj557.20	$⊢ ζ \leftrightarrow (i \in ω \land suc i \in n \land m = suc i)$
7		bnj557.21	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
8		bnj557.22	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
9		bnj557.23	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
10		bnj557.24	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
11		bnj557.25	$⊢ G = f \cup \{⟨m, C⟩\}$
12		bnj557.28	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
13		bnj557.29	Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode \|-
14		bnj557.36	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
15		3an4anass	$⊢ ((R FrSe A \land τ \land η) \land ζ) \leftrightarrow ((R FrSe A \land τ) \land (η \land ζ))$
16	4 5	bnj556	$⊢ η \to σ$
17	16	3anim3i	$⊢ (R FrSe A \land τ \land η) \to (R FrSe A \land τ \land σ)$
18		vex	$⊢ i \in V$
19	18	bnj216	$⊢ m = suc i \to i \in m$
20	6 19	bnj837	$⊢ ζ \to i \in m$
21	17 20	anim12i	$⊢ ((R FrSe A \land τ \land η) \land ζ) \to ((R FrSe A \land τ \land σ) \land i \in m)$
22	15 21	sylbir	$⊢ ((R FrSe A \land τ) \land (η \land ζ)) \to ((R FrSe A \land τ \land σ) \land i \in m)$
23	5	bnj1254	$⊢ η \to m = suc p$
24	6	simp3bi	$⊢ ζ \to m = suc i$
25		bnj551	$⊢ (m = suc p \land m = suc i) \to p = i$
26	23 24 25	syl2an	$⊢ (η \land ζ) \to p = i$
27	26	adantl	$⊢ ((R FrSe A \land τ) \land (η \land ζ)) \to p = i$
28	22 27	jca	$⊢ ((R FrSe A \land τ) \land (η \land ζ)) \to (((R FrSe A \land τ \land σ) \land i \in m) \land p = i)$
29		bnj256	$⊢ (R FrSe A \land τ \land η \land ζ) \leftrightarrow ((R FrSe A \land τ) \land (η \land ζ))$
30		df-3an	$⊢ ((R FrSe A \land τ \land σ) \land i \in m \land p = i) \leftrightarrow (((R FrSe A \land τ \land σ) \land i \in m) \land p = i)$
31	28 29 30	3imtr4i	$⊢ (R FrSe A \land τ \land η \land ζ) \to ((R FrSe A \land τ \land σ) \land i \in m \land p = i)$
32	12 13 1 2 3 4 8 11 7 9 10 14	bnj553	$⊢ ((R FrSe A \land τ \land σ) \land i \in m \land p = i) \to G (m) = L$
33	31 32	syl	$⊢ (R FrSe A \land τ \land η \land ζ) \to G (m) = L$

Metamath Proof Explorer

Theorem bnj557

Proof