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

Metamath Proof Explorer

Theorem bnj998

Description: Technical lemma for bnj69 . 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 bnj998.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
bnj998.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
bnj998.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
bnj998.4 ⊢ θ ↔ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R ∧ z ∈ pred y A R
bnj998.5 ⊢ τ ↔ m ∈ ω ∧ n = suc ⁡ m ∧ p = suc ⁡ n
bnj998.7 No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
bnj998.8 No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
bnj998.9 No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
bnj998.10 No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
bnj998.11 No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
bnj998.12 No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
bnj998.13 ⊢ D = ω ∖ ∅
bnj998.14 ⊢ B = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
bnj998.15 ⊢ C = ⋃ y ∈ f ⁡ m pred y A R
bnj998.16 ⊢ G = f ∪ n C
Assertion bnj998 Could not format assertion : No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj998.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj998.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj998.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
4 bnj998.4 ⊢ θ ↔ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R ∧ z ∈ pred y A R
5 bnj998.5 ⊢ τ ↔ m ∈ ω ∧ n = suc ⁡ m ∧ p = suc ⁡ n
6 bnj998.7 Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
7 bnj998.8 Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
8 bnj998.9 Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
9 bnj998.10 Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
10 bnj998.11 Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
11 bnj998.12 Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
12 bnj998.13 ⊢ D = ω ∖ ∅
13 bnj998.14 ⊢ B = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
14 bnj998.15 ⊢ C = ⋃ y ∈ f ⁡ m pred y A R
15 bnj998.16 ⊢ G = f ∪ n C
16 bnj253 ⊢ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R ∧ z ∈ pred y A R ↔ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R ∧ z ∈ pred y A R
17 16 simp1bi ⊢ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R ∧ z ∈ pred y A R → R FrSe A ∧ X ∈ A
18 4 17 sylbi ⊢ θ → R FrSe A ∧ X ∈ A
19 18 bnj705 ⊢ θ ∧ χ ∧ τ ∧ η → R FrSe A ∧ X ∈ A
20 bnj643 ⊢ θ ∧ χ ∧ τ ∧ η → χ
21 3simpc ⊢ m ∈ ω ∧ n = suc ⁡ m ∧ p = suc ⁡ n → n = suc ⁡ m ∧ p = suc ⁡ n
22 5 21 sylbi ⊢ τ → n = suc ⁡ m ∧ p = suc ⁡ n
23 22 bnj707 ⊢ θ ∧ χ ∧ τ ∧ η → n = suc ⁡ m ∧ p = suc ⁡ n
24 bnj255 ⊢ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n ↔ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n
25 19 20 23 24 syl3anbrc ⊢ θ ∧ χ ∧ τ ∧ η → R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n
26 bnj252 ⊢ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n ↔ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n
27 25 26 sylib ⊢ θ ∧ χ ∧ τ ∧ η → R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n
28 biid ⊢ f Fn n ∧ φ ∧ ψ ↔ f Fn n ∧ φ ∧ ψ
29 biid ⊢ n ∈ D ∧ p = suc ⁡ n ∧ m ∈ n ↔ n ∈ D ∧ p = suc ⁡ n ∧ m ∈ n
30 1 2 3 6 7 8 9 10 11 12 13 14 15 28 29 bnj910 Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) with typecode |-
31 27 30 syl Could not format ( ( th /\ ch /\ ta /\ et ) -> ch" ) : No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode |-