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

Metamath Proof Explorer

Theorem bnj1053

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

Proof

Step Hyp Ref Expression
1 bnj1053.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj1053.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj1053.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
4 bnj1053.4 ⊢ θ ↔ R FrSe A ∧ X ∈ A
5 bnj1053.5 ⊢ τ ↔ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B
6 bnj1053.6 ⊢ ζ ↔ i ∈ n ∧ z ∈ f ⁡ i
7 bnj1053.7 ⊢ D = ω ∖ ∅
8 bnj1053.8 ⊢ K = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
9 bnj1053.9 ⊢ η ↔ θ ∧ τ ∧ χ ∧ ζ → z ∈ B
10 bnj1053.10 ⊢ ρ ↔ ∀ j ∈ n j E i → [˙j / i]˙ η
11 bnj1053.37 ⊢ θ ∧ τ ∧ χ ∧ ζ → ∀ i ∈ n ρ → η
12 7 bnj923 ⊢ n ∈ D → n ∈ ω
13 nnord ⊢ n ∈ ω → Ord ⁡ n
14 ordfr ⊢ Ord ⁡ n → E Fr n
15 12 13 14 3syl ⊢ n ∈ D → E Fr n
16 3 15 bnj769 ⊢ χ → E Fr n
17 16 bnj707 ⊢ θ ∧ τ ∧ χ ∧ ζ → E Fr n
18 17 11 jca ⊢ θ ∧ τ ∧ χ ∧ ζ → E Fr n ∧ ∀ i ∈ n ρ → η
19 1 2 3 4 5 6 7 8 9 10 18 bnj1052 ⊢ θ ∧ τ → trCl X A R ⊆ B