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 31103
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 591 . . . 4 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → (∃𝑚𝑝𝜂𝜃))
3 nfv 1883 . . . . . . 7 𝑝𝜃
4319.41 2141 . . . . . 6 (∃𝑝(𝜂𝜃) ↔ (∃𝑝𝜂𝜃))
54exbii 1814 . . . . 5 (∃𝑚𝑝(𝜂𝜃) ↔ ∃𝑚(∃𝑝𝜂𝜃))
6 bnj605.5 . . . . . . . 8 (𝜃 ↔ ∀𝑚𝐷 (𝑚 E 𝑛[𝑚 / 𝑛]𝜒))
76bnj1095 30978 . . . . . . 7 (𝜃 → ∀𝑚𝜃)
87nf5i 2064 . . . . . 6 𝑚𝜃
9819.41 2141 . . . . 5 (∃𝑚(∃𝑝𝜂𝜃) ↔ (∃𝑚𝑝𝜂𝜃))
105, 9bitr2i 265 . . . 4 ((∃𝑚𝑝𝜂𝜃) ↔ ∃𝑚𝑝(𝜂𝜃))
112, 10sylib 208 . . 3 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ∃𝑚𝑝(𝜂𝜃))
12 bnj605.19 . . . . . . . . . 10 (𝜂 ↔ (𝑚𝐷𝑛 = suc 𝑚𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
1312bnj1232 31000 . . . . . . . . 9 (𝜂𝑚𝐷)
14 bnj219 30927 . . . . . . . . . 10 (𝑛 = suc 𝑚𝑚 E 𝑛)
1512, 14bnj770 30959 . . . . . . . . 9 (𝜂𝑚 E 𝑛)
1613, 15jca 553 . . . . . . . 8 (𝜂 → (𝑚𝐷𝑚 E 𝑛))
1716anim1i 591 . . . . . . 7 ((𝜂𝜃) → ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
18 bnj170 30892 . . . . . . 7 ((𝜃𝑚𝐷𝑚 E 𝑛) ↔ ((𝑚𝐷𝑚 E 𝑛) ∧ 𝜃))
1917, 18sylibr 224 . . . . . 6 ((𝜂𝜃) → (𝜃𝑚𝐷𝑚 E 𝑛))
20 bnj605.38 . . . . . 6 ((𝜃𝑚𝐷𝑚 E 𝑛) → 𝜒′)
2119, 20syl 17 . . . . 5 ((𝜂𝜃) → 𝜒′)
22 simpl 472 . . . . 5 ((𝜂𝜃) → 𝜂)
2321, 22jca 553 . . . 4 ((𝜂𝜃) → (𝜒′𝜂))
24232eximi 1803 . . 3 (∃𝑚𝑝(𝜂𝜃) → ∃𝑚𝑝(𝜒′𝜂))
25 bnj248 30894 . . . . . . . 8 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) ↔ (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) ∧ 𝜂))
26 bnj605.31 . . . . . . . . . . 11 (𝜒′ ↔ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′)))
27 pm3.35 610 . . . . . . . . . . 11 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ ((𝑅 FrSe 𝐴𝑥𝐴) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
2826, 27sylan2b 491 . . . . . . . . . 10 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
29 euex 2522 . . . . . . . . . 10 (∃!𝑓(𝑓 Fn 𝑚𝜑′𝜓′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
3028, 29syl 17 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓(𝑓 Fn 𝑚𝜑′𝜓′))
31 bnj605.17 . . . . . . . . 9 (𝜏 ↔ (𝑓 Fn 𝑚𝜑′𝜓′))
3230, 31bnj1198 30992 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) → ∃𝑓𝜏)
3325, 32bnj832 30954 . . . . . . 7 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → ∃𝑓𝜏)
34 bnj605.41 . . . . . . . . . . . . . 14 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝑓 Fn 𝑛)
35 bnj605.42 . . . . . . . . . . . . . 14 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜑″)
36 bnj605.43 . . . . . . . . . . . . . 14 ((𝑅 FrSe 𝐴𝜏𝜂) → 𝜓″)
3734, 35, 363jca 1261 . . . . . . . . . . . . 13 ((𝑅 FrSe 𝐴𝜏𝜂) → (𝑓 Fn 𝑛𝜑″𝜓″))
38373com23 1291 . . . . . . . . . . . 12 ((𝑅 FrSe 𝐴𝜂𝜏) → (𝑓 Fn 𝑛𝜑″𝜓″))
39383expia 1286 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝜂) → (𝜏 → (𝑓 Fn 𝑛𝜑″𝜓″)))
4039eximdv 1886 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4140adantlr 751 . . . . . . . . 9 (((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4241adantlr 751 . . . . . . . 8 ((((𝑅 FrSe 𝐴𝑥𝐴) ∧ 𝜒′) ∧ 𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4325, 42sylbi 207 . . . . . . 7 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → (∃𝑓𝜏 → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″)))
4433, 43mpd 15 . . . . . 6 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) → ∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″))
45 bnj432 30910 . . . . . 6 ((𝑅 FrSe 𝐴𝑥𝐴𝜒′𝜂) ↔ ((𝜒′𝜂) ∧ (𝑅 FrSe 𝐴𝑥𝐴)))
46 biid 251 . . . . . . . 8 (𝑓 Fn 𝑛𝑓 Fn 𝑛)
47 bnj605.13 . . . . . . . . 9 (𝜑″[𝑓 / 𝑓]𝜑)
48 sbcid 3485 . . . . . . . . 9 ([𝑓 / 𝑓]𝜑𝜑)
4947, 48bitri 264 . . . . . . . 8 (𝜑″𝜑)
50 bnj605.14 . . . . . . . . 9 (𝜓″[𝑓 / 𝑓]𝜓)
51 sbcid 3485 . . . . . . . . 9 ([𝑓 / 𝑓]𝜓𝜓)
5250, 51bitri 264 . . . . . . . 8 (𝜓″𝜓)
5346, 49, 523anbi123i 1270 . . . . . . 7 ((𝑓 Fn 𝑛𝜑″𝜓″) ↔ (𝑓 Fn 𝑛𝜑𝜓))
5453exbii 1814 . . . . . 6 (∃𝑓(𝑓 Fn 𝑛𝜑″𝜓″) ↔ ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
5544, 45, 543imtr3i 280 . . . . 5 (((𝜒′𝜂) ∧ (𝑅 FrSe 𝐴𝑥𝐴)) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓))
5655ex 449 . . . 4 ((𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
5756exlimivv 1900 . . 3 (∃𝑚𝑝(𝜒′𝜂) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
5811, 24, 573syl 18 . 2 (((𝑛 ≠ 1𝑜𝑛𝐷) ∧ 𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
59583impa 1278 1 ((𝑛 ≠ 1𝑜𝑛𝐷𝜃) → ((𝑅 FrSe 𝐴𝑥𝐴) → ∃𝑓(𝑓 Fn 𝑛𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  ∃!weu 2498  wne 2823  wral 2941  Vcvv 3231  [wsbc 3468  c0 3948   ciun 4552   class class class wbr 4685   E cep 5057  suc csuc 5763   Fn wfn 5921  cfv 5926  ωcom 7107  1𝑜c1o 7598  w-bnj17 30880   predc-bnj14 30882   FrSe w-bnj15 30886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-eprel 5058  df-suc 5767  df-bnj17 30881
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator