Metamath Proof Explorer


Theorem bnj130

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

Ref Expression
Hypotheses bnj130.1 θ R FrSe A x A ∃! f f Fn n φ ψ
bnj130.2 No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
bnj130.3 No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
bnj130.4 No typesetting found for |- ( th' <-> [. 1o / n ]. th ) with typecode |-
Assertion bnj130 Could not format assertion : No typesetting found for |- ( th' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj130.1 θ R FrSe A x A ∃! f f Fn n φ ψ
2 bnj130.2 Could not format ( ph' <-> [. 1o / n ]. ph ) : No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
3 bnj130.3 Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
4 bnj130.4 Could not format ( th' <-> [. 1o / n ]. th ) : No typesetting found for |- ( th' <-> [. 1o / n ]. th ) with typecode |-
5 1 sbcbii [˙ 1 𝑜 / n]˙ θ [˙ 1 𝑜 / n]˙ R FrSe A x A ∃! f f Fn n φ ψ
6 bnj105 1 𝑜 V
7 6 bnj90 [˙ 1 𝑜 / n]˙ f Fn n f Fn 1 𝑜
8 7 bicomi f Fn 1 𝑜 [˙ 1 𝑜 / n]˙ f Fn n
9 8 2 3 3anbi123i Could not format ( ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. 1o / n ]. f Fn n /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) ) : No typesetting found for |- ( ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. 1o / n ]. f Fn n /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) ) with typecode |-
10 sbc3an [˙ 1 𝑜 / n]˙ f Fn n φ ψ [˙ 1 𝑜 / n]˙ f Fn n [˙ 1 𝑜 / n]˙ φ [˙ 1 𝑜 / n]˙ ψ
11 9 10 bitr4i Could not format ( ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) with typecode |-
12 11 eubii Could not format ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> E! f [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> E! f [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) with typecode |-
13 6 bnj89 [˙ 1 𝑜 / n]˙ ∃! f f Fn n φ ψ ∃! f [˙ 1 𝑜 / n]˙ f Fn n φ ψ
14 12 13 bitr4i Could not format ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. E! f ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. E! f ( f Fn n /\ ph /\ ps ) ) with typecode |-
15 14 imbi2i Could not format ( ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. E! f ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. E! f ( f Fn n /\ ph /\ ps ) ) ) with typecode |-
16 nfv n R FrSe A x A
17 16 sbc19.21g 1 𝑜 V [˙ 1 𝑜 / n]˙ R FrSe A x A ∃! f f Fn n φ ψ R FrSe A x A [˙ 1 𝑜 / n]˙ ∃! f f Fn n φ ψ
18 6 17 ax-mp [˙ 1 𝑜 / n]˙ R FrSe A x A ∃! f f Fn n φ ψ R FrSe A x A [˙ 1 𝑜 / n]˙ ∃! f f Fn n φ ψ
19 15 18 bitr4i Could not format ( ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) ) with typecode |-
20 5 4 19 3bitr4i Could not format ( th' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( th' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-