Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1090 Structured version   Visualization version   GIF version

Theorem bnj1090 32148
Description: Technical lemma for bnj69 32179. 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:   𝜒(𝑓,𝑖,𝑗,𝑛)   𝜃(𝑓,𝑖,𝑗,𝑛)   𝜏(𝑓,𝑖,𝑗,𝑛)   𝜂(𝑓,𝑖,𝑛)   𝜁(𝑓,𝑖,𝑗,𝑛)   𝜎(𝑓,𝑖,𝑗,𝑛)   𝜌(𝑓,𝑖,𝑗,𝑛)   𝐵(𝑓,𝑖,𝑗,𝑛)   𝐾(𝑓,𝑖,𝑗,𝑛)   𝜂′(𝑓,𝑖,𝑗,𝑛)   𝜑0(𝑓,𝑖,𝑗,𝑛)

Proof of Theorem bnj1090
StepHypRef Expression
1 bnj1090.28 . 2 ((𝜃𝜏𝜒𝜁) → ∀𝑖𝑗(𝜑0 → (𝑓𝑖) ⊆ 𝐵))
2 impexp 451 . . . . . . 7 (((𝑖𝑛𝜎) → 𝜂) ↔ (𝑖𝑛 → (𝜎𝜂)))
32exbii 1839 . . . . . 6 (∃𝑗((𝑖𝑛𝜎) → 𝜂) ↔ ∃𝑗(𝑖𝑛 → (𝜎𝜂)))
4 bnj1090.18 . . . . . . . . . 10 (𝜎 ↔ ((𝑗𝑛𝑗 E 𝑖) → 𝜂′))
54imbi1i 351 . . . . . . . . 9 ((𝜎𝜂) ↔ (((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂))
65exbii 1839 . . . . . . . 8 (∃𝑗(𝜎𝜂) ↔ ∃𝑗(((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂))
76imbi2i 337 . . . . . . 7 ((𝑖𝑛 → ∃𝑗(𝜎𝜂)) ↔ (𝑖𝑛 → ∃𝑗(((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂)))
8 19.37v 1989 . . . . . . 7 (∃𝑗(𝑖𝑛 → (𝜎𝜂)) ↔ (𝑖𝑛 → ∃𝑗(𝜎𝜂)))
9 bnj1090.10 . . . . . . . . . . . 12 (𝜌 ↔ ∀𝑗𝑛 (𝑗 E 𝑖[𝑗 / 𝑖]𝜂))
109bnj115 31894 . . . . . . . . . . 11 (𝜌 ↔ ∀𝑗((𝑗𝑛𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
11 bnj1090.17 . . . . . . . . . . . . 13 (𝜂′[𝑗 / 𝑖]𝜂)
1211imbi2i 337 . . . . . . . . . . . 12 (((𝑗𝑛𝑗 E 𝑖) → 𝜂′) ↔ ((𝑗𝑛𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
1312albii 1811 . . . . . . . . . . 11 (∀𝑗((𝑗𝑛𝑗 E 𝑖) → 𝜂′) ↔ ∀𝑗((𝑗𝑛𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
1410, 13bitr4i 279 . . . . . . . . . 10 (𝜌 ↔ ∀𝑗((𝑗𝑛𝑗 E 𝑖) → 𝜂′))
1514imbi1i 351 . . . . . . . . 9 ((𝜌𝜂) ↔ (∀𝑗((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂))
16 19.36v 1985 . . . . . . . . 9 (∃𝑗(((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂) ↔ (∀𝑗((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂))
1715, 16bitr4i 279 . . . . . . . 8 ((𝜌𝜂) ↔ ∃𝑗(((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂))
1817imbi2i 337 . . . . . . 7 ((𝑖𝑛 → (𝜌𝜂)) ↔ (𝑖𝑛 → ∃𝑗(((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂)))
197, 8, 183bitr4i 304 . . . . . 6 (∃𝑗(𝑖𝑛 → (𝜎𝜂)) ↔ (𝑖𝑛 → (𝜌𝜂)))
203, 19bitr2i 277 . . . . 5 ((𝑖𝑛 → (𝜌𝜂)) ↔ ∃𝑗((𝑖𝑛𝜎) → 𝜂))
21 impexp 451 . . . . . 6 ((((𝑖𝑛𝜎) ∧ (𝑓𝐾𝑖 ∈ dom 𝑓)) → (𝑓𝑖) ⊆ 𝐵) ↔ ((𝑖𝑛𝜎) → ((𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵)))
22 bnj256 31875 . . . . . . 7 ((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) ↔ ((𝑖𝑛𝜎) ∧ (𝑓𝐾𝑖 ∈ dom 𝑓)))
2322imbi1i 351 . . . . . 6 (((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵) ↔ (((𝑖𝑛𝜎) ∧ (𝑓𝐾𝑖 ∈ dom 𝑓)) → (𝑓𝑖) ⊆ 𝐵))
24 bnj1090.9 . . . . . . 7 (𝜂 ↔ ((𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
2524imbi2i 337 . . . . . 6 (((𝑖𝑛𝜎) → 𝜂) ↔ ((𝑖𝑛𝜎) → ((𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵)))
2621, 23, 253bitr4i 304 . . . . 5 (((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵) ↔ ((𝑖𝑛𝜎) → 𝜂))
2720, 26bnj133 31896 . . . 4 ((𝑖𝑛 → (𝜌𝜂)) ↔ ∃𝑗((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
2827albii 1811 . . 3 (∀𝑖(𝑖𝑛 → (𝜌𝜂)) ↔ ∀𝑖𝑗((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
29 df-ral 3140 . . 3 (∀𝑖𝑛 (𝜌𝜂) ↔ ∀𝑖(𝑖𝑛 → (𝜌𝜂)))
30 bnj1090.19 . . . . . 6 (𝜑0 ↔ (𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓))
3130imbi1i 351 . . . . 5 ((𝜑0 → (𝑓𝑖) ⊆ 𝐵) ↔ ((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
3231exbii 1839 . . . 4 (∃𝑗(𝜑0 → (𝑓𝑖) ⊆ 𝐵) ↔ ∃𝑗((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
3332albii 1811 . . 3 (∀𝑖𝑗(𝜑0 → (𝑓𝑖) ⊆ 𝐵) ↔ ∀𝑖𝑗((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
3428, 29, 333bitr4i 304 . 2 (∀𝑖𝑛 (𝜌𝜂) ↔ ∀𝑖𝑗(𝜑0 → (𝑓𝑖) ⊆ 𝐵))
351, 34sylibr 235 1 ((𝜃𝜏𝜒𝜁) → ∀𝑖𝑛 (𝜌𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1526  wex 1771  wcel 2105  wral 3135  [wsbc 3769  wss 3933   class class class wbr 5057   E cep 5457  dom cdm 5548  cfv 6348  w-bnj17 31855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961
This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1081  df-ex 1772  df-ral 3140  df-bnj17 31856
This theorem is referenced by:  bnj1030  32156
  Copyright terms: Public domain W3C validator