bnj607

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	bnj607.5	$⊢ θ \leftrightarrow \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ)$
	bnj607.13	No typesetting found for \|- ( ph" <-> [. G / f ]. ph ) with typecode \|-
	bnj607.14	No typesetting found for \|- ( ps" <-> [. G / f ]. ps ) with typecode \|-
	bnj607.17	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj607.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
	bnj607.28	$⊢ G \in V$
	bnj607.31	No typesetting found for \|- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode \|-
	bnj607.32	No typesetting found for \|- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
	bnj607.33	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 \|-
	bnj607.37	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \exists p η$
	bnj607.38	No typesetting found for \|- ( ( th /\ m e. D /\ m _E n ) -> ch' ) with typecode \|-
	bnj607.41	$⊢ (R FrSe A \land τ \land η) \to G Fn n$
	bnj607.42	No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode \|-
	bnj607.43	No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode \|-
	bnj607.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
	bnj607.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj607.400	No typesetting found for \|- ( ph0 <-> [. h / f ]. ph ) with typecode \|-
	bnj607.401	No typesetting found for \|- ( ps0 <-> [. h / f ]. ps ) with typecode \|-
	bnj607.300	No typesetting found for \|- ( ph1 <-> [. G / h ]. ph0 ) with typecode \|-
	bnj607.301	No typesetting found for \|- ( ps1 <-> [. G / h ]. ps0 ) with typecode \|-
Assertion	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 ψ))$

Proof

Step	Hyp	Ref	Expression
1		bnj607.5	$⊢ θ \leftrightarrow \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ)$
2		bnj607.13	Could not format ( ph" <-> [. G / f ]. ph ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph ) with typecode \|-
3		bnj607.14	Could not format ( ps" <-> [. G / f ]. ps ) : No typesetting found for \|- ( ps" <-> [. G / f ]. ps ) with typecode \|-
4		bnj607.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
5		bnj607.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
6		bnj607.28	$⊢ G \in V$
7		bnj607.31	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 \|-
8		bnj607.32	Could not format ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
9		bnj607.33	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 \|-
10		bnj607.37	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \exists p η$
11		bnj607.38	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 \|-
12		bnj607.41	$⊢ (R FrSe A \land τ \land η) \to G Fn n$
13		bnj607.42	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ph" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode \|-
14		bnj607.43	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ps" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode \|-
15		bnj607.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (x, A, R)$
16		bnj607.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
17		bnj607.400	Could not format ( ph0 <-> [. h / f ]. ph ) : No typesetting found for \|- ( ph0 <-> [. h / f ]. ph ) with typecode \|-
18		bnj607.401	Could not format ( ps0 <-> [. h / f ]. ps ) : No typesetting found for \|- ( ps0 <-> [. h / f ]. ps ) with typecode \|-
19		bnj607.300	Could not format ( ph1 <-> [. G / h ]. ph0 ) : No typesetting found for \|- ( ph1 <-> [. G / h ]. ph0 ) with typecode \|-
20		bnj607.301	Could not format ( ps1 <-> [. G / h ]. ps0 ) : No typesetting found for \|- ( ps1 <-> [. G / h ]. ps0 ) with typecode \|-
21	10	anim1i	$⊢ ((n \neq 1_{𝑜} \land n \in D) \land θ) \to (\exists m \exists p η \land θ)$
22		nfv	$⊢ Ⅎ p θ$
23	22	19.41	$⊢ \exists p (η \land θ) \leftrightarrow (\exists p η \land θ)$
24	23	exbii	$⊢ \exists m \exists p (η \land θ) \leftrightarrow \exists m (\exists p η \land θ)$
25	1	bnj1095	$⊢ θ \to \forall m θ$
26	25	nf5i	$⊢ Ⅎ m θ$
27	26	19.41	$⊢ \exists m (\exists p η \land θ) \leftrightarrow (\exists m \exists p η \land θ)$
28	24 27	bitr2i	$⊢ (\exists m \exists p η \land θ) \leftrightarrow \exists m \exists p (η \land θ)$
29	21 28	sylib	$⊢ ((n \neq 1_{𝑜} \land n \in D) \land θ) \to \exists m \exists p (η \land θ)$
30	5	bnj1232	$⊢ η \to m \in D$
31		bnj219	$⊢ n = suc m \to m E n$
32	5 31	bnj770	$⊢ η \to m E n$
33	30 32	jca	$⊢ η \to (m \in D \land m E n)$
34	33	anim1i	$⊢ (η \land θ) \to ((m \in D \land m E n) \land θ)$
35		bnj170	$⊢ (θ \land m \in D \land m E n) \leftrightarrow ((m \in D \land m E n) \land θ)$
36	34 35	sylibr	$⊢ (η \land θ) \to (θ \land m \in D \land m E n)$
37	36 11	syl	Could not format ( ( et /\ th ) -> ch' ) : No typesetting found for \|- ( ( et /\ th ) -> ch' ) with typecode \|-
38		simpl	$⊢ (η \land θ) \to η$
39	37 38	jca	Could not format ( ( et /\ th ) -> ( ch' /\ et ) ) : No typesetting found for \|- ( ( et /\ th ) -> ( ch' /\ et ) ) with typecode \|-
40	39	2eximi	Could not format ( E. m E. p ( et /\ th ) -> E. m E. p ( ch' /\ et ) ) : No typesetting found for \|- ( E. m E. p ( et /\ th ) -> E. m E. p ( ch' /\ et ) ) with typecode \|-
41	7	biimpi	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 \|-
42		euex	Could not format ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
43	41 42	syl6	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 \|-
44	43	impcom	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
45	44 4	bnj1198	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ta ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ta ) with typecode \|-
46	45	adantrr	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ta ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ta ) with typecode \|-
47		id	$⊢ (R FrSe A \land τ \land η) \to (R FrSe A \land τ \land η)$
48	47	3com23	$⊢ (R FrSe A \land η \land τ) \to (R FrSe A \land τ \land η)$
49	48	3expia	$⊢ (R FrSe A \land η) \to (τ \to (R FrSe A \land τ \land η))$
50	49	eximdv	$⊢ (R FrSe A \land η) \to (\exists f τ \to \exists f (R FrSe A \land τ \land η))$
51	50	ad2ant2rl	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> ( E. f ta -> E. f ( R _FrSe A /\ ta /\ et ) ) ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> ( E. f ta -> E. f ( R _FrSe A /\ ta /\ et ) ) ) with typecode \|-
52	46 51	mpd	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ( R _FrSe A /\ ta /\ et ) ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ( R _FrSe A /\ ta /\ et ) ) with typecode \|-
53	12 13 14	3jca	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ( G Fn n /\ ph" /\ ps" ) ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ( G Fn n /\ ph" /\ ps" ) ) with typecode \|-
54	53	eximi	Could not format ( E. f ( R _FrSe A /\ ta /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) ) : No typesetting found for \|- ( E. f ( R _FrSe A /\ ta /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) ) with typecode \|-
55		nfe1	$⊢ Ⅎ f \exists f (f Fn n \land φ \land ψ)$
56		nfcv	$⊢ \underline{Ⅎ} h G$
57		nfv	$⊢ Ⅎ h G Fn n$
58		nfsbc1v	Could not format F/ h [. G / h ]. ph0 : No typesetting found for \|- F/ h [. G / h ]. ph0 with typecode \|-
59	19 58	nfxfr	Could not format F/ h ph1 : No typesetting found for \|- F/ h ph1 with typecode \|-
60		nfsbc1v	Could not format F/ h [. G / h ]. ps0 : No typesetting found for \|- F/ h [. G / h ]. ps0 with typecode \|-
61	20 60	nfxfr	Could not format F/ h ps1 : No typesetting found for \|- F/ h ps1 with typecode \|-
62	57 59 61	nf3an	Could not format F/ h ( G Fn n /\ ph1 /\ ps1 ) : No typesetting found for \|- F/ h ( G Fn n /\ ph1 /\ ps1 ) with typecode \|-
63		fneq1	$⊢ h = G \to (h Fn n \leftrightarrow G Fn n)$
64		sbceq1a	Could not format ( h = G -> ( ph0 <-> [. G / h ]. ph0 ) ) : No typesetting found for \|- ( h = G -> ( ph0 <-> [. G / h ]. ph0 ) ) with typecode \|-
65	64 19	bitr4di	Could not format ( h = G -> ( ph0 <-> ph1 ) ) : No typesetting found for \|- ( h = G -> ( ph0 <-> ph1 ) ) with typecode \|-
66		sbceq1a	Could not format ( h = G -> ( ps0 <-> [. G / h ]. ps0 ) ) : No typesetting found for \|- ( h = G -> ( ps0 <-> [. G / h ]. ps0 ) ) with typecode \|-
67	66 20	bitr4di	Could not format ( h = G -> ( ps0 <-> ps1 ) ) : No typesetting found for \|- ( h = G -> ( ps0 <-> ps1 ) ) with typecode \|-
68	63 65 67	3anbi123d	Could not format ( h = G -> ( ( h Fn n /\ ph0 /\ ps0 ) <-> ( G Fn n /\ ph1 /\ ps1 ) ) ) : No typesetting found for \|- ( h = G -> ( ( h Fn n /\ ph0 /\ ps0 ) <-> ( G Fn n /\ ph1 /\ ps1 ) ) ) with typecode \|-
69	56 62 68	spcegf	Could not format ( G e. _V -> ( ( G Fn n /\ ph1 /\ ps1 ) -> E. h ( h Fn n /\ ph0 /\ ps0 ) ) ) : No typesetting found for \|- ( G e. _V -> ( ( G Fn n /\ ph1 /\ ps1 ) -> E. h ( h Fn n /\ ph0 /\ ps0 ) ) ) with typecode \|-
70	6 69	ax-mp	Could not format ( ( G Fn n /\ ph1 /\ ps1 ) -> E. h ( h Fn n /\ ph0 /\ ps0 ) ) : No typesetting found for \|- ( ( G Fn n /\ ph1 /\ ps1 ) -> E. h ( h Fn n /\ ph0 /\ ps0 ) ) with typecode \|-
71	17 15	bnj154	Could not format ( ph0 <-> ( h ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph0 <-> ( h ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
72	71 19 6	bnj526	Could not format ( ph1 <-> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph1 <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
73	8 72	bitr4i	Could not format ( ph" <-> ph1 ) : No typesetting found for \|- ( ph" <-> ph1 ) with typecode \|-
74		vex	$⊢ h \in V$
75	16 18 74	bnj540	Could not format ( ps0 <-> A. i e. _om ( suc i e. n -> ( h ` suc i ) = U_ y e. ( h ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps0 <-> A. i e. _om ( suc i e. n -> ( h ` suc i ) = U_ y e. ( h ` i ) _pred ( y , A , R ) ) ) with typecode \|-
76	75 20 6	bnj540	Could not format ( ps1 <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps1 <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode \|-
77	9 76	bitr4i	Could not format ( ps" <-> ps1 ) : No typesetting found for \|- ( ps" <-> ps1 ) with typecode \|-
78	73 77	anbi12i	Could not format ( ( ph" /\ ps" ) <-> ( ph1 /\ ps1 ) ) : No typesetting found for \|- ( ( ph" /\ ps" ) <-> ( ph1 /\ ps1 ) ) with typecode \|-
79	78	anbi2i	Could not format ( ( G Fn n /\ ( ph" /\ ps" ) ) <-> ( G Fn n /\ ( ph1 /\ ps1 ) ) ) : No typesetting found for \|- ( ( G Fn n /\ ( ph" /\ ps" ) ) <-> ( G Fn n /\ ( ph1 /\ ps1 ) ) ) with typecode \|-
80		3anass	Could not format ( ( G Fn n /\ ph" /\ ps" ) <-> ( G Fn n /\ ( ph" /\ ps" ) ) ) : No typesetting found for \|- ( ( G Fn n /\ ph" /\ ps" ) <-> ( G Fn n /\ ( ph" /\ ps" ) ) ) with typecode \|-
81		3anass	Could not format ( ( G Fn n /\ ph1 /\ ps1 ) <-> ( G Fn n /\ ( ph1 /\ ps1 ) ) ) : No typesetting found for \|- ( ( G Fn n /\ ph1 /\ ps1 ) <-> ( G Fn n /\ ( ph1 /\ ps1 ) ) ) with typecode \|-
82	79 80 81	3bitr4i	Could not format ( ( G Fn n /\ ph" /\ ps" ) <-> ( G Fn n /\ ph1 /\ ps1 ) ) : No typesetting found for \|- ( ( G Fn n /\ ph" /\ ps" ) <-> ( G Fn n /\ ph1 /\ ps1 ) ) with typecode \|-
83		nfv	$⊢ Ⅎ h (f Fn n \land φ \land ψ)$
84		nfv	$⊢ Ⅎ f h Fn n$
85		nfsbc1v	$⊢ Ⅎ f \underset{˙}{[} h / f \underset{˙}{]} φ$
86	17 85	nfxfr	Could not format F/ f ph0 : No typesetting found for \|- F/ f ph0 with typecode \|-
87		nfsbc1v	$⊢ Ⅎ f \underset{˙}{[} h / f \underset{˙}{]} ψ$
88	18 87	nfxfr	Could not format F/ f ps0 : No typesetting found for \|- F/ f ps0 with typecode \|-
89	84 86 88	nf3an	Could not format F/ f ( h Fn n /\ ph0 /\ ps0 ) : No typesetting found for \|- F/ f ( h Fn n /\ ph0 /\ ps0 ) with typecode \|-
90		fneq1	$⊢ f = h \to (f Fn n \leftrightarrow h Fn n)$
91		sbceq1a	$⊢ f = h \to (φ \leftrightarrow \underset{˙}{[} h / f \underset{˙}{]} φ)$
92	91 17	bitr4di	Could not format ( f = h -> ( ph <-> ph0 ) ) : No typesetting found for \|- ( f = h -> ( ph <-> ph0 ) ) with typecode \|-
93		sbceq1a	$⊢ f = h \to (ψ \leftrightarrow \underset{˙}{[} h / f \underset{˙}{]} ψ)$
94	93 18	bitr4di	Could not format ( f = h -> ( ps <-> ps0 ) ) : No typesetting found for \|- ( f = h -> ( ps <-> ps0 ) ) with typecode \|-
95	90 92 94	3anbi123d	Could not format ( f = h -> ( ( f Fn n /\ ph /\ ps ) <-> ( h Fn n /\ ph0 /\ ps0 ) ) ) : No typesetting found for \|- ( f = h -> ( ( f Fn n /\ ph /\ ps ) <-> ( h Fn n /\ ph0 /\ ps0 ) ) ) with typecode \|-
96	83 89 95	cbvexv1	Could not format ( E. f ( f Fn n /\ ph /\ ps ) <-> E. h ( h Fn n /\ ph0 /\ ps0 ) ) : No typesetting found for \|- ( E. f ( f Fn n /\ ph /\ ps ) <-> E. h ( h Fn n /\ ph0 /\ ps0 ) ) with typecode \|-
97	70 82 96	3imtr4i	Could not format ( ( G Fn n /\ ph" /\ ps" ) -> E. f ( f Fn n /\ ph /\ ps ) ) : No typesetting found for \|- ( ( G Fn n /\ ph" /\ ps" ) -> E. f ( f Fn n /\ ph /\ ps ) ) with typecode \|-
98	55 97	exlimi	Could not format ( E. f ( G Fn n /\ ph" /\ ps" ) -> E. f ( f Fn n /\ ph /\ ps ) ) : No typesetting found for \|- ( E. f ( G Fn n /\ ph" /\ ps" ) -> E. f ( f Fn n /\ ph /\ ps ) ) with typecode \|-
99	52 54 98	3syl	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ( f Fn n /\ ph /\ ps ) ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ( f Fn n /\ ph /\ ps ) ) with typecode \|-
100	99	expcom	Could not format ( ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for \|- ( ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) ) with typecode \|-
101	100	exlimivv	Could not format ( E. m E. p ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for \|- ( E. m E. p ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) ) with typecode \|-
102	29 40 101	3syl	$⊢ ((n \neq 1_{𝑜} \land n \in D) \land θ) \to ((R FrSe A \land x \in A) \to \exists f (f Fn n \land φ \land ψ))$
103	102	3impa	$⊢ (n \neq 1_{𝑜} \land n \in D \land θ) \to ((R FrSe A \land x \in A) \to \exists f (f Fn n \land φ \land ψ))$

Metamath Proof Explorer

Theorem bnj607

Proof