Theorem bnj1090 32253

Description: Technical lemma for bnj69 32284. 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 453	. . . . . . 7 ⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ (𝑖 ∈ 𝑛 → (𝜎 → 𝜂)))
3	2	exbii 1848	. . . . . 6 ⊢ (∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ ∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂)))
4		bnj1090.18	. . . . . . . . . 10 ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))
5	4	imbi1i 352	. . . . . . . . 9 ⊢ ((𝜎 → 𝜂) ↔ (((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
6	5	exbii 1848	. . . . . . . 8 ⊢ (∃𝑗(𝜎 → 𝜂) ↔ ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
7	6	imbi2i 338	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑛 → ∃𝑗(𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂)))
8		19.37v 1998	. . . . . . 7 ⊢ (∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(𝜎 → 𝜂)))
9		bnj1090.10	. . . . . . . . . . . 12 ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂))
10	9	bnj115 31997	. . . . . . . . . . 11 ⊢ (𝜌 ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
11		bnj1090.17	. . . . . . . . . . . . 13 ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂)
12	11	imbi2i 338	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
13	12	albii 1820	. . . . . . . . . . 11 ⊢ (∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
14	10, 13	bitr4i 280	. . . . . . . . . 10 ⊢ (𝜌 ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))
15	14	imbi1i 352	. . . . . . . . 9 ⊢ ((𝜌 → 𝜂) ↔ (∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
16		19.36v 1994	. . . . . . . . 9 ⊢ (∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂) ↔ (∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
17	15, 16	bitr4i 280	. . . . . . . 8 ⊢ ((𝜌 → 𝜂) ↔ ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))
18	17	imbi2i 338	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂)))
19	7, 8, 18	3bitr4i 305	. . . . . 6 ⊢ (∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → (𝜌 → 𝜂)))
20	3, 19	bitr2i 278	. . . . 5 ⊢ ((𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂))
21		impexp 453	. . . . . 6 ⊢ ((((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) → ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)))
22		bnj256 31978	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)))
23	22	imbi1i 352	. . . . . 6 ⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ (((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) → (𝑓‘𝑖) ⊆ 𝐵))
24		bnj1090.9	. . . . . . 7 ⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
25	24	imbi2i 338	. . . . . 6 ⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) → ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)))
26	21, 23, 25	3bitr4i 305	. . . . 5 ⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂))
27	20, 26	bnj133 31999	. . . 4 ⊢ ((𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
28	27	albii 1820	. . 3 ⊢ (∀𝑖(𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∀𝑖∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
29		df-ral 3145	. . 3 ⊢ (∀𝑖 ∈ 𝑛 (𝜌 → 𝜂) ↔ ∀𝑖(𝑖 ∈ 𝑛 → (𝜌 → 𝜂)))
30		bnj1090.19	. . . . . 6 ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓))
31	30	imbi1i 352	. . . . 5 ⊢ ((𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
32	31	exbii 1848	. . . 4 ⊢ (∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
33	32	albii 1820	. . 3 ⊢ (∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ∀𝑖∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))
34	28, 29, 33	3bitr4i 305	. 2 ⊢ (∀𝑖 ∈ 𝑛 (𝜌 → 𝜂) ↔ ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵))
35	1, 34	sylibr 236	1 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535  ∃wex 1780   ∈ wcel 2114  ∀wral 3140  [wsbc 3774   ⊆ wss 3938   class class class wbr 5068   E cep 5466  dom cdm 5557  ‘cfv 6357   ∧ w-bnj17 31958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085  df-ex 1781  df-ral 3145  df-bnj17 31959

This theorem is referenced by:  bnj1030  32261