bnj908

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	bnj908.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
	bnj908.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj908.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj908.4	$⊢ χ \leftrightarrow ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land φ \land ψ))$
	bnj908.5	$⊢ θ \leftrightarrow \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ)$
	bnj908.10	No typesetting found for \|- ( ph' <-> [. m / n ]. ph ) with typecode \|-
	bnj908.11	No typesetting found for \|- ( ps' <-> [. m / n ]. ps ) with typecode \|-
	bnj908.12	No typesetting found for \|- ( ch' <-> [. m / n ]. ch ) with typecode \|-
	bnj908.13	No typesetting found for \|- ( ph" <-> [. G / f ]. ph ) with typecode \|-
	bnj908.14	No typesetting found for \|- ( ps" <-> [. G / f ]. ps ) with typecode \|-
	bnj908.15	No typesetting found for \|- ( ch" <-> [. G / f ]. ch ) with typecode \|-
	bnj908.16	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
	bnj908.17	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj908.18	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
	bnj908.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
	bnj908.20	$⊢ ζ \leftrightarrow (i \in ω \land suc i \in n \land m = suc i)$
	bnj908.21	$⊢ ρ \leftrightarrow (i \in ω \land suc i \in n \land m \neq suc i)$
	bnj908.22	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
	bnj908.23	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
	bnj908.24	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
	bnj908.25	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
	bnj908.26	$⊢ G = f \cup \{⟨m, C⟩\}$
Assertion	bnj908	Could not format assertion : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj908.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
2		bnj908.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj908.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj908.4	$⊢ χ \leftrightarrow ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land φ \land ψ))$
5		bnj908.5	$⊢ θ \leftrightarrow \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ)$
6		bnj908.10	Could not format ( ph' <-> [. m / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. m / n ]. ph ) with typecode \|-
7		bnj908.11	Could not format ( ps' <-> [. m / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. m / n ]. ps ) with typecode \|-
8		bnj908.12	Could not format ( ch' <-> [. m / n ]. ch ) : No typesetting found for \|- ( ch' <-> [. m / n ]. ch ) with typecode \|-
9		bnj908.13	Could not format ( ph" <-> [. G / f ]. ph ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph ) with typecode \|-
10		bnj908.14	Could not format ( ps" <-> [. G / f ]. ps ) : No typesetting found for \|- ( ps" <-> [. G / f ]. ps ) with typecode \|-
11		bnj908.15	Could not format ( ch" <-> [. G / f ]. ch ) : No typesetting found for \|- ( ch" <-> [. G / f ]. ch ) with typecode \|-
12		bnj908.16	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
13		bnj908.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
14		bnj908.18	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
15		bnj908.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
16		bnj908.20	$⊢ ζ \leftrightarrow (i \in ω \land suc i \in n \land m = suc i)$
17		bnj908.21	$⊢ ρ \leftrightarrow (i \in ω \land suc i \in n \land m \neq suc i)$
18		bnj908.22	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
19		bnj908.23	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
20		bnj908.24	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
21		bnj908.25	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
22		bnj908.26	$⊢ G = f \cup \{⟨m, C⟩\}$
23		bnj248	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) ) with typecode \|-
24		vex	$⊢ m \in V$
25	4 6 7 8 24	bnj207	Could not format ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode \|-
26	25	biimpi	Could not format ( ch' -> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( ch' -> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode \|-
27		euex	Could not format ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
28	26 27	syl6	Could not format ( ch' -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( ch' -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode \|-
29	28	impcom	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
30	29 13	bnj1198	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ta ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ta ) with typecode \|-
31	23 30	bnj832	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ta ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ta ) with typecode \|-
32		bnj645	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> et ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> et ) with typecode \|-
33		19.41v	$⊢ \exists f (τ \land η) \leftrightarrow (\exists f τ \land η)$
34	31 32 33	sylanbrc	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( ta /\ et ) ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( ta /\ et ) ) with typecode \|-
35		bnj642	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> R _FrSe A ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> R _FrSe A ) with typecode \|-
36		19.41v	$⊢ \exists f ((τ \land η) \land R FrSe A) \leftrightarrow (\exists f (τ \land η) \land R FrSe A)$
37	34 35 36	sylanbrc	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( ( ta /\ et ) /\ R _FrSe A ) ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( ( ta /\ et ) /\ R _FrSe A ) ) with typecode \|-
38		bnj170	$⊢ (R FrSe A \land τ \land η) \leftrightarrow ((τ \land η) \land R FrSe A)$
39	37 38	bnj1198	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( R _FrSe A /\ ta /\ et ) ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( R _FrSe A /\ ta /\ et ) ) with typecode \|-
40	1 6 24	bnj523	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
41	2 7 24	bnj539	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 \|-
42	40 41 3 12 13 14	bnj544	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
43	14 15 42	bnj561	$⊢ (R FrSe A \land τ \land η) \to G Fn n$
44	12	bnj528	$⊢ G \in V$
45	1 9 44	bnj609	Could not format ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
46	40 3 12 13 14 42 45	bnj545	Could not format ( ( R _FrSe A /\ ta /\ si ) -> ph" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ si ) -> ph" ) with typecode \|-
47	14 15 46	bnj562	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ph" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode \|-
48	2 10 44	bnj611	Could not format ( ps" <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps" <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode \|-
49	3 12 13 14 15 16 18 19 20 21 22 40 41 42 17 43 48	bnj571	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ps" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode \|-
50	43 47 49	3jca	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ( G Fn n /\ ph" /\ ps" ) ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ( G Fn n /\ ph" /\ ps" ) ) with typecode \|-
51	39 50	bnj593	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) ) with typecode \|-

Metamath Proof Explorer

Theorem bnj908

Proof