bnj605

Description: Technical lemma. 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	bnj605.5	$⊢ θ \leftrightarrow \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ)$
	bnj605.13	No typesetting found for \|- ( ph" <-> [. f / f ]. ph ) with typecode \|-
	bnj605.14	No typesetting found for \|- ( ps" <-> [. f / f ]. ps ) with typecode \|-
	bnj605.17	No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
	bnj605.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
	bnj605.28	$⊢ f \in V$
	bnj605.31	No typesetting found for \|- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode \|-
	bnj605.32	No typesetting found for \|- ( ph" <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
	bnj605.33	No typesetting found for \|- ( ps" <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode \|-
	bnj605.37	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \exists p η$
	bnj605.38	No typesetting found for \|- ( ( th /\ m e. D /\ m _E n ) -> ch' ) with typecode \|-
	bnj605.41	$⊢ (R FrSe A \land τ \land η) \to f Fn n$
	bnj605.42	No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode \|-
	bnj605.43	No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode \|-
Assertion	bnj605	$⊢ (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		bnj605.5	$⊢ θ \leftrightarrow \forall m \in D (m E n \to \underset{˙}{[} m / n \underset{˙}{]} χ)$
2		bnj605.13	Could not format ( ph" <-> [. f / f ]. ph ) : No typesetting found for \|- ( ph" <-> [. f / f ]. ph ) with typecode \|-
3		bnj605.14	Could not format ( ps" <-> [. f / f ]. ps ) : No typesetting found for \|- ( ps" <-> [. f / f ]. ps ) with typecode \|-
4		bnj605.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
5		bnj605.19	$⊢ η \leftrightarrow (m \in D \land n = suc m \land p \in ω \land m = suc p)$
6		bnj605.28	$⊢ f \in V$
7		bnj605.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		bnj605.32	Could not format ( ph" <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for \|- ( ph" <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode \|-
9		bnj605.33	Could not format ( ps" <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for \|- ( ps" <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode \|-
10		bnj605.37	$⊢ (n \neq 1_{𝑜} \land n \in D) \to \exists m \exists p η$
11		bnj605.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		bnj605.41	$⊢ (R FrSe A \land τ \land η) \to f Fn n$
13		bnj605.42	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ph" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode \|-
14		bnj605.43	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ps" ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode \|-
15	10	anim1i	$⊢ ((n \neq 1_{𝑜} \land n \in D) \land θ) \to (\exists m \exists p η \land θ)$
16		nfv	$⊢ Ⅎ p θ$
17	16	19.41	$⊢ \exists p (η \land θ) \leftrightarrow (\exists p η \land θ)$
18	17	exbii	$⊢ \exists m \exists p (η \land θ) \leftrightarrow \exists m (\exists p η \land θ)$
19	1	bnj1095	$⊢ θ \to \forall m θ$
20	19	nf5i	$⊢ Ⅎ m θ$
21	20	19.41	$⊢ \exists m (\exists p η \land θ) \leftrightarrow (\exists m \exists p η \land θ)$
22	18 21	bitr2i	$⊢ (\exists m \exists p η \land θ) \leftrightarrow \exists m \exists p (η \land θ)$
23	15 22	sylib	$⊢ ((n \neq 1_{𝑜} \land n \in D) \land θ) \to \exists m \exists p (η \land θ)$
24	5	bnj1232	$⊢ η \to m \in D$
25		bnj219	$⊢ n = suc m \to m E n$
26	5 25	bnj770	$⊢ η \to m E n$
27	24 26	jca	$⊢ η \to (m \in D \land m E n)$
28	27	anim1i	$⊢ (η \land θ) \to ((m \in D \land m E n) \land θ)$
29		bnj170	$⊢ (θ \land m \in D \land m E n) \leftrightarrow ((m \in D \land m E n) \land θ)$
30	28 29	sylibr	$⊢ (η \land θ) \to (θ \land m \in D \land m E n)$
31	30 11	syl	Could not format ( ( et /\ th ) -> ch' ) : No typesetting found for \|- ( ( et /\ th ) -> ch' ) with typecode \|-
32		simpl	$⊢ (η \land θ) \to η$
33	31 32	jca	Could not format ( ( et /\ th ) -> ( ch' /\ et ) ) : No typesetting found for \|- ( ( et /\ th ) -> ( ch' /\ et ) ) with typecode \|-
34	33	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 \|-
35		bnj248	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) ) with typecode \|-
36		pm3.35	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ( ( R _FrSe A /\ x e. A ) /\ ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) with typecode \|-
37	7 36	sylan2b	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 \|-
38		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 \|-
39	37 38	syl	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 \|-
40	39 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 \|-
41	35 40	bnj832	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 \|-
42	12 13 14	3jca	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ( f Fn n /\ ph" /\ ps" ) ) : No typesetting found for \|- ( ( R _FrSe A /\ ta /\ et ) -> ( f Fn n /\ ph" /\ ps" ) ) with typecode \|-
43	42	3com23	Could not format ( ( R _FrSe A /\ et /\ ta ) -> ( f Fn n /\ ph" /\ ps" ) ) : No typesetting found for \|- ( ( R _FrSe A /\ et /\ ta ) -> ( f Fn n /\ ph" /\ ps" ) ) with typecode \|-
44	43	3expia	Could not format ( ( R _FrSe A /\ et ) -> ( ta -> ( f Fn n /\ ph" /\ ps" ) ) ) : No typesetting found for \|- ( ( R _FrSe A /\ et ) -> ( ta -> ( f Fn n /\ ph" /\ ps" ) ) ) with typecode \|-
45	44	eximdv	Could not format ( ( R _FrSe A /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) : No typesetting found for \|- ( ( R _FrSe A /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) with typecode \|-
46	45	ad4ant14	Could not format ( ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) : No typesetting found for \|- ( ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) with typecode \|-
47	35 46	sylbi	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) with typecode \|-
48	41 47	mpd	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 \|-
49		bnj432	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ch' /\ et ) /\ ( R _FrSe A /\ x e. A ) ) ) : No typesetting found for \|- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ch' /\ et ) /\ ( R _FrSe A /\ x e. A ) ) ) with typecode \|-
50		biid	$⊢ f Fn n \leftrightarrow f Fn n$
51		sbcid	$⊢ \underset{˙}{[} f / f \underset{˙}{]} φ \leftrightarrow φ$
52	2 51	bitri	Could not format ( ph" <-> ph ) : No typesetting found for \|- ( ph" <-> ph ) with typecode \|-
53		sbcid	$⊢ \underset{˙}{[} f / f \underset{˙}{]} ψ \leftrightarrow ψ$
54	3 53	bitri	Could not format ( ps" <-> ps ) : No typesetting found for \|- ( ps" <-> ps ) with typecode \|-
55	50 52 54	3anbi123i	Could not format ( ( f Fn n /\ ph" /\ ps" ) <-> ( f Fn n /\ ph /\ ps ) ) : No typesetting found for \|- ( ( f Fn n /\ ph" /\ ps" ) <-> ( f Fn n /\ ph /\ ps ) ) with typecode \|-
56	55	exbii	Could not format ( E. f ( f Fn n /\ ph" /\ ps" ) <-> E. f ( f Fn n /\ ph /\ ps ) ) : No typesetting found for \|- ( E. f ( f Fn n /\ ph" /\ ps" ) <-> E. f ( f Fn n /\ ph /\ ps ) ) with typecode \|-
57	48 49 56	3imtr3i	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 \|-
58	57	ex	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 \|-
59	58	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 \|-
60	23 34 59	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 ψ))$
61	60	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 bnj605

Proof