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

Metamath Proof Explorer

Theorem bnj1006

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

Proof

Step Hyp Ref Expression
1 bnj1006.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj1006.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj1006.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
4 bnj1006.4 ⊢ θ ↔ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R ∧ z ∈ pred y A R
5 bnj1006.5 ⊢ τ ↔ m ∈ ω ∧ n = suc ⁡ m ∧ p = suc ⁡ n
6 bnj1006.6 ⊢ η ↔ i ∈ n ∧ y ∈ f ⁡ i
7 bnj1006.7 Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
8 bnj1006.8 Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
9 bnj1006.9 Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
10 bnj1006.10 Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
11 bnj1006.11 Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
12 bnj1006.12 Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
13 bnj1006.13 ⊢ D = ω ∖ ∅
14 bnj1006.15 ⊢ C = ⋃ y ∈ f ⁡ m pred y A R
15 bnj1006.16 ⊢ G = f ∪ n C
16 bnj1006.28 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 |-
17 6 simprbi ⊢ η → y ∈ f ⁡ i
18 17 bnj708 ⊢ θ ∧ χ ∧ τ ∧ η → y ∈ f ⁡ i
19 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
20 19 simp1bi ⊢ R FrSe A ∧ X ∈ A ∧ y ∈ trCl X A R ∧ z ∈ pred y A R → R FrSe A ∧ X ∈ A
21 4 20 sylbi ⊢ θ → R FrSe A ∧ X ∈ A
22 21 bnj705 ⊢ θ ∧ χ ∧ τ ∧ η → R FrSe A ∧ X ∈ A
23 bnj643 ⊢ θ ∧ χ ∧ τ ∧ η → χ
24 3simpc ⊢ m ∈ ω ∧ n = suc ⁡ m ∧ p = suc ⁡ n → n = suc ⁡ m ∧ p = suc ⁡ n
25 5 24 sylbi ⊢ τ → n = suc ⁡ m ∧ p = suc ⁡ n
26 25 bnj707 ⊢ θ ∧ χ ∧ τ ∧ η → n = suc ⁡ m ∧ p = suc ⁡ n
27 3anass ⊢ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n ↔ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n
28 23 26 27 sylanbrc ⊢ θ ∧ χ ∧ τ ∧ η → χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n
29 biid ⊢ f Fn n ∧ φ ∧ ψ ↔ f Fn n ∧ φ ∧ ψ
30 biid ⊢ n ∈ D ∧ p = suc ⁡ n ∧ m ∈ n ↔ n ∈ D ∧ p = suc ⁡ n ∧ m ∈ n
31 1 2 3 13 14 29 30 bnj969 ⊢ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → C ∈ V
32 22 28 31 syl2anc ⊢ θ ∧ χ ∧ τ ∧ η → C ∈ V
33 3 bnj1235 ⊢ χ → f Fn n
34 33 bnj706 ⊢ θ ∧ χ ∧ τ ∧ η → f Fn n
35 5 simp3bi ⊢ τ → p = suc ⁡ n
36 35 bnj707 ⊢ θ ∧ χ ∧ τ ∧ η → p = suc ⁡ n
37 6 simplbi ⊢ η → i ∈ n
38 37 bnj708 ⊢ θ ∧ χ ∧ τ ∧ η → i ∈ n
39 32 34 36 38 bnj951 ⊢ θ ∧ χ ∧ τ ∧ η → C ∈ V ∧ f Fn n ∧ p = suc ⁡ n ∧ i ∈ n
40 15 bnj945 ⊢ C ∈ V ∧ f Fn n ∧ p = suc ⁡ n ∧ i ∈ n → G ⁡ i = f ⁡ i
41 39 40 syl ⊢ θ ∧ χ ∧ τ ∧ η → G ⁡ i = f ⁡ i
42 18 41 eleqtrrd ⊢ θ ∧ χ ∧ τ ∧ η → y ∈ G ⁡ i
43 16 anim1i Could not format ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ( ch" /\ i e. _om /\ suc i e. p ) /\ y e. ( G ` i ) ) ) : No typesetting found for |- ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ( ch" /\ i e. _om /\ suc i e. p ) /\ y e. ( G ` i ) ) ) with typecode |-
44 df-bnj17 Could not format ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ( ch" /\ i e. _om /\ suc i e. p ) /\ y e. ( G ` i ) ) ) : No typesetting found for |- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ( ch" /\ i e. _om /\ suc i e. p ) /\ y e. ( G ` i ) ) ) with typecode |-
45 43 44 sylibr Could not format ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) : No typesetting found for |- ( ( ( th /\ ch /\ ta /\ et ) /\ y e. ( G ` i ) ) -> ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) with typecode |-
46 1 2 3 7 8 9 10 11 12 14 15 bnj999 Could not format ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) : No typesetting found for |- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) with typecode |-
47 45 46 syl ⊢ θ ∧ χ ∧ τ ∧ η ∧ y ∈ G ⁡ i → pred y A R ⊆ G ⁡ suc ⁡ i
48 42 47 mpdan ⊢ θ ∧ χ ∧ τ ∧ η → pred y A R ⊆ G ⁡ suc ⁡ i