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 30231
 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 590 . . . 4 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → (∃𝑚𝑝𝜂𝜃))
3 nfv 1830 . . . . . . 7 𝑝𝜃
4319.41 2090 . . . . . 6 (∃𝑝(𝜂𝜃) ↔ (∃𝑝𝜂𝜃))
54exbii 1764 . . . . 5 (∃𝑚𝑝(𝜂𝜃) ↔ ∃𝑚(∃𝑝𝜂𝜃))
6 bnj605.5 . . . . . . . 8 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
76bnj1095 30106 . . . . . . 7 (𝜃 → ∀𝑚𝜃)
87nf5i 2011 . . . . . 6 𝑚𝜃
9819.41 2090 . . . . 5 (∃𝑚(∃𝑝𝜂𝜃) ↔ (∃𝑚𝑝𝜂𝜃))
105, 9bitr2i 264 . . . 4 ((∃𝑚𝑝𝜂𝜃) ↔ ∃𝑚𝑝(𝜂𝜃))
112, 10sylib 207 . . 3 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ∃𝑚𝑝(𝜂𝜃))
12 bnj605.19 . . . . . . . . . 10 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
1312bnj1232 30128 . . . . . . . . 9 (𝜂𝑚𝐷)
14 bnj219 30055 . . . . . . . . . 10 (𝑛 = suc 𝑚𝑚 E 𝑛)
1512, 14bnj770 30087 . . . . . . . . 9 (𝜂𝑚 E 𝑛)
1613, 15jca 553 . . . . . . . 8 (𝜂 → (𝑚𝐷𝑚 E 𝑛))
1716anim1i 590 . . . . . . 7 ((𝜂𝜃) → ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
18 bnj170 30017 . . . . . . 7 ((𝜃𝑚𝐷𝑚 E 𝑛) ↔ ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
1917, 18sylibr 223 . . . . . 6 ((𝜂𝜃) → (𝜃𝑚𝐷𝑚 E 𝑛))
20 bnj605.38 . . . . . 6 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
2119, 20syl 17 . . . . 5 ((𝜂𝜃) → 𝜒′)
22 simpl 472 . . . . 5 ((𝜂𝜃) → 𝜂)
2321, 22jca 553 . . . 4 ((𝜂𝜃) → (𝜒′𝜂))
24232eximi 1753 . . 3 (∃𝑚𝑝(𝜂𝜃) → ∃𝑚𝑝(𝜒′𝜂))
25 bnj248 30019 . . . . . . . 8 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) ↔ (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) ∧ 𝜂))
26 bnj605.31 . . . . . . . . . . 11 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
27 pm3.35 609 . . . . . . . . . . 11 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
2826, 27sylan2b 491 . . . . . . . . . 10 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
29 euex 2482 . . . . . . . . . 10 (∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
3028, 29syl 17 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
31 bnj605.17 . . . . . . . . 9 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
3230, 31bnj1198 30120 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
3325, 32bnj832 30082 . . . . . . 7 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → ∃𝑓𝜏)
34 bnj605.41 . . . . . . . . . . . . . 14 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝑓 Fn 𝑛)
35 bnj605.42 . . . . . . . . . . . . . 14 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜑″)
36 bnj605.43 . . . . . . . . . . . . . 14 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜓″)
3734, 35, 363jca 1235 . . . . . . . . . . . . 13 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝑓 Fn 𝑛𝜑″𝜓″))
38373com23 1263 . . . . . . . . . . . 12 ((𝑅 FrSe 𝐴𝜂𝜏) → (𝑓 Fn 𝑛𝜑″𝜓″))
39383expia 1259 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝜂) → (𝜏 → (𝑓 Fn 𝑛𝜑″𝜓″)))
4039eximdv 1833 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4140adantlr 747 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4241adantlr 747 . . . . . . . 8 ((((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) ∧ 𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4325, 42sylbi 206 . . . . . . 7 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4433, 43mpd 15 . . . . . 6 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″))
45 bnj432 30035 . . . . . 6 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) ↔ ((𝜒′𝜂) ∧ (𝑅 FrSe 𝐴𝑥𝐴)))
46 biid 250 . . . . . . . 8 (𝑓 Fn 𝑛𝑓 Fn 𝑛)
47 bnj605.13 . . . . . . . . 9 (𝜑″[𝑓 / 𝑓]𝜑)
48 sbcid 3419 . . . . . . . . 9 ([𝑓 / 𝑓]𝜑𝜑)
4947, 48bitri 263 . . . . . . . 8 (𝜑″𝜑)
50 bnj605.14 . . . . . . . . 9 (𝜓″[𝑓 / 𝑓]𝜓)
51 sbcid 3419 . . . . . . . . 9 ([𝑓 / 𝑓]𝜓𝜓)
5250, 51bitri 263 . . . . . . . 8 (𝜓″𝜓)
5346, 49, 523anbi123i 1244 . . . . . . 7 ((𝑓 Fn 𝑛𝜑″𝜓″) ↔ (𝑓 Fn 𝑛𝜑𝜓))
5453exbii 1764 . . . . . 6 (∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″) ↔ ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
5544, 45, 543imtr3i 279 . . . . 5 (((𝜒′𝜂) ∧ (𝑅 FrSe 𝐴𝑥𝐴)) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
5655ex 449 . . . 4 ((𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
5756exlimivv 1847 . . 3 (∃𝑚𝑝(𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
5811, 24, 573syl 18 . 2 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
59583impa 1251 1 ((𝑛 ≠ 1𝑜𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃!weu 2458   ≠ wne 2780  ∀wral 2896  Vcvv 3173  [wsbc 3402  ∅c0 3874  ∪ ciun 4455   class class class wbr 4583   E cep 4947  suc csuc 5642   Fn wfn 5799  ‘cfv 5804  ωcom 6957  1𝑜c1o 7440   ∧ w-bnj17 30005   predc-bnj14 30007   FrSe w-bnj15 30011 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-eprel 4949  df-suc 5646  df-bnj17 30006 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator