Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-charfunr GIF version

Theorem bj-charfunr 13344
 Description: If a class 𝐴 has a "weak" characteristic function on a class 𝑋, then negated membership in 𝐴 is decidable (in other words, membership in 𝐴 is testable) in 𝑋. The hypothesis imposes that 𝑋 be a set. As usual, it could be formulated as ⊢ (𝜑 → (𝐹:𝑋⟶ω ∧ ...)) to deal with general classes, but that extra generality would not make the theorem much more useful. The theorem would still hold if the codomain of 𝑓 were any class with testable equality to the point where (𝑋 ∖ 𝐴) is sent. (Contributed by BJ, 6-Aug-2024.)
Hypothesis
Ref Expression
bj-charfunr.1 (𝜑 → ∃𝑓 ∈ (ω ↑𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅))
Assertion
Ref Expression
bj-charfunr (𝜑 → ∀𝑥𝑋 DECID ¬ 𝑥𝐴)
Distinct variable groups:   𝐴,𝑓   𝑓,𝑋   𝜑,𝑓,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝑋(𝑥)

Proof of Theorem bj-charfunr
StepHypRef Expression
1 bj-charfunr.1 . . . . 5 (𝜑 → ∃𝑓 ∈ (ω ↑𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅))
2 elmapi 6608 . . . . . . . . . 10 (𝑓 ∈ (ω ↑𝑚 𝑋) → 𝑓:𝑋⟶ω)
3 ffvelrn 5597 . . . . . . . . . . 11 ((𝑓:𝑋⟶ω ∧ 𝑥𝑋) → (𝑓𝑥) ∈ ω)
43ex 114 . . . . . . . . . 10 (𝑓:𝑋⟶ω → (𝑥𝑋 → (𝑓𝑥) ∈ ω))
52, 4syl 14 . . . . . . . . 9 (𝑓 ∈ (ω ↑𝑚 𝑋) → (𝑥𝑋 → (𝑓𝑥) ∈ ω))
6 0elnn 4576 . . . . . . . . . 10 ((𝑓𝑥) ∈ ω → ((𝑓𝑥) = ∅ ∨ ∅ ∈ (𝑓𝑥)))
7 nn0eln0 4577 . . . . . . . . . . 11 ((𝑓𝑥) ∈ ω → (∅ ∈ (𝑓𝑥) ↔ (𝑓𝑥) ≠ ∅))
87orbi2d 780 . . . . . . . . . 10 ((𝑓𝑥) ∈ ω → (((𝑓𝑥) = ∅ ∨ ∅ ∈ (𝑓𝑥)) ↔ ((𝑓𝑥) = ∅ ∨ (𝑓𝑥) ≠ ∅)))
96, 8mpbid 146 . . . . . . . . 9 ((𝑓𝑥) ∈ ω → ((𝑓𝑥) = ∅ ∨ (𝑓𝑥) ≠ ∅))
105, 9syl6 33 . . . . . . . 8 (𝑓 ∈ (ω ↑𝑚 𝑋) → (𝑥𝑋 → ((𝑓𝑥) = ∅ ∨ (𝑓𝑥) ≠ ∅)))
1110adantr 274 . . . . . . 7 ((𝑓 ∈ (ω ↑𝑚 𝑋) ∧ (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅)) → (𝑥𝑋 → ((𝑓𝑥) = ∅ ∨ (𝑓𝑥) ≠ ∅)))
12 elin 3290 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑋𝐴) ↔ (𝑥𝑋𝑥𝐴))
13 rsp 2504 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ → (𝑥 ∈ (𝑋𝐴) → (𝑓𝑥) ≠ ∅))
1412, 13syl5bir 152 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ → ((𝑥𝑋𝑥𝐴) → (𝑓𝑥) ≠ ∅))
1514expd 256 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ → (𝑥𝑋 → (𝑥𝐴 → (𝑓𝑥) ≠ ∅)))
1615adantr 274 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) → (𝑥𝑋 → (𝑥𝐴 → (𝑓𝑥) ≠ ∅)))
1716imp 123 . . . . . . . . . . 11 (((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) ∧ 𝑥𝑋) → (𝑥𝐴 → (𝑓𝑥) ≠ ∅))
1817necon2bd 2385 . . . . . . . . . 10 (((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) ∧ 𝑥𝑋) → ((𝑓𝑥) = ∅ → ¬ 𝑥𝐴))
19 eldif 3111 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑋𝐴) ↔ (𝑥𝑋 ∧ ¬ 𝑥𝐴))
20 rsp 2504 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅ → (𝑥 ∈ (𝑋𝐴) → (𝑓𝑥) = ∅))
2119, 20syl5bir 152 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅ → ((𝑥𝑋 ∧ ¬ 𝑥𝐴) → (𝑓𝑥) = ∅))
2221expd 256 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅ → (𝑥𝑋 → (¬ 𝑥𝐴 → (𝑓𝑥) = ∅)))
2322adantl 275 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) → (𝑥𝑋 → (¬ 𝑥𝐴 → (𝑓𝑥) = ∅)))
2423imp 123 . . . . . . . . . . 11 (((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) ∧ 𝑥𝑋) → (¬ 𝑥𝐴 → (𝑓𝑥) = ∅))
2524necon3ad 2369 . . . . . . . . . 10 (((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) ∧ 𝑥𝑋) → ((𝑓𝑥) ≠ ∅ → ¬ ¬ 𝑥𝐴))
2618, 25orim12d 776 . . . . . . . . 9 (((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) ∧ 𝑥𝑋) → (((𝑓𝑥) = ∅ ∨ (𝑓𝑥) ≠ ∅) → (¬ 𝑥𝐴 ∨ ¬ ¬ 𝑥𝐴)))
2726ex 114 . . . . . . . 8 ((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) → (𝑥𝑋 → (((𝑓𝑥) = ∅ ∨ (𝑓𝑥) ≠ ∅) → (¬ 𝑥𝐴 ∨ ¬ ¬ 𝑥𝐴))))
2827adantl 275 . . . . . . 7 ((𝑓 ∈ (ω ↑𝑚 𝑋) ∧ (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅)) → (𝑥𝑋 → (((𝑓𝑥) = ∅ ∨ (𝑓𝑥) ≠ ∅) → (¬ 𝑥𝐴 ∨ ¬ ¬ 𝑥𝐴))))
2911, 28mpdd 41 . . . . . 6 ((𝑓 ∈ (ω ↑𝑚 𝑋) ∧ (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅)) → (𝑥𝑋 → (¬ 𝑥𝐴 ∨ ¬ ¬ 𝑥𝐴)))
3029adantl 275 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (ω ↑𝑚 𝑋) ∧ (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅))) → (𝑥𝑋 → (¬ 𝑥𝐴 ∨ ¬ ¬ 𝑥𝐴)))
311, 30rexlimddv 2579 . . . 4 (𝜑 → (𝑥𝑋 → (¬ 𝑥𝐴 ∨ ¬ ¬ 𝑥𝐴)))
3231imp 123 . . 3 ((𝜑𝑥𝑋) → (¬ 𝑥𝐴 ∨ ¬ ¬ 𝑥𝐴))
33 df-dc 821 . . 3 (DECID ¬ 𝑥𝐴 ↔ (¬ 𝑥𝐴 ∨ ¬ ¬ 𝑥𝐴))
3432, 33sylibr 133 . 2 ((𝜑𝑥𝑋) → DECID ¬ 𝑥𝐴)
3534ralrimiva 2530 1 (𝜑 → ∀𝑥𝑋 DECID ¬ 𝑥𝐴)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∨ wo 698  DECID wdc 820   = wceq 1335   ∈ wcel 2128   ≠ wne 2327  ∀wral 2435  ∃wrex 2436   ∖ cdif 3099   ∩ cin 3101  ∅c0 3394  ωcom 4547  ⟶wf 5163  ‘cfv 5167  (class class class)co 5818   ↑𝑚 cmap 6586 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-nul 4090  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-iinf 4545 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-ne 2328  df-ral 2440  df-rex 2441  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-br 3966  df-opab 4026  df-id 4252  df-suc 4330  df-iom 4548  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-fv 5175  df-ov 5821  df-oprab 5822  df-mpo 5823  df-map 6588 This theorem is referenced by:  bj-charfunbi  13345
 Copyright terms: Public domain W3C validator