Theorem bnj1090

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	bnj1090.9	⊢ ( 𝜂 ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
	bnj1090.10	⊢ ( 𝜌 ↔ ∀ 𝑗 ∈ 𝑛 ( 𝑗 E 𝑖 → [ 𝑗 / 𝑖 ] 𝜂 ) )
	bnj1090.17	⊢ ( 𝜂′ ↔ [ 𝑗 / 𝑖 ] 𝜂 )
	bnj1090.18	⊢ ( 𝜎 ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) )
	bnj1090.19	⊢ ( 𝜑0 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) )
	bnj1090.28	⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) → ∀ 𝑖 ∃ 𝑗 ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
Assertion	bnj1090	⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) → ∀ 𝑖 ∈ 𝑛 ( 𝜌 → 𝜂 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1090.9	⊢ ( 𝜂 ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
2		bnj1090.10	⊢ ( 𝜌 ↔ ∀ 𝑗 ∈ 𝑛 ( 𝑗 E 𝑖 → [ 𝑗 / 𝑖 ] 𝜂 ) )
3		bnj1090.17	⊢ ( 𝜂′ ↔ [ 𝑗 / 𝑖 ] 𝜂 )
4		bnj1090.18	⊢ ( 𝜎 ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) )
5		bnj1090.19	⊢ ( 𝜑0 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) )
6		bnj1090.28	⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) → ∀ 𝑖 ∃ 𝑗 ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
7		impexp	⊢ ( ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ) → 𝜂 ) ↔ ( 𝑖 ∈ 𝑛 → ( 𝜎 → 𝜂 ) ) )
8	7	exbii	⊢ ( ∃ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ) → 𝜂 ) ↔ ∃ 𝑗 ( 𝑖 ∈ 𝑛 → ( 𝜎 → 𝜂 ) ) )
9	4	imbi1i	⊢ ( ( 𝜎 → 𝜂 ) ↔ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) → 𝜂 ) )
10	9	exbii	⊢ ( ∃ 𝑗 ( 𝜎 → 𝜂 ) ↔ ∃ 𝑗 ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) → 𝜂 ) )
11	10	imbi2i	⊢ ( ( 𝑖 ∈ 𝑛 → ∃ 𝑗 ( 𝜎 → 𝜂 ) ) ↔ ( 𝑖 ∈ 𝑛 → ∃ 𝑗 ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) → 𝜂 ) ) )
12		19.37v	⊢ ( ∃ 𝑗 ( 𝑖 ∈ 𝑛 → ( 𝜎 → 𝜂 ) ) ↔ ( 𝑖 ∈ 𝑛 → ∃ 𝑗 ( 𝜎 → 𝜂 ) ) )
13	2	bnj115	⊢ ( 𝜌 ↔ ∀ 𝑗 ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → [ 𝑗 / 𝑖 ] 𝜂 ) )
14	3	imbi2i	⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → [ 𝑗 / 𝑖 ] 𝜂 ) )
15	14	albii	⊢ ( ∀ 𝑗 ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) ↔ ∀ 𝑗 ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → [ 𝑗 / 𝑖 ] 𝜂 ) )
16	13 15	bitr4i	⊢ ( 𝜌 ↔ ∀ 𝑗 ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) )
17	16	imbi1i	⊢ ( ( 𝜌 → 𝜂 ) ↔ ( ∀ 𝑗 ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) → 𝜂 ) )
18		19.36v	⊢ ( ∃ 𝑗 ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) → 𝜂 ) ↔ ( ∀ 𝑗 ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) → 𝜂 ) )
19	17 18	bitr4i	⊢ ( ( 𝜌 → 𝜂 ) ↔ ∃ 𝑗 ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) → 𝜂 ) )
20	19	imbi2i	⊢ ( ( 𝑖 ∈ 𝑛 → ( 𝜌 → 𝜂 ) ) ↔ ( 𝑖 ∈ 𝑛 → ∃ 𝑗 ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) → 𝜂 ) ) )
21	11 12 20	3bitr4i	⊢ ( ∃ 𝑗 ( 𝑖 ∈ 𝑛 → ( 𝜎 → 𝜂 ) ) ↔ ( 𝑖 ∈ 𝑛 → ( 𝜌 → 𝜂 ) ) )
22	8 21	bitr2i	⊢ ( ( 𝑖 ∈ 𝑛 → ( 𝜌 → 𝜂 ) ) ↔ ∃ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ) → 𝜂 ) )
23		impexp	⊢ ( ( ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ) ∧ ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ) → ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ) )
24		bnj256	⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) ↔ ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ) ∧ ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) ) )
25	24	imbi1i	⊢ ( ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ( ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ) ∧ ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
26	1	imbi2i	⊢ ( ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ) → 𝜂 ) ↔ ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ) → ( ( 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ) )
27	23 25 26	3bitr4i	⊢ ( ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ) → 𝜂 ) )
28	22 27	bnj133	⊢ ( ( 𝑖 ∈ 𝑛 → ( 𝜌 → 𝜂 ) ) ↔ ∃ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
29	28	albii	⊢ ( ∀ 𝑖 ( 𝑖 ∈ 𝑛 → ( 𝜌 → 𝜂 ) ) ↔ ∀ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
30		df-ral	⊢ ( ∀ 𝑖 ∈ 𝑛 ( 𝜌 → 𝜂 ) ↔ ∀ 𝑖 ( 𝑖 ∈ 𝑛 → ( 𝜌 → 𝜂 ) ) )
31	5	imbi1i	⊢ ( ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
32	31	exbii	⊢ ( ∃ 𝑗 ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ∃ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
33	32	albii	⊢ ( ∀ 𝑖 ∃ 𝑗 ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) ↔ ∀ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
34	29 30 33	3bitr4i	⊢ ( ∀ 𝑖 ∈ 𝑛 ( 𝜌 → 𝜂 ) ↔ ∀ 𝑖 ∃ 𝑗 ( 𝜑0 → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ) )
35	6 34	sylibr	⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) → ∀ 𝑖 ∈ 𝑛 ( 𝜌 → 𝜂 ) )