bj-charfunr - Mathbox for BJ

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

Theorem bj-charfunr 13323

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**
Step	Hyp	Ref	Expression
1		bj-charfunr.1	. . . . 5 $/\$ $\$
2		elmapi 6604	. . . . . . . . . 10
3		ffvelrn 5593	. . . . . . . . . . 11 $/\$
4	3	ex 114	. . . . . . . . . 10
5	2, 4	syl 14	. . . . . . . . 9
6		0elnn 4572	. . . . . . . . . 10 $\/$
7		nn0eln0 4573	. . . . . . . . . . 11
8	7	orbi2d 780	. . . . . . . . . 10 $\/$ $\/$
9	6, 8	mpbid 146	. . . . . . . . 9 $\/$
10	5, 9	syl6 33	. . . . . . . 8 $\/$
11	10	adantr 274	. . . . . . 7 $/\$ $/\$ $\$ $\/$
12		elin 3286	. . . . . . . . . . . . . . 15 $/\$
13		rsp 2501	. . . . . . . . . . . . . . 15
14	12, 13	syl5bir 152	. . . . . . . . . . . . . 14 $/\$
15	14	expd 256	. . . . . . . . . . . . 13
16	15	adantr 274	. . . . . . . . . . . 12 $/\$ $\$
17	16	imp 123	. . . . . . . . . . 11 $/\$ $\$ $/\$
18	17	necon2bd 2382	. . . . . . . . . 10 $/\$ $\$ $/\$
19		eldif 3107	. . . . . . . . . . . . . . 15 $\$ $/\$
20		rsp 2501	. . . . . . . . . . . . . . 15 $\$ $\$
21	19, 20	syl5bir 152	. . . . . . . . . . . . . 14 $\$ $/\$
22	21	expd 256	. . . . . . . . . . . . 13 $\$
23	22	adantl 275	. . . . . . . . . . . 12 $/\$ $\$
24	23	imp 123	. . . . . . . . . . 11 $/\$ $\$ $/\$
25	24	necon3ad 2366	. . . . . . . . . 10 $/\$ $\$ $/\$
26	18, 25	orim12d 776	. . . . . . . . 9 $/\$ $\$ $/\$ $\/$ $\/$
27	26	ex 114	. . . . . . . 8 $/\$ $\$ $\/$ $\/$
28	27	adantl 275	. . . . . . 7 $/\$ $/\$ $\$ $\/$ $\/$
29	11, 28	mpdd 41	. . . . . 6 $/\$ $/\$ $\$ $\/$
30	29	adantl 275	. . . . 5 $/\$ $/\$ $/\$ $\$ $\/$
31	1, 30	rexlimddv 2576	. . . 4 $\/$
32	31	imp 123	. . 3 $/\$ $\/$
33		df-dc 821	. . 3 DECID $\/$
34	32, 33	sylibr 133	. 2 $/\$ DECID
35	34	ralrimiva 2527	1 DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103 $\/$ wo 698 DECID wdc 820

wceq 1332

wcel 2125

wne 2324

wral 2432

wrex 2433 $\$ cdif 3095

cin 3097

c0 3390

com 4543

wf 5159

cfv 5163 (class class class)co 5814

cmap 6582

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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-sep 4078 ax-nul 4086 ax-pow 4130 ax-pr 4164 ax-un 4388 ax-setind 4490 ax-iinf 4541

This theorem depends on definitions: df-bi 116 df-dc 821 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-ral 2437 df-rex 2438 df-v 2711 df-sbc 2934 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-nul 3391 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-int 3804 df-br 3962 df-opab 4022 df-id 4248 df-suc 4326 df-iom 4544 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-rn 4590 df-iota 5128 df-fun 5165 df-fn 5166 df-f 5167 df-fv 5171 df-ov 5817 df-oprab 5818 df-mpo 5819 df-map 6584

This theorem is referenced by: bj-charfunbi 13324

W3C validator