This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑜 = ∅
9 8 fneq2i ⊢ f Fn 1 𝑜 ↔ f Fn ∅
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 ⁡ ∅ ∈ V
14 13 elsn ⊢ f ⁡ ∅ ∈ pred x A R ↔ f ⁡ ∅ = pred x A R
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 ⊢ ∅ ∈ V
17 fveq2 ⊢ g = ∅ → f ⁡ g = f ⁡ ∅
18 17 eleq1d ⊢ g = ∅ → f ⁡ g ∈ pred x A R ↔ f ⁡ ∅ ∈ pred x A R
19 16 18 ralsn ⊢ ∀ g ∈ ∅ f ⁡ g ∈ pred x A R ↔ f ⁡ ∅ ∈ pred x A R
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 : ∅ ⟶ pred x A R ↔ f Fn ∅ ∧ ∀ g ∈ ∅ f ⁡ g ∈ pred x A R
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 ⊢ R FrSe A ∧ x ∈ A → pred x A R ∈ 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 ⊢ ∅ ∈ V ∧ pred x A R ∈ V → f : ∅ ⟶ pred x A R ↔ f = ∅ pred x A R
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 |-