Theorem bnj149

Description: Technical lemma for bnj151 . 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) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj149.1	No typesetting found for |- ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
	bnj149.2	No typesetting found for |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
	bnj149.3	No typesetting found for |- ( ze1 <-> [. g / f ]. ze0 ) with typecode |-
	bnj149.4	No typesetting found for |- ( ph1 <-> [. g / f ]. ph' ) with typecode |-
	bnj149.5	No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
	bnj149.6	No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
Assertion	bnj149	Could not format assertion : No typesetting found for |- th1 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj149.1	Could not format ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
2		bnj149.2	Could not format ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
3		bnj149.3	Could not format ( ze1 <-> [. g / f ]. ze0 ) : No typesetting found for |- ( ze1 <-> [. g / f ]. ze0 ) with typecode |-
4		bnj149.4	Could not format ( ph1 <-> [. g / f ]. ph' ) : No typesetting found for |- ( ph1 <-> [. g / f ]. ph' ) with typecode |-
5		bnj149.5	Could not format ( ps1 <-> [. g / f ]. ps' ) : No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
6		bnj149.6	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
7		simpr1	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f Fn 1o ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f Fn 1o ) with typecode |-
8		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
9	8	fneq2i	$$⊢fFn{1}_{𝑜}\leftrightarrow fFn\left\{\varnothing \right\}$$
10	7 9	sylib	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f Fn { (/) } ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f Fn { (/) } ) with typecode |-
11		simpr2	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ph' ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ph' ) with typecode |-
12	11 6	sylib	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
13		fvex	$$⊢f\left(\varnothing \right)\in \mathrm{V}$$
14	13	elsn	$$⊢f\left(\varnothing \right)\in \left\{pred\left(x,A,R\right)\right\}\leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
15	12 14	sylibr	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f ` (/) ) e. { _pred ( x , A , R ) } ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f ` (/) ) e. { _pred ( x , A , R ) } ) with typecode |-
16		0ex	$$⊢\varnothing \in \mathrm{V}$$
17		fveq2	$$⊢g=\varnothing \to f\left(g\right)=f\left(\varnothing \right)$$
18	17	eleq1d	$$⊢g=\varnothing \to \left(f\left(g\right)\in \left\{pred\left(x,A,R\right)\right\}\leftrightarrow f\left(\varnothing \right)\in \left\{pred\left(x,A,R\right)\right\}\right)$$
19	16 18	ralsn	$$⊢\forall g\in \left\{\varnothing \right\}f\left(g\right)\in \left\{pred\left(x,A,R\right)\right\}\leftrightarrow f\left(\varnothing \right)\in \left\{pred\left(x,A,R\right)\right\}$$
20	15 19	sylibr	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> A. g e. { (/) } ( f ` g ) e. { _pred ( x , A , R ) } ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> A. g e. { (/) } ( f ` g ) e. { _pred ( x , A , R ) } ) with typecode |-
21		ffnfv	$$⊢f:\left\{\varnothing \right\}⟶\left\{pred\left(x,A,R\right)\right\}\leftrightarrow \left(fFn\left\{\varnothing \right\}\wedge \forall g\in \left\{\varnothing \right\}f\left(g\right)\in \left\{pred\left(x,A,R\right)\right\}\right)$$
22	10 20 21	sylanbrc	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f : { (/) } --> { _pred ( x , A , R ) } ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f : { (/) } --> { _pred ( x , A , R ) } ) with typecode |-
23		bnj93	$$⊢\left(RFrSeA\wedge x\in A\right)\to pred\left(x,A,R\right)\in \mathrm{V}$$
24	23	adantr	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> _pred ( x , A , R ) e. _V ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> _pred ( x , A , R ) e. _V ) with typecode |-
25		fsng	$$⊢\left(\varnothing \in \mathrm{V}\wedge pred\left(x,A,R\right)\in \mathrm{V}\right)\to \left(f:\left\{\varnothing \right\}⟶\left\{pred\left(x,A,R\right)\right\}\leftrightarrow f=\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}\right)$$
26	16 24 25	sylancr	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f : { (/) } --> { _pred ( x , A , R ) } <-> f = { <. (/) , _pred ( x , A , R ) >. } ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> ( f : { (/) } --> { _pred ( x , A , R ) } <-> f = { <. (/) , _pred ( x , A , R ) >. } ) ) with typecode |-
27	22 26	mpbid	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( f Fn 1o /\ ph' /\ ps' ) ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) with typecode |-
28	27	ex	Could not format ( ( R _FrSe A /\ x e. A ) -> ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) ) with typecode |-
29	28	alrimiv	Could not format ( ( R _FrSe A /\ x e. A ) -> A. f ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> A. f ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) ) with typecode |-
30		mo2icl	Could not format ( A. f ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( A. f ( ( f Fn 1o /\ ph' /\ ps' ) -> f = { <. (/) , _pred ( x , A , R ) >. } ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
31	29 30	syl	Could not format ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
32	31 1	mpbir	Could not format th1 : No typesetting found for |- th1 with typecode |-