Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ctiunctlemudc GIF version

Theorem ctiunctlemudc 12138
 Description: Lemma for ctiunct 12141. (Contributed by Jim Kingdon, 28-Oct-2023.)
Hypotheses
Ref Expression
ctiunct.som (𝜑𝑆 ⊆ ω)
ctiunct.sdc (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)
ctiunct.f (𝜑𝐹:𝑆onto𝐴)
ctiunct.tom ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)
ctiunct.tdc ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)
ctiunct.g ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)
ctiunct.j (𝜑𝐽:ω–1-1-onto→(ω × ω))
ctiunct.u 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}
Assertion
Ref Expression
ctiunctlemudc (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑈)
Distinct variable groups:   𝑥,𝐴   𝑛,𝐹,𝑥   𝑧,𝐹,𝑥   𝑛,𝐽,𝑥   𝑧,𝐽   𝑆,𝑛   𝑧,𝑆   𝑇,𝑛   𝑧,𝑇   𝑈,𝑛   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑧,𝑛)   𝐴(𝑧,𝑛)   𝐵(𝑥,𝑧,𝑛)   𝑆(𝑥)   𝑇(𝑥)   𝑈(𝑥,𝑧)   𝐺(𝑥,𝑧,𝑛)

Proof of Theorem ctiunctlemudc
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 eleq1 2220 . . . . . . . . 9 (𝑛 = (1st ‘(𝐽𝑚)) → (𝑛𝑆 ↔ (1st ‘(𝐽𝑚)) ∈ 𝑆))
21dcbid 824 . . . . . . . 8 (𝑛 = (1st ‘(𝐽𝑚)) → (DECID 𝑛𝑆DECID (1st ‘(𝐽𝑚)) ∈ 𝑆))
3 ctiunct.sdc . . . . . . . . 9 (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)
43adantr 274 . . . . . . . 8 ((𝜑𝑚 ∈ ω) → ∀𝑛 ∈ ω DECID 𝑛𝑆)
5 ctiunct.j . . . . . . . . . . . 12 (𝜑𝐽:ω–1-1-onto→(ω × ω))
65adantr 274 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ω) → 𝐽:ω–1-1-onto→(ω × ω))
7 f1of 5411 . . . . . . . . . . 11 (𝐽:ω–1-1-onto→(ω × ω) → 𝐽:ω⟶(ω × ω))
86, 7syl 14 . . . . . . . . . 10 ((𝜑𝑚 ∈ ω) → 𝐽:ω⟶(ω × ω))
9 simpr 109 . . . . . . . . . 10 ((𝜑𝑚 ∈ ω) → 𝑚 ∈ ω)
108, 9ffvelrnd 5600 . . . . . . . . 9 ((𝜑𝑚 ∈ ω) → (𝐽𝑚) ∈ (ω × ω))
11 xp1st 6107 . . . . . . . . 9 ((𝐽𝑚) ∈ (ω × ω) → (1st ‘(𝐽𝑚)) ∈ ω)
1210, 11syl 14 . . . . . . . 8 ((𝜑𝑚 ∈ ω) → (1st ‘(𝐽𝑚)) ∈ ω)
132, 4, 12rspcdva 2821 . . . . . . 7 ((𝜑𝑚 ∈ ω) → DECID (1st ‘(𝐽𝑚)) ∈ 𝑆)
1413adantr 274 . . . . . 6 (((𝜑𝑚 ∈ ω) ∧ (1st ‘(𝐽𝑚)) ∈ 𝑆) → DECID (1st ‘(𝐽𝑚)) ∈ 𝑆)
15 eleq1 2220 . . . . . . . 8 (𝑛 = (2nd ‘(𝐽𝑚)) → (𝑛(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇 ↔ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
1615dcbid 824 . . . . . . 7 (𝑛 = (2nd ‘(𝐽𝑚)) → (DECID 𝑛(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇DECID (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
17 ctiunct.f . . . . . . . . . . 11 (𝜑𝐹:𝑆onto𝐴)
18 fof 5389 . . . . . . . . . . 11 (𝐹:𝑆onto𝐴𝐹:𝑆𝐴)
1917, 18syl 14 . . . . . . . . . 10 (𝜑𝐹:𝑆𝐴)
2019ad2antrr 480 . . . . . . . . 9 (((𝜑𝑚 ∈ ω) ∧ (1st ‘(𝐽𝑚)) ∈ 𝑆) → 𝐹:𝑆𝐴)
21 simpr 109 . . . . . . . . 9 (((𝜑𝑚 ∈ ω) ∧ (1st ‘(𝐽𝑚)) ∈ 𝑆) → (1st ‘(𝐽𝑚)) ∈ 𝑆)
2220, 21ffvelrnd 5600 . . . . . . . 8 (((𝜑𝑚 ∈ ω) ∧ (1st ‘(𝐽𝑚)) ∈ 𝑆) → (𝐹‘(1st ‘(𝐽𝑚))) ∈ 𝐴)
23 ctiunct.tdc . . . . . . . . . 10 ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)
2423ralrimiva 2530 . . . . . . . . 9 (𝜑 → ∀𝑥𝐴𝑛 ∈ ω DECID 𝑛𝑇)
2524ad2antrr 480 . . . . . . . 8 (((𝜑𝑚 ∈ ω) ∧ (1st ‘(𝐽𝑚)) ∈ 𝑆) → ∀𝑥𝐴𝑛 ∈ ω DECID 𝑛𝑇)
26 nfcv 2299 . . . . . . . . . 10 𝑥ω
27 nfcsb1v 3064 . . . . . . . . . . . 12 𝑥(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇
2827nfcri 2293 . . . . . . . . . . 11 𝑥 𝑛(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇
2928nfdc 1639 . . . . . . . . . 10 𝑥DECID 𝑛(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇
3026, 29nfralya 2497 . . . . . . . . 9 𝑥𝑛 ∈ ω DECID 𝑛(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇
31 csbeq1a 3040 . . . . . . . . . . . 12 (𝑥 = (𝐹‘(1st ‘(𝐽𝑚))) → 𝑇 = (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)
3231eleq2d 2227 . . . . . . . . . . 11 (𝑥 = (𝐹‘(1st ‘(𝐽𝑚))) → (𝑛𝑇𝑛(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
3332dcbid 824 . . . . . . . . . 10 (𝑥 = (𝐹‘(1st ‘(𝐽𝑚))) → (DECID 𝑛𝑇DECID 𝑛(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
3433ralbidv 2457 . . . . . . . . 9 (𝑥 = (𝐹‘(1st ‘(𝐽𝑚))) → (∀𝑛 ∈ ω DECID 𝑛𝑇 ↔ ∀𝑛 ∈ ω DECID 𝑛(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
3530, 34rspc 2810 . . . . . . . 8 ((𝐹‘(1st ‘(𝐽𝑚))) ∈ 𝐴 → (∀𝑥𝐴𝑛 ∈ ω DECID 𝑛𝑇 → ∀𝑛 ∈ ω DECID 𝑛(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
3622, 25, 35sylc 62 . . . . . . 7 (((𝜑𝑚 ∈ ω) ∧ (1st ‘(𝐽𝑚)) ∈ 𝑆) → ∀𝑛 ∈ ω DECID 𝑛(𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)
3710adantr 274 . . . . . . . 8 (((𝜑𝑚 ∈ ω) ∧ (1st ‘(𝐽𝑚)) ∈ 𝑆) → (𝐽𝑚) ∈ (ω × ω))
38 xp2nd 6108 . . . . . . . 8 ((𝐽𝑚) ∈ (ω × ω) → (2nd ‘(𝐽𝑚)) ∈ ω)
3937, 38syl 14 . . . . . . 7 (((𝜑𝑚 ∈ ω) ∧ (1st ‘(𝐽𝑚)) ∈ 𝑆) → (2nd ‘(𝐽𝑚)) ∈ ω)
4016, 36, 39rspcdva 2821 . . . . . 6 (((𝜑𝑚 ∈ ω) ∧ (1st ‘(𝐽𝑚)) ∈ 𝑆) → DECID (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)
41 dcan 919 . . . . . 6 (DECID (1st ‘(𝐽𝑚)) ∈ 𝑆 → (DECID (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇DECID ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)))
4214, 40, 41sylc 62 . . . . 5 (((𝜑𝑚 ∈ ω) ∧ (1st ‘(𝐽𝑚)) ∈ 𝑆) → DECID ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
43 simpr 109 . . . . . . . 8 (((𝜑𝑚 ∈ ω) ∧ ¬ (1st ‘(𝐽𝑚)) ∈ 𝑆) → ¬ (1st ‘(𝐽𝑚)) ∈ 𝑆)
4443intnanrd 918 . . . . . . 7 (((𝜑𝑚 ∈ ω) ∧ ¬ (1st ‘(𝐽𝑚)) ∈ 𝑆) → ¬ ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
4544olcd 724 . . . . . 6 (((𝜑𝑚 ∈ ω) ∧ ¬ (1st ‘(𝐽𝑚)) ∈ 𝑆) → (((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇) ∨ ¬ ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)))
46 df-dc 821 . . . . . 6 (DECID ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇) ↔ (((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇) ∨ ¬ ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)))
4745, 46sylibr 133 . . . . 5 (((𝜑𝑚 ∈ ω) ∧ ¬ (1st ‘(𝐽𝑚)) ∈ 𝑆) → DECID ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
48 exmiddc 822 . . . . . 6 (DECID (1st ‘(𝐽𝑚)) ∈ 𝑆 → ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∨ ¬ (1st ‘(𝐽𝑚)) ∈ 𝑆))
4913, 48syl 14 . . . . 5 ((𝜑𝑚 ∈ ω) → ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∨ ¬ (1st ‘(𝐽𝑚)) ∈ 𝑆))
5042, 47, 49mpjaodan 788 . . . 4 ((𝜑𝑚 ∈ ω) → DECID ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
51 2fveq3 5470 . . . . . . . . 9 (𝑧 = 𝑚 → (1st ‘(𝐽𝑧)) = (1st ‘(𝐽𝑚)))
5251eleq1d 2226 . . . . . . . 8 (𝑧 = 𝑚 → ((1st ‘(𝐽𝑧)) ∈ 𝑆 ↔ (1st ‘(𝐽𝑚)) ∈ 𝑆))
53 2fveq3 5470 . . . . . . . . 9 (𝑧 = 𝑚 → (2nd ‘(𝐽𝑧)) = (2nd ‘(𝐽𝑚)))
5451fveq2d 5469 . . . . . . . . . 10 (𝑧 = 𝑚 → (𝐹‘(1st ‘(𝐽𝑧))) = (𝐹‘(1st ‘(𝐽𝑚))))
5554csbeq1d 3038 . . . . . . . . 9 (𝑧 = 𝑚(𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇 = (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)
5653, 55eleq12d 2228 . . . . . . . 8 (𝑧 = 𝑚 → ((2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇 ↔ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))
5752, 56anbi12d 465 . . . . . . 7 (𝑧 = 𝑚 → (((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇) ↔ ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)))
58 ctiunct.u . . . . . . 7 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}
5957, 58elrab2 2871 . . . . . 6 (𝑚𝑈 ↔ (𝑚 ∈ ω ∧ ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)))
60 ibar 299 . . . . . . 7 (𝑚 ∈ ω → (((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇) ↔ (𝑚 ∈ ω ∧ ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))))
6160adantl 275 . . . . . 6 ((𝜑𝑚 ∈ ω) → (((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇) ↔ (𝑚 ∈ ω ∧ ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇))))
6259, 61bitr4id 198 . . . . 5 ((𝜑𝑚 ∈ ω) → (𝑚𝑈 ↔ ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)))
6362dcbid 824 . . . 4 ((𝜑𝑚 ∈ ω) → (DECID 𝑚𝑈DECID ((1st ‘(𝐽𝑚)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑚)) ∈ (𝐹‘(1st ‘(𝐽𝑚))) / 𝑥𝑇)))
6450, 63mpbird 166 . . 3 ((𝜑𝑚 ∈ ω) → DECID 𝑚𝑈)
6564ralrimiva 2530 . 2 (𝜑 → ∀𝑚 ∈ ω DECID 𝑚𝑈)
66 eleq1 2220 . . . 4 (𝑚 = 𝑛 → (𝑚𝑈𝑛𝑈))
6766dcbid 824 . . 3 (𝑚 = 𝑛 → (DECID 𝑚𝑈DECID 𝑛𝑈))
6867cbvralv 2680 . 2 (∀𝑚 ∈ ω DECID 𝑚𝑈 ↔ ∀𝑛 ∈ ω DECID 𝑛𝑈)
6965, 68sylib 121 1 (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑈)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820   = wceq 1335   ∈ wcel 2128  ∀wral 2435  {crab 2439  ⦋csb 3031   ⊆ wss 3102  ωcom 4547   × cxp 4581  ⟶wf 5163  –onto→wfo 5165  –1-1-onto→wf1o 5166  ‘cfv 5167  1st c1st 6080  2nd c2nd 6081 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168  ax-un 4392 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-mpt 4027  df-id 4252  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-f1 5172  df-fo 5173  df-f1o 5174  df-fv 5175  df-1st 6082  df-2nd 6083 This theorem is referenced by:  ctiunct  12141
 Copyright terms: Public domain W3C validator