bnj999

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

Proof

Step	Hyp	Ref	Expression
1		bnj999.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj999.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj999.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj999.7	Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
5		bnj999.8	Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
6		bnj999.9	Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for \|- ( ch' <-> [. p / n ]. ch ) with typecode \|-
7		bnj999.10	Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
8		bnj999.11	Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
9		bnj999.12	Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for \|- ( ch" <-> [. G / f ]. ch' ) with typecode \|-
10		bnj999.15	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
11		bnj999.16	$⊢ G = f \cup \{⟨n, C⟩\}$
12		vex	$⊢ p \in V$
13	3 4 5 6 12	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 \|-
14	11	bnj918	$⊢ G \in V$
15	13 7 8 9 14	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 \|-
16	15	bnj1254	Could not format ( ch" -> ps" ) : No typesetting found for \|- ( ch" -> ps" ) with typecode \|-
17	16	anim1i	Could not format ( ( ch" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) -> ( ps" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) : No typesetting found for \|- ( ( ch" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) -> ( ps" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) with typecode \|-
18		bnj252	Could not format ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ch" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) : No typesetting found for \|- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ch" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) with typecode \|-
19		bnj252	Could not format ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ps" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) : No typesetting found for \|- ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ps" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) with typecode \|-
20	17 18 19	3imtr4i	Could not format ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) : No typesetting found for \|- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) with typecode \|-
21		ssiun2	$⊢ y \in G (i) \to pred (y, A, R) \subseteq ⋃_{y \in G (i)} pred (y, A, R)$
22	21	bnj708	Could not format ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ U_ y e. ( G ` i ) _pred ( y , A , R ) ) : No typesetting found for \|- ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ U_ y e. ( G ` i ) _pred ( y , A , R ) ) with typecode \|-
23		3simpa	Could not format ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( ps" /\ i e. _om ) ) : No typesetting found for \|- ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( ps" /\ i e. _om ) ) with typecode \|-
24	23	ancomd	Could not format ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( i e. _om /\ ps" ) ) : No typesetting found for \|- ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( i e. _om /\ ps" ) ) with typecode \|-
25		simp3	Could not format ( ( ps" /\ i e. _om /\ suc i e. p ) -> suc i e. p ) : No typesetting found for \|- ( ( ps" /\ i e. _om /\ suc i e. p ) -> suc i e. p ) with typecode \|-
26	2 5 12	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 \|-
27	26 8 10 11	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 \|-
28	27	bnj228	Could not format ( ( i e. _om /\ ps" ) -> ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ( i e. _om /\ ps" ) -> ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode \|-
29	24 25 28	sylc	Could not format ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) : No typesetting found for \|- ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) with typecode \|-
30	29	bnj721	Could not format ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) : No typesetting found for \|- ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) with typecode \|-
31	22 30	sseqtrrd	Could not format ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) : No typesetting found for \|- ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) with typecode \|-
32	20 31	syl	Could not format ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) : No typesetting found for \|- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) with typecode \|-

Metamath Proof Explorer

Theorem bnj999

Proof