Metamath Proof Explorer

Theorem bnj125

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) (New usage is discouraged.)

Ref Expression
Hypotheses bnj125.1 ${⊢}{\phi }↔{f}\left(\varnothing \right)=pred\left({x},{A},{R}\right)$
bnj125.2 No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
bnj125.3 No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
bnj125.4 ${⊢}{F}=\left\{⟨\varnothing ,pred\left({x},{A},{R}\right)⟩\right\}$
Assertion bnj125 Could not format assertion : No typesetting found for |- ( ph" <-> ( F  (/) ) = _pred ( x , A , R ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj125.1 ${⊢}{\phi }↔{f}\left(\varnothing \right)=pred\left({x},{A},{R}\right)$
2 bnj125.2 Could not format ( ph' <-> [. 1o / n ]. ph ) : No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
3 bnj125.3 Could not format ( ph" <-> [. F / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
4 bnj125.4 ${⊢}{F}=\left\{⟨\varnothing ,pred\left({x},{A},{R}\right)⟩\right\}$
5 2 sbcbii Could not format ( [. F / f ]. ph' <-> [. F / f ]. [. 1o / n ]. ph ) : No typesetting found for |- ( [. F / f ]. ph' <-> [. F / f ]. [. 1o / n ]. ph ) with typecode |-
6 bnj105 ${⊢}{1}_{𝑜}\in \mathrm{V}$
7 1 6 bnj91
8 7 sbcbii
9 4 bnj95 ${⊢}{F}\in \mathrm{V}$
10 fveq1 ${⊢}{f}={F}\to {f}\left(\varnothing \right)={F}\left(\varnothing \right)$
11 10 eqeq1d ${⊢}{f}={F}\to \left({f}\left(\varnothing \right)=pred\left({x},{A},{R}\right)↔{F}\left(\varnothing \right)=pred\left({x},{A},{R}\right)\right)$
12 9 11 sbcie
13 8 12 bitri
14 5 13 bitri Could not format ( [. F / f ]. ph' <-> ( F  (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( [. F / f ]. ph' <-> ( F  (/) ) = _pred ( x , A , R ) ) with typecode |-
15 3 14 bitri Could not format ( ph" <-> ( F  (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph" <-> ( F ` (/) ) = _pred ( x , A , R ) ) with typecode |-