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

Theorem bnj605 31305
Description: Technical lemma. 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
bnj605.5 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
bnj605.13 (𝜑″[𝑓 / 𝑓]𝜑)
bnj605.14 (𝜓″[𝑓 / 𝑓]𝜓)
bnj605.17 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
bnj605.19 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
bnj605.28 𝑓 ∈ V
bnj605.31 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
bnj605.32 (𝜑″ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
bnj605.33 (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj605.37 ((𝑛 ≠ 1𝑜𝑛𝐷) → ∃𝑚𝑝𝜂)
bnj605.38 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
bnj605.41 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝑓 Fn 𝑛)
bnj605.42 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜑″)
bnj605.43 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜓″)
Assertion
Ref Expression
bnj605 ((𝑛 ≠ 1𝑜𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Distinct variable groups:   𝐴,𝑓,𝑚   𝐴,𝑝,𝑓   𝑅,𝑓,𝑚   𝑅,𝑝   𝜂,𝑓   𝑚,𝑛   𝜑,𝑚   𝜓,𝑚   𝑥,𝑚   𝑛,𝑝   𝜑,𝑝   𝜓,𝑝   𝜃,𝑝   𝑥,𝑝
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜓(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜒(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜃(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛)   𝜏(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜂(𝑥,𝑦,𝑖,𝑚,𝑛,𝑝)   𝐴(𝑥,𝑦,𝑖,𝑛)   𝐷(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝑅(𝑥,𝑦,𝑖,𝑛)   𝜑′(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜓′(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜒′(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜑″(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜓″(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)

Proof of Theorem bnj605
StepHypRef Expression
1 bnj605.37 . . . . 5 ((𝑛 ≠ 1𝑜𝑛𝐷) → ∃𝑚𝑝𝜂)
21anim1i 604 . . . 4 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → (∃𝑚𝑝𝜂𝜃))
3 nfv 2005 . . . . . . 7 𝑝𝜃
4319.41 2272 . . . . . 6 (∃𝑝(𝜂𝜃) ↔ (∃𝑝𝜂𝜃))
54exbii 1933 . . . . 5 (∃𝑚𝑝(𝜂𝜃) ↔ ∃𝑚(∃𝑝𝜂𝜃))
6 bnj605.5 . . . . . . . 8 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
76bnj1095 31180 . . . . . . 7 (𝜃 → ∀𝑚𝜃)
87nf5i 2191 . . . . . 6 𝑚𝜃
9819.41 2272 . . . . 5 (∃𝑚(∃𝑝𝜂𝜃) ↔ (∃𝑚𝑝𝜂𝜃))
105, 9bitr2i 267 . . . 4 ((∃𝑚𝑝𝜂𝜃) ↔ ∃𝑚𝑝(𝜂𝜃))
112, 10sylib 209 . . 3 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ∃𝑚𝑝(𝜂𝜃))
12 bnj605.19 . . . . . . . . . 10 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
1312bnj1232 31202 . . . . . . . . 9 (𝜂𝑚𝐷)
14 bnj219 31130 . . . . . . . . . 10 (𝑛 = suc 𝑚𝑚 E 𝑛)
1512, 14bnj770 31161 . . . . . . . . 9 (𝜂𝑚 E 𝑛)
1613, 15jca 503 . . . . . . . 8 (𝜂 → (𝑚𝐷𝑚 E 𝑛))
1716anim1i 604 . . . . . . 7 ((𝜂𝜃) → ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
18 bnj170 31095 . . . . . . 7 ((𝜃𝑚𝐷𝑚 E 𝑛) ↔ ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
1917, 18sylibr 225 . . . . . 6 ((𝜂𝜃) → (𝜃𝑚𝐷𝑚 E 𝑛))
20 bnj605.38 . . . . . 6 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
2119, 20syl 17 . . . . 5 ((𝜂𝜃) → 𝜒′)
22 simpl 470 . . . . 5 ((𝜂𝜃) → 𝜂)
2321, 22jca 503 . . . 4 ((𝜂𝜃) → (𝜒′𝜂))
24232eximi 1920 . . 3 (∃𝑚𝑝(𝜂𝜃) → ∃𝑚𝑝(𝜒′𝜂))
25 bnj248 31097 . . . . . . . 8 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) ↔ (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) ∧ 𝜂))
26 bnj605.31 . . . . . . . . . . 11 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
27 pm3.35 828 . . . . . . . . . . 11 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
2826, 27sylan2b 583 . . . . . . . . . 10 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
29 euex 2663 . . . . . . . . . 10 (∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
3028, 29syl 17 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
31 bnj605.17 . . . . . . . . 9 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
3230, 31bnj1198 31194 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
3325, 32bnj832 31156 . . . . . . 7 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → ∃𝑓𝜏)
34 bnj605.41 . . . . . . . . . . . . . 14 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝑓 Fn 𝑛)
35 bnj605.42 . . . . . . . . . . . . . 14 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜑″)
36 bnj605.43 . . . . . . . . . . . . . 14 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜓″)
3734, 35, 363jca 1151 . . . . . . . . . . . . 13 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝑓 Fn 𝑛𝜑″𝜓″))
38373com23 1149 . . . . . . . . . . . 12 ((𝑅 FrSe 𝐴𝜂𝜏) → (𝑓 Fn 𝑛𝜑″𝜓″))
39383expia 1143 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝜂) → (𝜏 → (𝑓 Fn 𝑛𝜑″𝜓″)))
4039eximdv 2008 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4140adantlr 697 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4241adantlr 697 . . . . . . . 8 ((((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) ∧ 𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4325, 42sylbi 208 . . . . . . 7 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4433, 43mpd 15 . . . . . 6 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″))
45 bnj432 31113 . . . . . 6 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) ↔ ((𝜒′𝜂) ∧ (𝑅 FrSe 𝐴𝑥𝐴)))
46 biid 252 . . . . . . . 8 (𝑓 Fn 𝑛𝑓 Fn 𝑛)
47 bnj605.13 . . . . . . . . 9 (𝜑″[𝑓 / 𝑓]𝜑)
48 sbcid 3657 . . . . . . . . 9 ([𝑓 / 𝑓]𝜑𝜑)
4947, 48bitri 266 . . . . . . . 8 (𝜑″𝜑)
50 bnj605.14 . . . . . . . . 9 (𝜓″[𝑓 / 𝑓]𝜓)
51 sbcid 3657 . . . . . . . . 9 ([𝑓 / 𝑓]𝜓𝜓)
5250, 51bitri 266 . . . . . . . 8 (𝜓″𝜓)
5346, 49, 523anbi123i 1187 . . . . . . 7 ((𝑓 Fn 𝑛𝜑″𝜓″) ↔ (𝑓 Fn 𝑛𝜑𝜓))
5453exbii 1933 . . . . . 6 (∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″) ↔ ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
5544, 45, 543imtr3i 282 . . . . 5 (((𝜒′𝜂) ∧ (𝑅 FrSe 𝐴𝑥𝐴)) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
5655ex 399 . . . 4 ((𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
5756exlimivv 2023 . . 3 (∃𝑚𝑝(𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
5811, 24, 573syl 18 . 2 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
59583impa 1129 1 ((𝑛 ≠ 1𝑜𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2157  ∃!weu 2637  wne 2985  wral 3103  Vcvv 3398  [wsbc 3640  c0 4123   ciun 4719   class class class wbr 4851   E cep 5230  suc csuc 5945   Fn wfn 6099  cfv 6104  ωcom 7298  1𝑜c1o 7792  w-bnj17 31083   predc-bnj14 31085   FrSe w-bnj15 31089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pr 5103
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-br 4852  df-opab 4914  df-eprel 5231  df-suc 5949  df-bnj17 31084
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator