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

Metamath Proof Explorer

Theorem bnj151

Description: Technical lemma for bnj153 . 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 bnj151.1 ⊢ φ ↔ f ⁡ ∅ = pred x A R
bnj151.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
bnj151.3 ⊢ D = ω ∖ ∅
bnj151.4 ⊢ θ ↔ R FrSe A ∧ x ∈ A → ∃! f f Fn n ∧ φ ∧ ψ
bnj151.5 ⊢ τ ↔ ∀ m ∈ D m E n → [˙m / n]˙ θ
bnj151.6 ⊢ ζ ↔ R FrSe A ∧ x ∈ A → f Fn n ∧ φ ∧ ψ
bnj151.7 No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
bnj151.8 No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
bnj151.9 No typesetting found for |- ( th' <-> [. 1o / n ]. th ) with typecode |-
bnj151.10 No typesetting found for |- ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
bnj151.11 No typesetting found for |- ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
bnj151.12 No typesetting found for |- ( ze' <-> [. 1o / n ]. ze ) with typecode |-
bnj151.13 ⊢ F = ∅ pred x A R
bnj151.14 No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
bnj151.15 No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
bnj151.16 No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |-
bnj151.17 No typesetting found for |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
bnj151.18 No typesetting found for |- ( ze1 <-> [. g / f ]. ze0 ) with typecode |-
bnj151.19 No typesetting found for |- ( ph1 <-> [. g / f ]. ph' ) with typecode |-
bnj151.20 No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
Assertion bnj151 ⊢ n = 1 𝑜 → n ∈ D ∧ τ → θ

Proof

Step Hyp Ref Expression
1 bnj151.1 ⊢ φ ↔ f ⁡ ∅ = pred x A R
2 bnj151.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj151.3 ⊢ D = ω ∖ ∅
4 bnj151.4 ⊢ θ ↔ R FrSe A ∧ x ∈ A → ∃! f f Fn n ∧ φ ∧ ψ
5 bnj151.5 ⊢ τ ↔ ∀ m ∈ D m E n → [˙m / n]˙ θ
6 bnj151.6 ⊢ ζ ↔ R FrSe A ∧ x ∈ A → f Fn n ∧ φ ∧ ψ
7 bnj151.7 Could not format ( ph' <-> [. 1o / n ]. ph ) : No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
8 bnj151.8 Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
9 bnj151.9 Could not format ( th' <-> [. 1o / n ]. th ) : No typesetting found for |- ( th' <-> [. 1o / n ]. th ) with typecode |-
10 bnj151.10 Could not format ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
11 bnj151.11 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 |-
12 bnj151.12 Could not format ( ze' <-> [. 1o / n ]. ze ) : No typesetting found for |- ( ze' <-> [. 1o / n ]. ze ) with typecode |-
13 bnj151.13 ⊢ F = ∅ pred x A R
14 bnj151.14 Could not format ( ph" <-> [. F / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
15 bnj151.15 Could not format ( ps" <-> [. F / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
16 bnj151.16 Could not format ( ze" <-> [. F / f ]. ze' ) : No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |-
17 bnj151.17 Could not format ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
18 bnj151.18 Could not format ( ze1 <-> [. g / f ]. ze0 ) : No typesetting found for |- ( ze1 <-> [. g / f ]. ze0 ) with typecode |-
19 bnj151.19 Could not format ( ph1 <-> [. g / f ]. ph' ) : No typesetting found for |- ( ph1 <-> [. g / f ]. ph' ) with typecode |-
20 bnj151.20 Could not format ( ps1 <-> [. g / f ]. ps' ) : No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
21 1 2 6 7 8 10 12 13 14 15 16 bnj150 Could not format th0 : No typesetting found for |- th0 with typecode |-
22 21 10 mpbi 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 |-
23 1 7 bnj118 Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
24 11 17 18 19 20 23 bnj149 Could not format th1 : No typesetting found for |- th1 with typecode |-
25 24 11 mpbi 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 |-
26 df-eu Could not format ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> ( E. f ( f Fn 1o /\ ph' /\ ps' ) /\ E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> ( E. f ( f Fn 1o /\ ph' /\ ps' ) /\ E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
27 22 25 26 sylanbrc 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 |-
28 4 7 8 9 bnj130 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 |-
29 27 28 mpbir Could not format th' : No typesetting found for |- th' with typecode |-
30 sbceq1a ⊢ n = 1 𝑜 → θ ↔ [˙ 1 𝑜 / n]˙ θ
31 30 9 bitr4di Could not format ( n = 1o -> ( th <-> th' ) ) : No typesetting found for |- ( n = 1o -> ( th <-> th' ) ) with typecode |-
32 29 31 mpbiri ⊢ n = 1 𝑜 → θ
33 32 a1d ⊢ n = 1 𝑜 → n ∈ D ∧ τ → θ