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

Theorem bnj1001 30771
 Description: Technical lemma for bnj69 30821. 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
bnj1001.3 (𝜒 ↔ (𝑛𝐷𝑓 Fn 𝑛𝜑𝜓))
bnj1001.5 (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚𝑝 = suc 𝑛))
bnj1001.6 (𝜂 ↔ (𝑖𝑛𝑦 ∈ (𝑓𝑖)))
bnj1001.13 𝐷 = (ω ∖ {∅})
bnj1001.27 ((𝜃𝜒𝜏𝜂) → 𝜒″)
Assertion
Ref Expression
bnj1001 ((𝜃𝜒𝜏𝜂) → (𝜒″𝑖 ∈ ω ∧ suc 𝑖𝑝))

Proof of Theorem bnj1001
StepHypRef Expression
1 bnj1001.27 . 2 ((𝜃𝜒𝜏𝜂) → 𝜒″)
2 bnj1001.6 . . . . 5 (𝜂 ↔ (𝑖𝑛𝑦 ∈ (𝑓𝑖)))
32simplbi 476 . . . 4 (𝜂𝑖𝑛)
43bnj708 30569 . . 3 ((𝜃𝜒𝜏𝜂) → 𝑖𝑛)
5 bnj1001.3 . . . . . 6 (𝜒 ↔ (𝑛𝐷𝑓 Fn 𝑛𝜑𝜓))
65bnj1232 30617 . . . . 5 (𝜒𝑛𝐷)
76bnj706 30567 . . . 4 ((𝜃𝜒𝜏𝜂) → 𝑛𝐷)
8 bnj1001.13 . . . . 5 𝐷 = (ω ∖ {∅})
98bnj923 30581 . . . 4 (𝑛𝐷𝑛 ∈ ω)
107, 9syl 17 . . 3 ((𝜃𝜒𝜏𝜂) → 𝑛 ∈ ω)
11 elnn 7029 . . 3 ((𝑖𝑛𝑛 ∈ ω) → 𝑖 ∈ ω)
124, 10, 11syl2anc 692 . 2 ((𝜃𝜒𝜏𝜂) → 𝑖 ∈ ω)
13 bnj1001.5 . . . . . 6 (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚𝑝 = suc 𝑛))
1413simp3bi 1076 . . . . 5 (𝜏𝑝 = suc 𝑛)
1514bnj707 30568 . . . 4 ((𝜃𝜒𝜏𝜂) → 𝑝 = suc 𝑛)
16 nnord 7027 . . . . . . 7 (𝑛 ∈ ω → Ord 𝑛)
17 ordsucelsuc 6976 . . . . . . 7 (Ord 𝑛 → (𝑖𝑛 ↔ suc 𝑖 ∈ suc 𝑛))
189, 16, 173syl 18 . . . . . 6 (𝑛𝐷 → (𝑖𝑛 ↔ suc 𝑖 ∈ suc 𝑛))
1918biimpa 501 . . . . 5 ((𝑛𝐷𝑖𝑛) → suc 𝑖 ∈ suc 𝑛)
20 eleq2 2687 . . . . 5 (𝑝 = suc 𝑛 → (suc 𝑖𝑝 ↔ suc 𝑖 ∈ suc 𝑛))
2119, 20anim12i 589 . . . 4 (((𝑛𝐷𝑖𝑛) ∧ 𝑝 = suc 𝑛) → (suc 𝑖 ∈ suc 𝑛 ∧ (suc 𝑖𝑝 ↔ suc 𝑖 ∈ suc 𝑛)))
227, 4, 15, 21syl21anc 1322 . . 3 ((𝜃𝜒𝜏𝜂) → (suc 𝑖 ∈ suc 𝑛 ∧ (suc 𝑖𝑝 ↔ suc 𝑖 ∈ suc 𝑛)))
23 bianir 1008 . . 3 ((suc 𝑖 ∈ suc 𝑛 ∧ (suc 𝑖𝑝 ↔ suc 𝑖 ∈ suc 𝑛)) → suc 𝑖𝑝)
2422, 23syl 17 . 2 ((𝜃𝜒𝜏𝜂) → suc 𝑖𝑝)
251, 12, 243jca 1240 1 ((𝜃𝜒𝜏𝜂) → (𝜒″𝑖 ∈ ω ∧ suc 𝑖𝑝))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ∖ cdif 3556  ∅c0 3896  {csn 4153  Ord word 5686  suc csuc 5689   Fn wfn 5847  ‘cfv 5852  ωcom 7019   ∧ w-bnj17 30494 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  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-om 7020  df-bnj17 30495 This theorem is referenced by:  bnj1020  30776
 Copyright terms: Public domain W3C validator