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 30752
Description: Technical lemma for bnj69 30783. 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 462 . . . . . . 7 (((𝑖𝑛𝜎) → 𝜂) ↔ (𝑖𝑛 → (𝜎𝜂)))
32exbii 1771 . . . . . 6 (∃𝑗((𝑖𝑛𝜎) → 𝜂) ↔ ∃𝑗(𝑖𝑛 → (𝜎𝜂)))
4 bnj1090.18 . . . . . . . . . 10 (𝜎 ↔ ((𝑗𝑛𝑗 E 𝑖) → 𝜂′))
54imbi1i 339 . . . . . . . . 9 ((𝜎𝜂) ↔ (((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂))
65exbii 1771 . . . . . . . 8 (∃𝑗(𝜎𝜂) ↔ ∃𝑗(((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂))
76imbi2i 326 . . . . . . 7 ((𝑖𝑛 → ∃𝑗(𝜎𝜂)) ↔ (𝑖𝑛 → ∃𝑗(((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂)))
8 19.37v 1907 . . . . . . 7 (∃𝑗(𝑖𝑛 → (𝜎𝜂)) ↔ (𝑖𝑛 → ∃𝑗(𝜎𝜂)))
9 bnj1090.10 . . . . . . . . . . . 12 (𝜌 ↔ ∀𝑗𝑛 (𝑗 E 𝑖[𝑗 / 𝑖]𝜂))
109bnj115 30496 . . . . . . . . . . 11 (𝜌 ↔ ∀𝑗((𝑗𝑛𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
11 bnj1090.17 . . . . . . . . . . . . 13 (𝜂′[𝑗 / 𝑖]𝜂)
1211imbi2i 326 . . . . . . . . . . . 12 (((𝑗𝑛𝑗 E 𝑖) → 𝜂′) ↔ ((𝑗𝑛𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
1312albii 1744 . . . . . . . . . . 11 (∀𝑗((𝑗𝑛𝑗 E 𝑖) → 𝜂′) ↔ ∀𝑗((𝑗𝑛𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂))
1410, 13bitr4i 267 . . . . . . . . . 10 (𝜌 ↔ ∀𝑗((𝑗𝑛𝑗 E 𝑖) → 𝜂′))
1514imbi1i 339 . . . . . . . . 9 ((𝜌𝜂) ↔ (∀𝑗((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂))
16 19.36v 1901 . . . . . . . . 9 (∃𝑗(((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂) ↔ (∀𝑗((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂))
1715, 16bitr4i 267 . . . . . . . 8 ((𝜌𝜂) ↔ ∃𝑗(((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂))
1817imbi2i 326 . . . . . . 7 ((𝑖𝑛 → (𝜌𝜂)) ↔ (𝑖𝑛 → ∃𝑗(((𝑗𝑛𝑗 E 𝑖) → 𝜂′) → 𝜂)))
197, 8, 183bitr4i 292 . . . . . 6 (∃𝑗(𝑖𝑛 → (𝜎𝜂)) ↔ (𝑖𝑛 → (𝜌𝜂)))
203, 19bitr2i 265 . . . . 5 ((𝑖𝑛 → (𝜌𝜂)) ↔ ∃𝑗((𝑖𝑛𝜎) → 𝜂))
21 impexp 462 . . . . . 6 ((((𝑖𝑛𝜎) ∧ (𝑓𝐾𝑖 ∈ dom 𝑓)) → (𝑓𝑖) ⊆ 𝐵) ↔ ((𝑖𝑛𝜎) → ((𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵)))
22 bnj256 30476 . . . . . . 7 ((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) ↔ ((𝑖𝑛𝜎) ∧ (𝑓𝐾𝑖 ∈ dom 𝑓)))
2322imbi1i 339 . . . . . 6 (((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵) ↔ (((𝑖𝑛𝜎) ∧ (𝑓𝐾𝑖 ∈ dom 𝑓)) → (𝑓𝑖) ⊆ 𝐵))
24 bnj1090.9 . . . . . . 7 (𝜂 ↔ ((𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
2524imbi2i 326 . . . . . 6 (((𝑖𝑛𝜎) → 𝜂) ↔ ((𝑖𝑛𝜎) → ((𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵)))
2621, 23, 253bitr4i 292 . . . . 5 (((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵) ↔ ((𝑖𝑛𝜎) → 𝜂))
2720, 26bnj133 30498 . . . 4 ((𝑖𝑛 → (𝜌𝜂)) ↔ ∃𝑗((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
2827albii 1744 . . 3 (∀𝑖(𝑖𝑛 → (𝜌𝜂)) ↔ ∀𝑖𝑗((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
29 df-ral 2912 . . 3 (∀𝑖𝑛 (𝜌𝜂) ↔ ∀𝑖(𝑖𝑛 → (𝜌𝜂)))
30 bnj1090.19 . . . . . 6 (𝜑0 ↔ (𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓))
3130imbi1i 339 . . . . 5 ((𝜑0 → (𝑓𝑖) ⊆ 𝐵) ↔ ((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
3231exbii 1771 . . . 4 (∃𝑗(𝜑0 → (𝑓𝑖) ⊆ 𝐵) ↔ ∃𝑗((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
3332albii 1744 . . 3 (∀𝑖𝑗(𝜑0 → (𝑓𝑖) ⊆ 𝐵) ↔ ∀𝑖𝑗((𝑖𝑛𝜎𝑓𝐾𝑖 ∈ dom 𝑓) → (𝑓𝑖) ⊆ 𝐵))
3428, 29, 333bitr4i 292 . 2 (∀𝑖𝑛 (𝜌𝜂) ↔ ∀𝑖𝑗(𝜑0 → (𝑓𝑖) ⊆ 𝐵))
351, 34sylibr 224 1 ((𝜃𝜏𝜒𝜁) → ∀𝑖𝑛 (𝜌𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478  wex 1701  wcel 1987  wral 2907  [wsbc 3417  wss 3555   class class class wbr 4613   E cep 4983  dom cdm 5074  cfv 5847  w-bnj17 30456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038  df-ex 1702  df-ral 2912  df-bnj17 30457
This theorem is referenced by:  bnj1030  30760
  Copyright terms: Public domain W3C validator