bnj998

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

Proof

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

Metamath Proof Explorer

Theorem bnj998

Proof