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

Metamath Proof Explorer

Theorem bnj1121

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 bnj1121.1 ⊢ θ ↔ R FrSe A ∧ X ∈ A
bnj1121.2 ⊢ τ ↔ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B
bnj1121.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
bnj1121.4 ⊢ ζ ↔ i ∈ n ∧ z ∈ f ⁡ i
bnj1121.5 ⊢ η ↔ f ∈ K ∧ i ∈ dom ⁡ f → f ⁡ i ⊆ B
bnj1121.6 ⊢ θ ∧ τ ∧ χ ∧ ζ → ∀ i ∈ n η
bnj1121.7 ⊢ K = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
Assertion bnj1121 ⊢ θ ∧ τ ∧ χ ∧ ζ → z ∈ B

Proof

Step Hyp Ref Expression
1 bnj1121.1 ⊢ θ ↔ R FrSe A ∧ X ∈ A
2 bnj1121.2 ⊢ τ ↔ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B
3 bnj1121.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
4 bnj1121.4 ⊢ ζ ↔ i ∈ n ∧ z ∈ f ⁡ i
5 bnj1121.5 ⊢ η ↔ f ∈ K ∧ i ∈ dom ⁡ f → f ⁡ i ⊆ B
6 bnj1121.6 ⊢ θ ∧ τ ∧ χ ∧ ζ → ∀ i ∈ n η
7 bnj1121.7 ⊢ K = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
8 19.8a ⊢ χ → ∃ n χ
9 8 bnj707 ⊢ θ ∧ τ ∧ χ ∧ ζ → ∃ n χ
10 3 7 bnj1083 ⊢ f ∈ K ↔ ∃ n χ
11 9 10 sylibr ⊢ θ ∧ τ ∧ χ ∧ ζ → f ∈ K
12 4 simplbi ⊢ ζ → i ∈ n
13 12 bnj708 ⊢ θ ∧ τ ∧ χ ∧ ζ → i ∈ n
14 3 bnj1235 ⊢ χ → f Fn n
15 14 bnj707 ⊢ θ ∧ τ ∧ χ ∧ ζ → f Fn n
16 15 fndmd ⊢ θ ∧ τ ∧ χ ∧ ζ → dom ⁡ f = n
17 13 16 eleqtrrd ⊢ θ ∧ τ ∧ χ ∧ ζ → i ∈ dom ⁡ f
18 6 13 bnj1294 ⊢ θ ∧ τ ∧ χ ∧ ζ → η
19 18 5 sylib ⊢ θ ∧ τ ∧ χ ∧ ζ → f ∈ K ∧ i ∈ dom ⁡ f → f ⁡ i ⊆ B
20 11 17 19 mp2and ⊢ θ ∧ τ ∧ χ ∧ ζ → f ⁡ i ⊆ B
21 4 simprbi ⊢ ζ → z ∈ f ⁡ i
22 21 bnj708 ⊢ θ ∧ τ ∧ χ ∧ ζ → z ∈ f ⁡ i
23 20 22 sseldd ⊢ θ ∧ τ ∧ χ ∧ ζ → z ∈ B