bnj910

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	bnj910.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj910.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj910.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj910.4	No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
	bnj910.5	No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
	bnj910.6	No typesetting found for \|- ( ch' <-> [. p / n ]. ch ) with typecode \|-
	bnj910.7	No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
	bnj910.8	No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
	bnj910.9	No typesetting found for \|- ( ch" <-> [. G / f ]. ch' ) with typecode \|-
	bnj910.10	$⊢ D = ω ∖ \{\emptyset\}$
	bnj910.11	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
	bnj910.12	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
	bnj910.13	$⊢ G = f \cup \{⟨n, C⟩\}$
	bnj910.14	$⊢ τ \leftrightarrow (f Fn n \land φ \land ψ)$
	bnj910.15	$⊢ σ \leftrightarrow (n \in D \land p = suc n \land m \in n)$
Assertion	bnj910	Could not format assertion : No typesetting found for \|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj910.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj910.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj910.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj910.4	Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
5		bnj910.5	Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
6		bnj910.6	Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for \|- ( ch' <-> [. p / n ]. ch ) with typecode \|-
7		bnj910.7	Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
8		bnj910.8	Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
9		bnj910.9	Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for \|- ( ch" <-> [. G / f ]. ch' ) with typecode \|-
10		bnj910.10	$⊢ D = ω ∖ \{\emptyset\}$
11		bnj910.11	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
12		bnj910.12	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
13		bnj910.13	$⊢ G = f \cup \{⟨n, C⟩\}$
14		bnj910.14	$⊢ τ \leftrightarrow (f Fn n \land φ \land ψ)$
15		bnj910.15	$⊢ σ \leftrightarrow (n \in D \land p = suc n \land m \in n)$
16	3 10	bnj970	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to p \in D$
17	1 2 3 10 12 14 15	bnj969	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to C \in V$
18		simpr3	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to p = suc n$
19	3	bnj1235	$⊢ χ \to f Fn n$
20	19	3ad2ant1	$⊢ (χ \land n = suc m \land p = suc n) \to f Fn n$
21	20	adantl	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to f Fn n$
22	13	bnj941	$⊢ C \in V \to ((p = suc n \land f Fn n) \to G Fn p)$
23	22	3impib	$⊢ (C \in V \land p = suc n \land f Fn n) \to G Fn p$
24	17 18 21 23	syl3anc	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to G Fn p$
25	1 2 3 4 7 10 12 13 14 15	bnj944	Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) : No typesetting found for \|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) with typecode \|-
26	2 3 10 12 13 17	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)$
27	3 10 12 13 17 24	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)$
28	2 3 5 8 12 13 26 27	bnj964	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 \|-
29	16 24 25 28	bnj951	Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for \|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode \|-
30		vex	$⊢ p \in V$
31	3 4 5 6 30	bnj919	Could not format ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) ) with typecode \|-
32	13	bnj918	$⊢ G \in V$
33	31 7 8 9 32	bnj976	Could not format ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for \|- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode \|-
34	29 33	sylibr	Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) : No typesetting found for \|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) with typecode \|-

Metamath Proof Explorer

Theorem bnj910

Proof