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 32600
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 ((𝑛 ≠ 1o𝑛𝐷) → ∃𝑚𝑝𝜂)
bnj605.38 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
bnj605.41 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝑓 Fn 𝑛)
bnj605.42 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜑″)
bnj605.43 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜓″)
Assertion
Ref Expression
bnj605 ((𝑛 ≠ 1o𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Distinct variable groups:   𝐴,𝑓,𝑚   𝐴,𝑝,𝑓   𝑅,𝑓,𝑚   𝑅,𝑝   𝜂,𝑓   𝑚,𝑛   𝜑,𝑚   𝜓,𝑚   𝑥,𝑚   𝑛,𝑝   𝜑,𝑝   𝜓,𝑝   𝜃,𝑝   𝑥,𝑝
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜓(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜒(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜃(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛)   𝜏(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜂(𝑥,𝑦,𝑖,𝑚,𝑛,𝑝)   𝐴(𝑥,𝑦,𝑖,𝑛)   𝐷(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝑅(𝑥,𝑦,𝑖,𝑛)   𝜑′(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜓′(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜒′(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜑″(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)   𝜓″(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛,𝑝)

Proof of Theorem bnj605
StepHypRef Expression
1 bnj605.37 . . . . 5 ((𝑛 ≠ 1o𝑛𝐷) → ∃𝑚𝑝𝜂)
21anim1i 618 . . . 4 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → (∃𝑚𝑝𝜂𝜃))
3 nfv 1922 . . . . . . 7 𝑝𝜃
4319.41 2233 . . . . . 6 (∃𝑝(𝜂𝜃) ↔ (∃𝑝𝜂𝜃))
54exbii 1855 . . . . 5 (∃𝑚𝑝(𝜂𝜃) ↔ ∃𝑚(∃𝑝𝜂𝜃))
6 bnj605.5 . . . . . . . 8 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
76bnj1095 32474 . . . . . . 7 (𝜃 → ∀𝑚𝜃)
87nf5i 2146 . . . . . 6 𝑚𝜃
9819.41 2233 . . . . 5 (∃𝑚(∃𝑝𝜂𝜃) ↔ (∃𝑚𝑝𝜂𝜃))
105, 9bitr2i 279 . . . 4 ((∃𝑚𝑝𝜂𝜃) ↔ ∃𝑚𝑝(𝜂𝜃))
112, 10sylib 221 . . 3 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → ∃𝑚𝑝(𝜂𝜃))
12 bnj605.19 . . . . . . . . . 10 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
1312bnj1232 32496 . . . . . . . . 9 (𝜂𝑚𝐷)
14 bnj219 32424 . . . . . . . . . 10 (𝑛 = suc 𝑚𝑚 E 𝑛)
1512, 14bnj770 32455 . . . . . . . . 9 (𝜂𝑚 E 𝑛)
1613, 15jca 515 . . . . . . . 8 (𝜂 → (𝑚𝐷𝑚 E 𝑛))
1716anim1i 618 . . . . . . 7 ((𝜂𝜃) → ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
18 bnj170 32389 . . . . . . 7 ((𝜃𝑚𝐷𝑚 E 𝑛) ↔ ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
1917, 18sylibr 237 . . . . . 6 ((𝜂𝜃) → (𝜃𝑚𝐷𝑚 E 𝑛))
20 bnj605.38 . . . . . 6 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
2119, 20syl 17 . . . . 5 ((𝜂𝜃) → 𝜒′)
22 simpl 486 . . . . 5 ((𝜂𝜃) → 𝜂)
2321, 22jca 515 . . . 4 ((𝜂𝜃) → (𝜒′𝜂))
24232eximi 1843 . . 3 (∃𝑚𝑝(𝜂𝜃) → ∃𝑚𝑝(𝜒′𝜂))
25 bnj248 32391 . . . . . . . 8 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) ↔ (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) ∧ 𝜂))
26 bnj605.31 . . . . . . . . . . 11 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
27 pm3.35 803 . . . . . . . . . . 11 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
2826, 27sylan2b 597 . . . . . . . . . 10 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
29 euex 2576 . . . . . . . . . 10 (∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
3028, 29syl 17 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
31 bnj605.17 . . . . . . . . 9 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
3230, 31bnj1198 32488 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
3325, 32bnj832 32450 . . . . . . 7 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → ∃𝑓𝜏)
34 bnj605.41 . . . . . . . . . . . . 13 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝑓 Fn 𝑛)
35 bnj605.42 . . . . . . . . . . . . 13 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜑″)
36 bnj605.43 . . . . . . . . . . . . 13 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜓″)
3734, 35, 363jca 1130 . . . . . . . . . . . 12 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝑓 Fn 𝑛𝜑″𝜓″))
38373com23 1128 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝜂𝜏) → (𝑓 Fn 𝑛𝜑″𝜓″))
39383expia 1123 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝜂) → (𝜏 → (𝑓 Fn 𝑛𝜑″𝜓″)))
4039eximdv 1925 . . . . . . . . 9 ((𝑅 FrSe 𝐴𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4140ad4ant14 752 . . . . . . . 8 ((((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) ∧ 𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4225, 41sylbi 220 . . . . . . 7 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4333, 42mpd 15 . . . . . 6 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″))
44 bnj432 32407 . . . . . 6 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) ↔ ((𝜒′𝜂) ∧ (𝑅 FrSe 𝐴𝑥𝐴)))
45 biid 264 . . . . . . . 8 (𝑓 Fn 𝑛𝑓 Fn 𝑛)
46 bnj605.13 . . . . . . . . 9 (𝜑″[𝑓 / 𝑓]𝜑)
47 sbcid 3711 . . . . . . . . 9 ([𝑓 / 𝑓]𝜑𝜑)
4846, 47bitri 278 . . . . . . . 8 (𝜑″𝜑)
49 bnj605.14 . . . . . . . . 9 (𝜓″[𝑓 / 𝑓]𝜓)
50 sbcid 3711 . . . . . . . . 9 ([𝑓 / 𝑓]𝜓𝜓)
5149, 50bitri 278 . . . . . . . 8 (𝜓″𝜓)
5245, 48, 513anbi123i 1157 . . . . . . 7 ((𝑓 Fn 𝑛𝜑″𝜓″) ↔ (𝑓 Fn 𝑛𝜑𝜓))
5352exbii 1855 . . . . . 6 (∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″) ↔ ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
5443, 44, 533imtr3i 294 . . . . 5 (((𝜒′𝜂) ∧ (𝑅 FrSe 𝐴𝑥𝐴)) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
5554ex 416 . . . 4 ((𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
5655exlimivv 1940 . . 3 (∃𝑚𝑝(𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
5711, 24, 563syl 18 . 2 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
58573impa 1112 1 ((𝑛 ≠ 1o𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wex 1787  wcel 2110  ∃!weu 2567  wne 2940  wral 3061  Vcvv 3408  [wsbc 3694  c0 4237   ciun 4904   class class class wbr 5053   E cep 5459  suc csuc 6215   Fn wfn 6375  cfv 6380  ωcom 7644  1oc1o 8195  w-bnj17 32377   predc-bnj14 32379   FrSe w-bnj15 32383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3066  df-rab 3070  df-v 3410  df-sbc 3695  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-eprel 5460  df-suc 6219  df-bnj17 32378
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator