bnj907

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

Proof

Step	Hyp	Ref	Expression
1		bnj907.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj907.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj907.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj907.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
5		bnj907.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
6		bnj907.6	$⊢ η \leftrightarrow (i \in n \land y \in f (i))$
7		bnj907.7	Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
8		bnj907.8	Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
9		bnj907.9	Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for \|- ( ch' <-> [. p / n ]. ch ) with typecode \|-
10		bnj907.10	Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
11		bnj907.11	Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
12		bnj907.12	Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for \|- ( ch" <-> [. G / f ]. ch' ) with typecode \|-
13		bnj907.13	$⊢ D = ω ∖ \{\emptyset\}$
14		bnj907.14	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
15		bnj907.15	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
16		bnj907.16	$⊢ G = f \cup \{⟨n, C⟩\}$
17	1 2 3 4 5 6 13 14	bnj1021	$⊢ \exists f \exists n \exists i \exists m (θ \to (θ \land χ \land η \land \exists p τ))$
18		vex	$⊢ p \in V$
19	3 7 8 9 18	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 \|-
20	16	bnj918	$⊢ G \in V$
21	19 10 11 12 20	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 \|-
22	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 21	bnj1020	$⊢ (θ \land χ \land η \land \exists p τ) \to pred (y, A, R) \subseteq trCl (X, A, R)$
23	22	ax-gen	$⊢ \forall m ((θ \land χ \land η \land \exists p τ) \to pred (y, A, R) \subseteq trCl (X, A, R))$
24		19.29r	$⊢ (\exists m (θ \to (θ \land χ \land η \land \exists p τ)) \land \forall m ((θ \land χ \land η \land \exists p τ) \to pred (y, A, R) \subseteq trCl (X, A, R))) \to \exists m ((θ \to (θ \land χ \land η \land \exists p τ)) \land ((θ \land χ \land η \land \exists p τ) \to pred (y, A, R) \subseteq trCl (X, A, R)))$
25		pm3.33	$⊢ ((θ \to (θ \land χ \land η \land \exists p τ)) \land ((θ \land χ \land η \land \exists p τ) \to pred (y, A, R) \subseteq trCl (X, A, R))) \to (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
26	24 25	bnj593	$⊢ (\exists m (θ \to (θ \land χ \land η \land \exists p τ)) \land \forall m ((θ \land χ \land η \land \exists p τ) \to pred (y, A, R) \subseteq trCl (X, A, R))) \to \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
27	23 26	mpan2	$⊢ \exists m (θ \to (θ \land χ \land η \land \exists p τ)) \to \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
28	27	2eximi	$⊢ \exists n \exists i \exists m (θ \to (θ \land χ \land η \land \exists p τ)) \to \exists n \exists i \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
29	17 28	bnj101	$⊢ \exists f \exists n \exists i \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
30		19.9v	$⊢ \exists f \exists n \exists i \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R)) \leftrightarrow \exists n \exists i \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
31	29 30	mpbi	$⊢ \exists n \exists i \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
32		19.9v	$⊢ \exists n \exists i \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R)) \leftrightarrow \exists i \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
33	31 32	mpbi	$⊢ \exists i \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
34		19.9v	$⊢ \exists i \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R)) \leftrightarrow \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
35	33 34	mpbi	$⊢ \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
36		19.9v	$⊢ \exists m (θ \to pred (y, A, R) \subseteq trCl (X, A, R)) \leftrightarrow (θ \to pred (y, A, R) \subseteq trCl (X, A, R))$
37	35 36	mpbi	$⊢ θ \to pred (y, A, R) \subseteq trCl (X, A, R)$
38	4	bnj1254	$⊢ θ \to z \in pred (y, A, R)$
39	37 38	sseldd	$⊢ θ \to z \in trCl (X, A, R)$
40	4 39	bnj978	$⊢ (R FrSe A \land X \in A) \to TrFo (trCl (X, A, R), A, R)$

Metamath Proof Explorer

Theorem bnj907

Proof