bnj558

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

Proof

Step	Hyp	Ref	Expression
1		bnj558.3	$⊢ D = ω ∖ \{\emptyset\}$
2		bnj558.16	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
3		bnj558.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
4		bnj558.18	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
5		bnj558.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
6		bnj558.20	$⊢ ζ \leftrightarrow (i \in ω \land suc i \in n \land m = suc i)$
7		bnj558.21	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
8		bnj558.22	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
9		bnj558.23	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
10		bnj558.24	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
11		bnj558.25	$⊢ G = f \cup \{⟨m, C⟩\}$
12		bnj558.28	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
13		bnj558.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		bnj558.36	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	bnj557	$⊢ (R FrSe A \land τ \land η \land ζ) \to G (m) = L$
16		bnj422	$⊢ (R FrSe A \land τ \land η \land ζ) \leftrightarrow (η \land ζ \land R FrSe A \land τ)$
17		bnj253	$⊢ (η \land ζ \land R FrSe A \land τ) \leftrightarrow ((η \land ζ) \land R FrSe A \land τ)$
18	16 17	bitri	$⊢ (R FrSe A \land τ \land η \land ζ) \leftrightarrow ((η \land ζ) \land R FrSe A \land τ)$
19	18	simp1bi	$⊢ (R FrSe A \land τ \land η \land ζ) \to (η \land ζ)$
20	5 6 9 10 9 10	bnj554	$⊢ (η \land ζ) \to (G (m) = L \leftrightarrow G (suc i) = K)$
21	19 20	syl	$⊢ (R FrSe A \land τ \land η \land ζ) \to (G (m) = L \leftrightarrow G (suc i) = K)$
22	15 21	mpbid	$⊢ (R FrSe A \land τ \land η \land ζ) \to G (suc i) = K$

Metamath Proof Explorer

Theorem bnj558

Proof