Theorem bnj1090 32672

Description: Technical lemma for bnj69 32703. 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 454	. . . . . . 7 ⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ (𝑖 ∈ 𝑛 → (𝜎 → 𝜂)))
3	2	exbii 1855	. . . . . 6 ⊢ (∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ ∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂)))
4		bnj1090.18	. . . . . . . . . 10 ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))
5	4	imbi1i 353	. . . . . . . . 9 ⊢ ((𝜎 → 𝜂) ↔ (((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
6	5	exbii 1855	. . . . . . . 8 ⊢ (∃𝑗(𝜎 → 𝜂) ↔ ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
7	6	imbi2i 339	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑛 → ∃𝑗(𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂)))
8		19.37v 2000	. . . . . . 7 ⊢ (∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(𝜎 → 𝜂)))
9		bnj1090.10	. . . . . . . . . . . 12 ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂))
10	9	bnj115 32416	. . . . . . . . . . 11 ⊢ (𝜌 ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
11		bnj1090.17	. . . . . . . . . . . . 13 ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂)
12	11	imbi2i 339	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
13	12	albii 1827	. . . . . . . . . . 11 ⊢ (∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
14	10, 13	bitr4i 281	. . . . . . . . . 10 ⊢ (𝜌 ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))
15	14	imbi1i 353	. . . . . . . . 9 ⊢ ((𝜌 → 𝜂) ↔ (∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
16		19.36v 1996	. . . . . . . . 9 ⊢ (∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂) ↔ (∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
17	15, 16	bitr4i 281	. . . . . . . 8 ⊢ ((𝜌 → 𝜂) ↔ ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
18	17	imbi2i 339	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂)))
19	7, 8, 18	3bitr4i 306	. . . . . 6 ⊢ (∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → (𝜌 → 𝜂)))
20	3, 19	bitr2i 279	. . . . 5 ⊢ ((𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂))
21		impexp 454	. . . . . 6 ⊢ ((((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) → ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)))
22		bnj256 32397	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)))
23	22	imbi1i 353	. . . . . 6 ⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ (((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) → (𝑓‘𝑖) ⊆ 𝐵))
24		bnj1090.9	. . . . . . 7 ⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
25	24	imbi2i 339	. . . . . 6 ⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) → ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)))
26	21, 23, 25	3bitr4i 306	. . . . 5 ⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂))
27	20, 26	bnj133 32418	. . . 4 ⊢ ((𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
28	27	albii 1827	. . 3 ⊢ (∀𝑖(𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∀𝑖∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
29		df-ral 3066	. . 3 ⊢ (∀𝑖 ∈ 𝑛 (𝜌 → 𝜂) ↔ ∀𝑖(𝑖 ∈ 𝑛 → (𝜌 → 𝜂)))
30		bnj1090.19	. . . . . 6 ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓))
31	30	imbi1i 353	. . . . 5 ⊢ ((𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
32	31	exbii 1855	. . . 4 ⊢ (∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
33	32	albii 1827	. . 3 ⊢ (∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ∀𝑖∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
34	28, 29, 33	3bitr4i 306	. 2 ⊢ (∀𝑖 ∈ 𝑛 (𝜌 → 𝜂) ↔ ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵))
35	1, 34	sylibr 237	1 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541  ∃wex 1787   ∈ wcel 2110  ∀wral 3061  [wsbc 3694   ⊆ wss 3866   class class class wbr 5053   E cep 5459  dom cdm 5551  ‘cfv 6380   ∧ w-bnj17 32377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-ex 1788  df-ral 3066  df-bnj17 32378

This theorem is referenced by:  bnj1030  32680