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

Metamath Proof Explorer

Theorem bnj1093

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 bnj1093.1 ⊢ ∃ 𝑗 ( ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )
bnj1093.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj1093.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
Assertion bnj1093 ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) → ∀ 𝑖 ∃ 𝑗 ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 bnj1093.1 ⊢ ∃ 𝑗 ( ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )
2 bnj1093.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj1093.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4 2 bnj1095 ⊢ ( 𝜓 → ∀ 𝑖 𝜓 )
5 4 3 bnj1096 ⊢ ( 𝜒 → ∀ 𝑖 𝜒 )
6 5 bnj1350 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → ∀ 𝑖 ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) )
7 impexp ⊢ ( ( ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ) )
8 7 exbii ⊢ ( ∃ 𝑗 ( ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ∃ 𝑗 ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ) )
9 1 8 mpbi ⊢ ∃ 𝑗 ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
10 9 19.37iv ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → ∃ 𝑗 ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
11 6 10 alrimih ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → ∀ 𝑖 ∃ 𝑗 ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
12 11 bnj721 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) → ∀ 𝑖 ∃ 𝑗 ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )