Metamath Proof Explorer

Theorem bnj546

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 bnj546.1 ⊢ D = ω ∖ ∅
bnj546.2 No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
bnj546.3 ⊢ σ ↔ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ m
bnj546.4 No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
bnj546.5 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 |-
Assertion bnj546 ⊢ R FrSe A ∧ τ ∧ σ → ⋃ y ∈ f ⁡ p pred y A R ∈ V

Proof

Step Hyp Ref Expression
1 bnj546.1 ⊢ D = ω ∖ ∅
2 bnj546.2 Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
3 bnj546.3 ⊢ σ ↔ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ m
4 bnj546.4 Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
5 bnj546.5 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 |-
6 3simpc Could not format ( ( f Fn m /\ ph' /\ ps' ) -> ( ph' /\ ps' ) ) : No typesetting found for |- ( ( f Fn m /\ ph' /\ ps' ) -> ( ph' /\ ps' ) ) with typecode |-
7 2 6 sylbi Could not format ( ta -> ( ph' /\ ps' ) ) : No typesetting found for |- ( ta -> ( ph' /\ ps' ) ) with typecode |-
8 1 bnj923 ⊢ m ∈ D → m ∈ ω
9 8 3ad2ant1 ⊢ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ m → m ∈ ω
10 simp3 ⊢ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ m → p ∈ m
11 9 10 jca ⊢ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ m → m ∈ ω ∧ p ∈ m
12 3 11 sylbi ⊢ σ → m ∈ ω ∧ p ∈ m
13 7 12 anim12i Could not format ( ( ta /\ si ) -> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) ) : No typesetting found for |- ( ( ta /\ si ) -> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) ) with typecode |-
14 bnj256 Could not format ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) ) : No typesetting found for |- ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) ) with typecode |-
15 13 14 sylibr Could not format ( ( ta /\ si ) -> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) : No typesetting found for |- ( ( ta /\ si ) -> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) with typecode |-
16 15 anim2i Could not format ( ( R _FrSe A /\ ( ta /\ si ) ) -> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ ( ta /\ si ) ) -> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) ) with typecode |-
17 16 3impb Could not format ( ( R _FrSe A /\ ta /\ si ) -> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ si ) -> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) ) with typecode |-
18 biid Could not format ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) : No typesetting found for |- ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) with typecode |-
19 4 5 18 bnj518 Could not format ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) -> A. y e. ( f ` p ) _pred ( y , A , R ) e. _V ) : No typesetting found for |- ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) -> A. y e. ( f ` p ) _pred ( y , A , R ) e. _V ) with typecode |-
20 fvex ⊢ f ⁡ p ∈ V
21 iunexg ⊢ f ⁡ p ∈ V ∧ ∀ y ∈ f ⁡ p pred y A R ∈ V → ⋃ y ∈ f ⁡ p pred y A R ∈ V
22 20 21 mpan ⊢ ∀ y ∈ f ⁡ p pred y A R ∈ V → ⋃ y ∈ f ⁡ p pred y A R ∈ V
23 17 19 22 3syl ⊢ R FrSe A ∧ τ ∧ σ → ⋃ y ∈ f ⁡ p pred y A R ∈ V