bnj1006

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	bnj1006.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj1006.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj1006.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj1006.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
	bnj1006.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
	bnj1006.6	$⊢ η \leftrightarrow (i \in n \land y \in f (i))$
	bnj1006.7	No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
	bnj1006.8	No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
	bnj1006.9	No typesetting found for \|- ( ch' <-> [. p / n ]. ch ) with typecode \|-
	bnj1006.10	No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
	bnj1006.11	No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
	bnj1006.12	No typesetting found for \|- ( ch" <-> [. G / f ]. ch' ) with typecode \|-
	bnj1006.13	$⊢ D = ω ∖ \{\emptyset\}$
	bnj1006.15	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
	bnj1006.16	$⊢ G = f \cup \{⟨n, C⟩\}$
	bnj1006.28	No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode \|-
Assertion	bnj1006	$⊢ (θ \land χ \land τ \land η) \to pred (y, A, R) \subseteq G (suc i)$

Proof

Step	Hyp	Ref	Expression
1		bnj1006.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1006.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1006.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj1006.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
5		bnj1006.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
6		bnj1006.6	$⊢ η \leftrightarrow (i \in n \land y \in f (i))$
7		bnj1006.7	Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
8		bnj1006.8	Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
9		bnj1006.9	Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for \|- ( ch' <-> [. p / n ]. ch ) with typecode \|-
10		bnj1006.10	Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
11		bnj1006.11	Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
12		bnj1006.12	Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for \|- ( ch" <-> [. G / f ]. ch' ) with typecode \|-
13		bnj1006.13	$⊢ D = ω ∖ \{\emptyset\}$
14		bnj1006.15	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
15		bnj1006.16	$⊢ G = f \cup \{⟨n, C⟩\}$
16		bnj1006.28	Could not format ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) : No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode \|-
17	6	simprbi	$⊢ η \to y \in f (i)$
18	17	bnj708	$⊢ (θ \land χ \land τ \land η) \to y \in f (i)$
19		bnj253	$⊢ (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \leftrightarrow ((R FrSe A \land X \in A) \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
20	19	simp1bi	$⊢ (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \to (R FrSe A \land X \in A)$
21	4 20	sylbi	$⊢ θ \to (R FrSe A \land X \in A)$
22	21	bnj705	$⊢ (θ \land χ \land τ \land η) \to (R FrSe A \land X \in A)$
23		bnj643	$⊢ (θ \land χ \land τ \land η) \to χ$
24		3simpc	$⊢ (m \in ω \land n = suc m \land p = suc n) \to (n = suc m \land p = suc n)$
25	5 24	sylbi	$⊢ τ \to (n = suc m \land p = suc n)$
26	25	bnj707	$⊢ (θ \land χ \land τ \land η) \to (n = suc m \land p = suc n)$
27		3anass	$⊢ (χ \land n = suc m \land p = suc n) \leftrightarrow (χ \land (n = suc m \land p = suc n))$
28	23 26 27	sylanbrc	$⊢ (θ \land χ \land τ \land η) \to (χ \land n = suc m \land p = suc n)$
29		biid	$⊢ (f Fn n \land φ \land ψ) \leftrightarrow (f Fn n \land φ \land ψ)$
30		biid	$⊢ (n \in D \land p = suc n \land m \in n) \leftrightarrow (n \in D \land p = suc n \land m \in n)$
31	1 2 3 13 14 29 30	bnj969	$⊢ ((R FrSe A \land X \in A) \land (χ \land n = suc m \land p = suc n)) \to C \in V$
32	22 28 31	syl2anc	$⊢ (θ \land χ \land τ \land η) \to C \in V$
33	3	bnj1235	$⊢ χ \to f Fn n$
34	33	bnj706	$⊢ (θ \land χ \land τ \land η) \to f Fn n$
35	5	simp3bi	$⊢ τ \to p = suc n$
36	35	bnj707	$⊢ (θ \land χ \land τ \land η) \to p = suc n$
37	6	simplbi	$⊢ η \to i \in n$
38	37	bnj708	$⊢ (θ \land χ \land τ \land η) \to i \in n$
39	32 34 36 38	bnj951	$⊢ (θ \land χ \land τ \land η) \to (C \in V \land f Fn n \land p = suc n \land i \in n)$
40	15	bnj945	$⊢ (C \in V \land f Fn n \land p = suc n \land i \in n) \to G (i) = f (i)$
41	39 40	syl	$⊢ (θ \land χ \land τ \land η) \to G (i) = f (i)$
42	18 41	eleqtrrd	$⊢ (θ \land χ \land τ \land η) \to y \in G (i)$
43	16	anim1i	Could not format ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ( ch" /\ i e. _om /\ suc i e. p ) /\ y e. ( G ` i ) ) ) : No typesetting found for \|- ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ( ch" /\ i e. _om /\ suc i e. p ) /\ y e. ( G ` i ) ) ) with typecode \|-
44		df-bnj17	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 \|-
45	43 44	sylibr	Could not format ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) : No typesetting found for \|- ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) with typecode \|-
46	1 2 3 7 8 9 10 11 12 14 15	bnj999	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 \|-
47	45 46	syl	$⊢ ((θ \land χ \land τ \land η) \land y \in G (i)) \to pred (y, A, R) \subseteq G (suc i)$
48	42 47	mpdan	$⊢ (θ \land χ \land τ \land η) \to pred (y, A, R) \subseteq G (suc i)$

Metamath Proof Explorer

Theorem bnj1006

Proof