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 13692

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 6636	. . . . . . . . . 10
3		ffvelrn 5618	. . . . . . . . . . 11 $/\$
4	3	ex 114	. . . . . . . . . 10
5	2, 4	syl 14	. . . . . . . . 9
6		0elnn 4596	. . . . . . . . . 10 $\/$
7		nn0eln0 4597	. . . . . . . . . . 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 3305	. . . . . . . . . . . . . . 15 $/\$
13		rsp 2513	. . . . . . . . . . . . . . 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 2394	. . . . . . . . . 10 $/\$ $\$ $/\$
19		eldif 3125	. . . . . . . . . . . . . . 15 $\$ $/\$
20		rsp 2513	. . . . . . . . . . . . . . 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 2378	. . . . . . . . . 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 2588	. . . 4 $\/$
32	31	imp 123	. . 3 $/\$ $\/$
33		df-dc 825	. . 3 DECID $\/$
34	32, 33	sylibr 133	. 2 $/\$ DECID
35	34	ralrimiva 2539	1 DECID

Colors of variables: wff set class

Syntax hints:

wn 3

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

wceq 1343

wcel 2136

wne 2336

wral 2444

wrex 2445 $\$ cdif 3113

cin 3115

c0 3409

com 4567

wf 5184

cfv 5188 (class class class)co 5842

cmap 6614

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 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565

This theorem depends on definitions: df-bi 116 df-dc 825 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-ral 2449 df-rex 2450 df-v 2728 df-sbc 2952 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-br 3983 df-opab 4044 df-id 4271 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-fv 5196 df-ov 5845 df-oprab 5846 df-mpo 5847 df-map 6616

This theorem is referenced by: bj-charfunbi 13693

W3C validator