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 31795
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 614 . . . 4 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → (∃𝑚𝑝𝜂𝜃))
3 nfv 1892 . . . . . . 7 𝑝𝜃
4319.41 2202 . . . . . 6 (∃𝑝(𝜂𝜃) ↔ (∃𝑝𝜂𝜃))
54exbii 1829 . . . . 5 (∃𝑚𝑝(𝜂𝜃) ↔ ∃𝑚(∃𝑝𝜂𝜃))
6 bnj605.5 . . . . . . . 8 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
76bnj1095 31670 . . . . . . 7 (𝜃 → ∀𝑚𝜃)
87nf5i 2117 . . . . . 6 𝑚𝜃
9819.41 2202 . . . . 5 (∃𝑚(∃𝑝𝜂𝜃) ↔ (∃𝑚𝑝𝜂𝜃))
105, 9bitr2i 277 . . . 4 ((∃𝑚𝑝𝜂𝜃) ↔ ∃𝑚𝑝(𝜂𝜃))
112, 10sylib 219 . . 3 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → ∃𝑚𝑝(𝜂𝜃))
12 bnj605.19 . . . . . . . . . 10 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
1312bnj1232 31692 . . . . . . . . 9 (𝜂𝑚𝐷)
14 bnj219 31620 . . . . . . . . . 10 (𝑛 = suc 𝑚𝑚 E 𝑛)
1512, 14bnj770 31651 . . . . . . . . 9 (𝜂𝑚 E 𝑛)
1613, 15jca 512 . . . . . . . 8 (𝜂 → (𝑚𝐷𝑚 E 𝑛))
1716anim1i 614 . . . . . . 7 ((𝜂𝜃) → ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
18 bnj170 31585 . . . . . . 7 ((𝜃𝑚𝐷𝑚 E 𝑛) ↔ ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
1917, 18sylibr 235 . . . . . 6 ((𝜂𝜃) → (𝜃𝑚𝐷𝑚 E 𝑛))
20 bnj605.38 . . . . . 6 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
2119, 20syl 17 . . . . 5 ((𝜂𝜃) → 𝜒′)
22 simpl 483 . . . . 5 ((𝜂𝜃) → 𝜂)
2321, 22jca 512 . . . 4 ((𝜂𝜃) → (𝜒′𝜂))
24232eximi 1817 . . 3 (∃𝑚𝑝(𝜂𝜃) → ∃𝑚𝑝(𝜒′𝜂))
25 bnj248 31587 . . . . . . . 8 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) ↔ (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) ∧ 𝜂))
26 bnj605.31 . . . . . . . . . . 11 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
27 pm3.35 799 . . . . . . . . . . 11 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
2826, 27sylan2b 593 . . . . . . . . . 10 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
29 euex 2622 . . . . . . . . . 10 (∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
3028, 29syl 17 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
31 bnj605.17 . . . . . . . . 9 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
3230, 31bnj1198 31684 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
3325, 32bnj832 31646 . . . . . . 7 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → ∃𝑓𝜏)
34 bnj605.41 . . . . . . . . . . . . 13 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝑓 Fn 𝑛)
35 bnj605.42 . . . . . . . . . . . . 13 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜑″)
36 bnj605.43 . . . . . . . . . . . . 13 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜓″)
3734, 35, 363jca 1121 . . . . . . . . . . . 12 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝑓 Fn 𝑛𝜑″𝜓″))
38373com23 1119 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝜂𝜏) → (𝑓 Fn 𝑛𝜑″𝜓″))
39383expia 1114 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝜂) → (𝜏 → (𝑓 Fn 𝑛𝜑″𝜓″)))
4039eximdv 1895 . . . . . . . . 9 ((𝑅 FrSe 𝐴𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4140ad4ant14 748 . . . . . . . 8 ((((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) ∧ 𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4225, 41sylbi 218 . . . . . . 7 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4333, 42mpd 15 . . . . . 6 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″))
44 bnj432 31603 . . . . . 6 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) ↔ ((𝜒′𝜂) ∧ (𝑅 FrSe 𝐴𝑥𝐴)))
45 biid 262 . . . . . . . 8 (𝑓 Fn 𝑛𝑓 Fn 𝑛)
46 bnj605.13 . . . . . . . . 9 (𝜑″[𝑓 / 𝑓]𝜑)
47 sbcid 3723 . . . . . . . . 9 ([𝑓 / 𝑓]𝜑𝜑)
4846, 47bitri 276 . . . . . . . 8 (𝜑″𝜑)
49 bnj605.14 . . . . . . . . 9 (𝜓″[𝑓 / 𝑓]𝜓)
50 sbcid 3723 . . . . . . . . 9 ([𝑓 / 𝑓]𝜓𝜓)
5149, 50bitri 276 . . . . . . . 8 (𝜓″𝜓)
5245, 48, 513anbi123i 1148 . . . . . . 7 ((𝑓 Fn 𝑛𝜑″𝜓″) ↔ (𝑓 Fn 𝑛𝜑𝜓))
5352exbii 1829 . . . . . 6 (∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″) ↔ ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
5443, 44, 533imtr3i 292 . . . . 5 (((𝜒′𝜂) ∧ (𝑅 FrSe 𝐴𝑥𝐴)) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
5554ex 413 . . . 4 ((𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
5655exlimivv 1910 . . 3 (∃𝑚𝑝(𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
5711, 24, 563syl 18 . 2 (((𝑛 ≠ 1o𝑛𝐷) ∧ 𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
58573impa 1103 1 ((𝑛 ≠ 1o𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1080   = wceq 1522  wex 1761  wcel 2081  ∃!weu 2611  wne 2984  wral 3105  Vcvv 3437  [wsbc 3706  c0 4211   ciun 4825   class class class wbr 4962   E cep 5352  suc csuc 6068   Fn wfn 6220  cfv 6225  ωcom 7436  1oc1o 7946  w-bnj17 31573   predc-bnj14 31575   FrSe w-bnj15 31579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-br 4963  df-opab 5025  df-eprel 5353  df-suc 6072  df-bnj17 31574
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator