![]() |
Mathbox for Jonathan Ben-Naim |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj1093 | Structured version Visualization version GIF version |
Description: Technical lemma for bnj69 33679. 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 |
---|---|
bnj1093.1 | ⊢ ∃𝑗(((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0) → (𝑓‘𝑖) ⊆ 𝐵) |
bnj1093.2 | ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
bnj1093.3 | ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
Ref | Expression |
---|---|
bnj1093 | ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj1093.2 | . . . . . 6 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | |
2 | 1 | bnj1095 33450 | . . . . 5 ⊢ (𝜓 → ∀𝑖𝜓) |
3 | bnj1093.3 | . . . . 5 ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) | |
4 | 2, 3 | bnj1096 33451 | . . . 4 ⊢ (𝜒 → ∀𝑖𝜒) |
5 | 4 | bnj1350 33494 | . . 3 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒) → ∀𝑖(𝜃 ∧ 𝜏 ∧ 𝜒)) |
6 | bnj1093.1 | . . . . 5 ⊢ ∃𝑗(((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0) → (𝑓‘𝑖) ⊆ 𝐵) | |
7 | impexp 452 | . . . . . 6 ⊢ ((((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒) → (𝜑0 → (𝑓‘𝑖) ⊆ 𝐵))) | |
8 | 7 | exbii 1851 | . . . . 5 ⊢ (∃𝑗(((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ∃𝑗((𝜃 ∧ 𝜏 ∧ 𝜒) → (𝜑0 → (𝑓‘𝑖) ⊆ 𝐵))) |
9 | 6, 8 | mpbi 229 | . . . 4 ⊢ ∃𝑗((𝜃 ∧ 𝜏 ∧ 𝜒) → (𝜑0 → (𝑓‘𝑖) ⊆ 𝐵)) |
10 | 9 | 19.37iv 1953 | . . 3 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒) → ∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵)) |
11 | 5, 10 | alrimih 1827 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒) → ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵)) |
12 | 11 | bnj721 33426 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 ∀wal 1540 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ∀wral 3061 ⊆ wss 3911 ∪ ciun 4955 suc csuc 6320 Fn wfn 6492 ‘cfv 6497 ωcom 7803 ∧ w-bnj17 33355 predc-bnj14 33357 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-ex 1783 df-nf 1787 df-ral 3062 df-bnj17 33356 |
This theorem is referenced by: bnj1030 33656 |
Copyright terms: Public domain | W3C validator |