Theorem bnj1090 30301

Description: Technical lemma for bnj69 30332. 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.)

Hypotheses

Ref	Expression
bnj1090.9	⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
bnj1090.10	⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂))
bnj1090.17	⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂)
bnj1090.18	⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))
bnj1090.19	⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓))
bnj1090.28	⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵))

Assertion

Ref	Expression
bnj1090	⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂))

Distinct variable groups:   𝜂,𝑗   𝑖,𝑗   𝑗,𝑛

Allowed substitution hints:   𝜒(𝑓,𝑖,𝑗,𝑛)   𝜃(𝑓,𝑖,𝑗,𝑛)   𝜏(𝑓,𝑖,𝑗,𝑛)   𝜂(𝑓,𝑖,𝑛)   𝜁(𝑓,𝑖,𝑗,𝑛)   𝜎(𝑓,𝑖,𝑗,𝑛)   𝜌(𝑓,𝑖,𝑗,𝑛)   𝐵(𝑓,𝑖,𝑗,𝑛)   𝐾(𝑓,𝑖,𝑗,𝑛)   𝜂′(𝑓,𝑖,𝑗,𝑛)   𝜑₀(𝑓,𝑖,𝑗,𝑛)

Proof of Theorem bnj1090

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695   ∈ wcel 1977  ∀wral 2896  [wsbc 3402   ⊆ wss 3540   class class class wbr 4583   E cep 4947  dom cdm 5038  ‘cfv 5804   ∧ w-bnj17 30005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033  df-ex 1696  df-ral 2901  df-bnj17 30006

This theorem is referenced by:  bnj1030  30309