Theorem bnj1090 35609

Description: Technical lemma for bnj69 35640. 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 456	. . . . . . 7 ⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ (𝑖 ∈ 𝑛 → (𝜎 → 𝜂)))
3	2	exbii 1880	. . . . . 6 ⊢ (∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ ∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂)))
4		bnj1090.18	. . . . . . . . . 10 ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))
5	4	imbi1i 352	. . . . . . . . 9 ⊢ ((𝜎 → 𝜂) ↔ (((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
6	5	exbii 1880	. . . . . . . 8 ⊢ (∃𝑗(𝜎 → 𝜂) ↔ ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
7	6	imbi2i 339	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑛 → ∃𝑗(𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂)))
8		19.37v 2029	. . . . . . 7 ⊢ (∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(𝜎 → 𝜂)))
9		bnj1090.10	. . . . . . . . . . . 12 ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂))
10	9	bnj115 35356	. . . . . . . . . . 11 ⊢ (𝜌 ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
11		bnj1090.17	. . . . . . . . . . . . 13 ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂)
12	11	imbi2i 339	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
13	12	albii 1851	. . . . . . . . . . 11 ⊢ (∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
14	10, 13	bitr4i 281	. . . . . . . . . 10 ⊢ (𝜌 ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))
15	14	imbi1i 352	. . . . . . . . 9 ⊢ ((𝜌 → 𝜂) ↔ (∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
16		19.36v 2025	. . . . . . . . 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 456	. . . . . 6 ⊢ ((((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) → ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)))
22		bnj256 35337	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)))
23	22	imbi1i 352	. . . . . 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 35358	. . . 4 ⊢ ((𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
28	27	albii 1851	. . 3 ⊢ (∀𝑖(𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∀𝑖∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
29		df-ral 3077	. . 3 ⊢ (∀𝑖 ∈ 𝑛 (𝜌 → 𝜂) ↔ ∀𝑖(𝑖 ∈ 𝑛 → (𝜌 → 𝜂)))
30		bnj1090.19	. . . . . 6 ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓))
31	30	imbi1i 352	. . . . 5 ⊢ ((𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
32	31	exbii 1880	. . . 4 ⊢ (∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
33	32	albii 1851	. . 3 ⊢ (∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ∀𝑖∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
34	28, 29, 33	3bitr4i 306	. 2 ⊢ (∀𝑖 ∈ 𝑛 (𝜌 → 𝜂) ↔ ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵))
35	1, 34	sylibr 237	1 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  ∃wex 1811   ∈ wcel 2144  ∀wral 3076  [wsbc 3738   ⊆ wss 3895   class class class wbr 5102   E cep 5549  dom cdm 5650  ‘cfv 6538   ∧ w-bnj17 35317

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1812  df-ral 3077  df-bnj17 35318

This theorem is used by:  bnj1030  35617