Theorem bnj124

Description: Technical lemma for bnj150 . 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	bnj124.1	$$⊢F=\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
	bnj124.2	No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
	bnj124.3	No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
	bnj124.4	No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |-
	bnj124.5	No typesetting found for |- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
Assertion	bnj124	Could not format assertion : No typesetting found for |- ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj124.1	$$⊢F=\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
2		bnj124.2	Could not format ( ph" <-> [. F / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
3		bnj124.3	Could not format ( ps" <-> [. F / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
4		bnj124.4	Could not format ( ze" <-> [. F / f ]. ze' ) : No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |-
5		bnj124.5	Could not format ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
6	5	sbcbii	Could not format ( [. F / f ]. ze' <-> [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( [. F / f ]. ze' <-> [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
7	1	bnj95	$$⊢F\in \mathrm{V}$$
8		nfv	$$⊢Ⅎf\left(RFrSeA\wedge x\in A\right)$$
9	8	sbc19.21g	Could not format ( F e. _V -> ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) ) : No typesetting found for |- ( F e. _V -> ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) ) with typecode |-
10	7 9	ax-mp	Could not format ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
11		fneq1	$$⊢f=z\to \left(fFn{1}_{𝑜}\leftrightarrow zFn{1}_{𝑜}\right)$$
12		fneq1	$$⊢z=F\to \left(zFn{1}_{𝑜}\leftrightarrow FFn{1}_{𝑜}\right)$$
13	11 12	sbcie2g	$$⊢F\in \mathrm{V}\to \left(\underset{\dot{}}{[}F/f\underset{\dot{}}{]}fFn{1}_{𝑜}\leftrightarrow FFn{1}_{𝑜}\right)$$
14	7 13	ax-mp	$$⊢\underset{\dot{}}{[}F/f\underset{\dot{}}{]}fFn{1}_{𝑜}\leftrightarrow FFn{1}_{𝑜}$$
15	14	bicomi	$$⊢FFn{1}_{𝑜}\leftrightarrow \underset{\dot{}}{[}F/f\underset{\dot{}}{]}fFn{1}_{𝑜}$$
16	15 2 3 7	bnj206	Could not format ( [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( F Fn 1o /\ ph" /\ ps" ) ) : No typesetting found for |- ( [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( F Fn 1o /\ ph" /\ ps" ) ) with typecode |-
17	16	imbi2i	Could not format ( ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |-
18	6 10 17	3bitri	Could not format ( [. F / f ]. ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( [. F / f ]. ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |-
19	4 18	bitri	Could not format ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |-