Metamath Proof Explorer

Theorem bnj544

Description: Technical lemma for bnj852 . 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 bnj544.1 No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
bnj544.2 No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
bnj544.3 ⊢ D = ω ∖ ∅
bnj544.4 ⊢ G = f ∪ m ⋃ y ∈ f ⁡ p pred y A R
bnj544.5 No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
bnj544.6 ⊢ σ ↔ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ m
Assertion bnj544 ⊢ R FrSe A ∧ τ ∧ σ → G Fn n

Proof

Step Hyp Ref Expression
1 bnj544.1 Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
2 bnj544.2 Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
3 bnj544.3 ⊢ D = ω ∖ ∅
4 bnj544.4 ⊢ G = f ∪ m ⋃ y ∈ f ⁡ p pred y A R
5 bnj544.5 Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
6 bnj544.6 ⊢ σ ↔ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ m
7 3 bnj923 ⊢ m ∈ D → m ∈ ω
8 7 3anim1i ⊢ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ m → m ∈ ω ∧ n = suc ⁡ m ∧ p ∈ m
9 6 8 sylbi ⊢ σ → m ∈ ω ∧ n = suc ⁡ m ∧ p ∈ m
10 biid ⊢ m ∈ ω ∧ n = suc ⁡ m ∧ p ∈ m ↔ m ∈ ω ∧ n = suc ⁡ m ∧ p ∈ m
11 1 2 4 5 10 bnj543 ⊢ R FrSe A ∧ τ ∧ m ∈ ω ∧ n = suc ⁡ m ∧ p ∈ m → G Fn n
12 9 11 syl3an3 ⊢ R FrSe A ∧ τ ∧ σ → G Fn n