bnj1020

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

Proof

Step	Hyp	Ref	Expression
1		bnj1020.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1020.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1020.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj1020.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
5		bnj1020.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
6		bnj1020.6	$⊢ η \leftrightarrow (i \in n \land y \in f (i))$
7		bnj1020.7	Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
8		bnj1020.8	Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
9		bnj1020.9	Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for \|- ( ch' <-> [. p / n ]. ch ) with typecode \|-
10		bnj1020.10	Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
11		bnj1020.11	Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
12		bnj1020.12	Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for \|- ( ch" <-> [. G / f ]. ch' ) with typecode \|-
13		bnj1020.13	$⊢ D = ω ∖ \{\emptyset\}$
14		bnj1020.14	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
15		bnj1020.15	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
16		bnj1020.16	$⊢ G = f \cup \{⟨n, C⟩\}$
17		bnj1020.26	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 \|-
18		bnj1019	$⊢ \exists p (θ \land χ \land τ \land η) \leftrightarrow (θ \land χ \land η \land \exists p τ)$
19	1 2 3 4 5 7 8 9 10 11 12 13 14 15 16	bnj998	Could not format ( ( th /\ ch /\ ta /\ et ) -> ch" ) : No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode \|-
20	3 5 6 13 19	bnj1001	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 \|-
21	1 2 3 4 5 6 7 8 9 10 11 12 13 15 16 20	bnj1006	$⊢ (θ \land χ \land τ \land η) \to pred (y, A, R) \subseteq G (suc i)$
22	21	exlimiv	$⊢ \exists p (θ \land χ \land τ \land η) \to pred (y, A, R) \subseteq G (suc i)$
23	18 22	sylbir	$⊢ (θ \land χ \land η \land \exists p τ) \to pred (y, A, R) \subseteq G (suc i)$
24	1 2 3 4 5 7 8 9 10 11 12 13 14 15 16 17 19 20	bnj1018	$⊢ (θ \land χ \land η \land \exists p τ) \to G (suc i) \subseteq trCl (X, A, R)$
25	23 24	sstrd	$⊢ (θ \land χ \land η \land \exists p τ) \to pred (y, A, R) \subseteq trCl (X, A, R)$

Metamath Proof Explorer

Theorem bnj1020

Proof