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

Metamath Proof Explorer

Theorem bnj518

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 bnj518.1 ⊢ φ ↔ f ⁡ ∅ = pred x A R
bnj518.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
bnj518.3 ⊢ τ ↔ φ ∧ ψ ∧ n ∈ ω ∧ p ∈ n
Assertion bnj518 ⊢ R FrSe A ∧ τ → ∀ y ∈ f ⁡ p pred y A R ∈ V

Proof

Step Hyp Ref Expression
1 bnj518.1 ⊢ φ ↔ f ⁡ ∅ = pred x A R
2 bnj518.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj518.3 ⊢ τ ↔ φ ∧ ψ ∧ n ∈ ω ∧ p ∈ n
4 bnj334 ⊢ φ ∧ ψ ∧ n ∈ ω ∧ p ∈ n ↔ n ∈ ω ∧ φ ∧ ψ ∧ p ∈ n
5 3 4 bitri ⊢ τ ↔ n ∈ ω ∧ φ ∧ ψ ∧ p ∈ n
6 df-bnj17 ⊢ n ∈ ω ∧ φ ∧ ψ ∧ p ∈ n ↔ n ∈ ω ∧ φ ∧ ψ ∧ p ∈ n
7 1 2 bnj517 ⊢ n ∈ ω ∧ φ ∧ ψ → ∀ p ∈ n f ⁡ p ⊆ A
8 7 r19.21bi ⊢ n ∈ ω ∧ φ ∧ ψ ∧ p ∈ n → f ⁡ p ⊆ A
9 6 8 sylbi ⊢ n ∈ ω ∧ φ ∧ ψ ∧ p ∈ n → f ⁡ p ⊆ A
10 5 9 sylbi ⊢ τ → f ⁡ p ⊆ A
11 ssel ⊢ f ⁡ p ⊆ A → y ∈ f ⁡ p → y ∈ A
12 bnj93 ⊢ R FrSe A ∧ y ∈ A → pred y A R ∈ V
13 12 ex ⊢ R FrSe A → y ∈ A → pred y A R ∈ V
14 11 13 sylan9r ⊢ R FrSe A ∧ f ⁡ p ⊆ A → y ∈ f ⁡ p → pred y A R ∈ V
15 14 ralrimiv ⊢ R FrSe A ∧ f ⁡ p ⊆ A → ∀ y ∈ f ⁡ p pred y A R ∈ V
16 10 15 sylan2 ⊢ R FrSe A ∧ τ → ∀ y ∈ f ⁡ p pred y A R ∈ V