Metamath Proof Explorer

Theorem bnj1034

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 bnj1034.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
bnj1034.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
bnj1034.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
bnj1034.4 ⊢ θ ↔ R FrSe A ∧ X ∈ A
bnj1034.5 ⊢ τ ↔ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B
bnj1034.7 ⊢ ζ ↔ i ∈ n ∧ z ∈ f ⁡ i
bnj1034.8 ⊢ D = ω ∖ ∅
bnj1034.9 ⊢ K = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
bnj1034.10 ⊢ ∃ f ∃ n ∃ i θ ∧ τ ∧ χ ∧ ζ → z ∈ B
Assertion bnj1034 ⊢ θ ∧ τ → trCl X A R ⊆ B

Proof

Step Hyp Ref Expression
1 bnj1034.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj1034.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj1034.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
4 bnj1034.4 ⊢ θ ↔ R FrSe A ∧ X ∈ A
5 bnj1034.5 ⊢ τ ↔ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B
6 bnj1034.7 ⊢ ζ ↔ i ∈ n ∧ z ∈ f ⁡ i
7 bnj1034.8 ⊢ D = ω ∖ ∅
8 bnj1034.9 ⊢ K = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
9 bnj1034.10 ⊢ ∃ f ∃ n ∃ i θ ∧ τ ∧ χ ∧ ζ → z ∈ B
10 biid ⊢ z ∈ trCl X A R ↔ z ∈ trCl X A R
11 1 2 3 4 5 10 6 7 8 9 bnj1033 ⊢ θ ∧ τ → trCl X A R ⊆ B