bnj600

Description: Technical lemma for bnj852 . 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	bnj600.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
	bnj600.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj600.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj600.4	$⊢ χ \leftrightarrow ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land φ \land ψ))$
	bnj600.5	$⊢ θ \leftrightarrow \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ)$
	bnj600.10	No typesetting found for \|- ( ph' <-> [. m / n ]. ph ) with typecode \|-
	bnj600.11	No typesetting found for \|- ( ps' <-> [. m / n ]. ps ) with typecode \|-
	bnj600.12	No typesetting found for \|- ( ch' <-> [. m / n ]. ch ) with typecode \|-
	bnj600.13	No typesetting found for \|- ( ph" <-> [. G / f ]. ph ) with typecode \|-
	bnj600.14	No typesetting found for \|- ( ps" <-> [. G / f ]. ps ) with typecode \|-
	bnj600.15	No typesetting found for \|- ( ch" <-> [. G / f ]. ch ) with typecode \|-
	bnj600.16	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
	bnj600.17	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj600.18	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
	bnj600.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
	bnj600.20	$⊢ ζ \leftrightarrow (i \in ω \land suc i \in n \land m = suc i)$
	bnj600.21	$⊢ ρ \leftrightarrow (i \in ω \land suc i \in n \land m \neq suc i)$
	bnj600.22	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
	bnj600.23	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
	bnj600.24	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
	bnj600.25	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
	bnj600.26	$⊢ G = f \cup \{⟨m, C⟩\}$
Assertion	bnj600	$⊢ n \neq 1_{𝑜} \to ((n \in D \land θ) \to χ)$

Proof

Step	Hyp	Ref	Expression
1		bnj600.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
2		bnj600.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj600.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj600.4	$⊢ χ \leftrightarrow ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land φ \land ψ))$
5		bnj600.5	$⊢ θ \leftrightarrow \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ)$
6		bnj600.10	Could not format ( ph' <-> [. m / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. m / n ]. ph ) with typecode \|-
7		bnj600.11	Could not format ( ps' <-> [. m / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. m / n ]. ps ) with typecode \|-
8		bnj600.12	Could not format ( ch' <-> [. m / n ]. ch ) : No typesetting found for \|- ( ch' <-> [. m / n ]. ch ) with typecode \|-
9		bnj600.13	Could not format ( ph" <-> [. G / f ]. ph ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph ) with typecode \|-
10		bnj600.14	Could not format ( ps" <-> [. G / f ]. ps ) : No typesetting found for \|- ( ps" <-> [. G / f ]. ps ) with typecode \|-
11		bnj600.15	Could not format ( ch" <-> [. G / f ]. ch ) : No typesetting found for \|- ( ch" <-> [. G / f ]. ch ) with typecode \|-
12		bnj600.16	$⊢ G = f \cup \{⟨m, ⋃_{y \in f (p)} pred (y, A, R)⟩\}$
13		bnj600.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
14		bnj600.18	$⊢ σ \leftrightarrow (m \in D \land n = suc m \land p \in m)$
15		bnj600.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
16		bnj600.20	$⊢ ζ \leftrightarrow (i \in ω \land suc i \in n \land m = suc i)$
17		bnj600.21	$⊢ ρ \leftrightarrow (i \in ω \land suc i \in n \land m \neq suc i)$
18		bnj600.22	$⊢ B = ⋃_{y \in f (i)} pred (y, A, R)$
19		bnj600.23	$⊢ C = ⋃_{y \in f (p)} pred (y, A, R)$
20		bnj600.24	$⊢ K = ⋃_{y \in G (i)} pred (y, A, R)$
21		bnj600.25	$⊢ L = ⋃_{y \in G (p)} pred (y, A, R)$
22		bnj600.26	$⊢ G = f \cup \{⟨m, C⟩\}$
23	12	bnj528	$⊢ G \in V$
24		vex	$⊢ m \in V$
25	4 6 7 8 24	bnj207	Could not format ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode \|-
26	1 9 23	bnj609	Could not format ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
27	2 10 23	bnj611	Could not format ( ps" <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps" <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode \|-
28	3	bnj168	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \in D n = suc m$
29		df-rex	$⊢ \exists m \in D n = suc m \leftrightarrow \exists m (m \in D \land n = suc m)$
30	28 29	sylib	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m (m \in D \land n = suc m)$
31	3	bnj158	$⊢ m \in D \to \exists p \in ω m = suc p$
32		df-rex	$⊢ \exists p \in ω m = suc p \leftrightarrow \exists p (p \in ω \land m = suc p)$
33	31 32	sylib	$⊢ m \in D \to \exists p (p \in ω \land m = suc p)$
34	33	adantr	$⊢ (m \in D \land n = suc m) \to \exists p (p \in ω \land m = suc p)$
35	34	ancri	$⊢ (m \in D \land n = suc m) \to (\exists p (p \in ω \land m = suc p) \land (m \in D \land n = suc m))$
36	35	bnj534	$⊢ (m \in D \land n = suc m) \to \exists p ((p \in ω \land m = suc p) \land (m \in D \land n = suc m))$
37		bnj432	$⊢ (m \in D \land n = suc m \land p \in ω \land m = suc p) \leftrightarrow ((p \in ω \land m = suc p) \land (m \in D \land n = suc m))$
38	37	exbii	$⊢ \exists p (m \in D \land n = suc m \land p \in ω \land m = suc p) \leftrightarrow \exists p ((p \in ω \land m = suc p) \land (m \in D \land n = suc m))$
39	36 38	sylibr	$⊢ (m \in D \land n = suc m) \to \exists p (m \in D \land n = suc m \land p \in ω \land m = suc p)$
40	39	eximi	$⊢ \exists m (m \in D \land n = suc m) \to \exists m \exists p (m \in D \land n = suc m \land p \in ω \land m = suc p)$
41	30 40	syl	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \exists p (m \in D \land n = suc m \land p \in ω \land m = suc p)$
42	15	2exbii	$⊢ \exists m \exists p η \leftrightarrow \exists m \exists p (m \in D \land n = suc m \land p \in ω \land m = suc p)$
43	41 42	sylibr	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \exists p η$
44		rsp	$⊢ \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ) \to (m \in D \to (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ))$
45	5 44	sylbi	$⊢ θ \to (m \in D \to (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ))$
46	45	3imp	$⊢ (θ \land m \in D \land m E n) \to \underset{˙}{[} m / n \underset{˙}{]} χ$
47	46 8	sylibr	Could not format ( ( th /\ m e. D /\ m _E n ) -> ch' ) : No typesetting found for \|- ( ( th /\ m e. D /\ m _E n ) -> ch' ) with typecode \|-
48	1 6 24	bnj523	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
49	2 7 24	bnj539	Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode \|-
50	48 49 3 12 13 14	bnj544	$⊢ (R FrSe A \land τ \land σ) \to G Fn n$
51	14 15 50	bnj561	$⊢ (R FrSe A \land τ \land η) \to G Fn n$
52	48 3 12 13 14 50 26	bnj545	Could not format ( ( R _FrSe A /\ ta /\ si ) -> ph" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ si ) -> ph" ) with typecode \|-
53	14 15 52	bnj562	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ph" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode \|-
54	3 12 13 14 15 16 18 19 20 21 22 48 49 50 17 51 27	bnj571	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ps" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode \|-
55		biid	$⊢ \underset{˙}{[} z / f \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} z / f \underset{˙}{]} φ$
56		biid	$⊢ \underset{˙}{[} z / f \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} z / f \underset{˙}{]} ψ$
57		biid	$⊢ \underset{˙}{[} G / z \underset{˙}{]} \underset{˙}{[} z / f \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} G / z \underset{˙}{]} \underset{˙}{[} z / f \underset{˙}{]} φ$
58		biid	$⊢ \underset{˙}{[} G / z \underset{˙}{]} \underset{˙}{[} z / f \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} G / z \underset{˙}{]} \underset{˙}{[} z / f \underset{˙}{]} ψ$
59	5 9 10 13 15 23 25 26 27 43 47 51 53 54 1 2 55 56 57 58	bnj607	$⊢ (n \neq 1_{𝑜} \land n \in D \land θ) \to ((R FrSe A \land x \in A) \to \exists f (f Fn n \land φ \land ψ))$
60	1 2 3	bnj579	$⊢ n \in D \to \exists^{*} f (f Fn n \land φ \land ψ)$
61	60	a1d	$⊢ n \in D \to ((R FrSe A \land x \in A) \to \exists^{*} f (f Fn n \land φ \land ψ))$
62	61	3ad2ant2	$⊢ (n \neq 1_{𝑜} \land n \in D \land θ) \to ((R FrSe A \land x \in A) \to \exists^{*} f (f Fn n \land φ \land ψ))$
63	59 62	jcad	$⊢ (n \neq 1_{𝑜} \land n \in D \land θ) \to ((R FrSe A \land x \in A) \to (\exists f (f Fn n \land φ \land ψ) \land \exists^{*} f (f Fn n \land φ \land ψ)))$
64		df-eu	$⊢ \exists! f (f Fn n \land φ \land ψ) \leftrightarrow (\exists f (f Fn n \land φ \land ψ) \land \exists^{*} f (f Fn n \land φ \land ψ))$
65	63 64	syl6ibr	$⊢ (n \neq 1_{𝑜} \land n \in D \land θ) \to ((R FrSe A \land x \in A) \to \exists! f (f Fn n \land φ \land ψ))$
66	65 4	sylibr	$⊢ (n \neq 1_{𝑜} \land n \in D \land θ) \to χ$
67	66	3expib	$⊢ n \neq 1_{𝑜} \to ((n \in D \land θ) \to χ)$

Metamath Proof Explorer

Theorem bnj600

Proof