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 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )