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

Metamath Proof Explorer

Theorem bnj1020

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

Proof

Step Hyp Ref Expression
1 bnj1020.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj1020.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj1020.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
4 bnj1020.4 ⊢ θ ↔ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R ∧ z ∈ pred y A R
5 bnj1020.5 ⊢ τ ↔ m ∈ ω ∧ n = suc ⁡ m ∧ p = suc ⁡ n
6 bnj1020.6 ⊢ η ↔ i ∈ n ∧ y ∈ f ⁡ i
7 bnj1020.7 Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
8 bnj1020.8 Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
9 bnj1020.9 Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
10 bnj1020.10 Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
11 bnj1020.11 Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
12 bnj1020.12 Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
13 bnj1020.13 ⊢ D = ω ∖ ∅
14 bnj1020.14 ⊢ B = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
15 bnj1020.15 ⊢ C = ⋃ y ∈ f ⁡ m pred y A R
16 bnj1020.16 ⊢ G = f ∪ n C
17 bnj1020.26 Could not format ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for |- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode |-
18 bnj1019 ⊢ ∃ p θ ∧ χ ∧ τ ∧ η ↔ θ ∧ χ ∧ η ∧ ∃ p τ
19 1 2 3 4 5 7 8 9 10 11 12 13 14 15 16 bnj998 Could not format ( ( th /\ ch /\ ta /\ et ) -> ch" ) : No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode |-
20 3 5 6 13 19 bnj1001 Could not format ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) : No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode |-
21 1 2 3 4 5 6 7 8 9 10 11 12 13 15 16 20 bnj1006 ⊢ θ ∧ χ ∧ τ ∧ η → pred y A R ⊆ G ⁡ suc ⁡ i
22 21 exlimiv ⊢ ∃ p θ ∧ χ ∧ τ ∧ η → pred y A R ⊆ G ⁡ suc ⁡ i
23 18 22 sylbir ⊢ θ ∧ χ ∧ η ∧ ∃ p τ → pred y A R ⊆ G ⁡ suc ⁡ i
24 1 2 3 4 5 7 8 9 10 11 12 13 14 15 16 17 19 20 bnj1018 ⊢ θ ∧ χ ∧ η ∧ ∃ p τ → G ⁡ suc ⁡ i ⊆ trCl X A R
25 23 24 sstrd ⊢ θ ∧ χ ∧ η ∧ ∃ p τ → pred y A R ⊆ trCl X A R