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 15302

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 6724	. . . . . . . . . 10
3		ffvelcdm 5691	. . . . . . . . . . 11 $/\$
4	3	ex 115	. . . . . . . . . 10
5	2, 4	syl 14	. . . . . . . . 9
6		0elnn 4651	. . . . . . . . . 10 $\/$
7		nn0eln0 4652	. . . . . . . . . . 11
8	7	orbi2d 791	. . . . . . . . . 10 $\/$ $\/$
9	6, 8	mpbid 147	. . . . . . . . 9 $\/$
10	5, 9	syl6 33	. . . . . . . 8 $\/$
11	10	adantr 276	. . . . . . 7 $/\$ $/\$ $\$ $\/$
12		elin 3342	. . . . . . . . . . . . . . 15 $/\$
13		rsp 2541	. . . . . . . . . . . . . . 15
14	12, 13	biimtrrid 153	. . . . . . . . . . . . . 14 $/\$
15	14	expd 258	. . . . . . . . . . . . 13
16	15	adantr 276	. . . . . . . . . . . 12 $/\$ $\$
17	16	imp 124	. . . . . . . . . . 11 $/\$ $\$ $/\$
18	17	necon2bd 2422	. . . . . . . . . 10 $/\$ $\$ $/\$
19		eldif 3162	. . . . . . . . . . . . . . 15 $\$ $/\$
20		rsp 2541	. . . . . . . . . . . . . . 15 $\$ $\$
21	19, 20	biimtrrid 153	. . . . . . . . . . . . . 14 $\$ $/\$
22	21	expd 258	. . . . . . . . . . . . 13 $\$
23	22	adantl 277	. . . . . . . . . . . 12 $/\$ $\$
24	23	imp 124	. . . . . . . . . . 11 $/\$ $\$ $/\$
25	24	necon3ad 2406	. . . . . . . . . 10 $/\$ $\$ $/\$
26	18, 25	orim12d 787	. . . . . . . . 9 $/\$ $\$ $/\$ $\/$ $\/$
27	26	ex 115	. . . . . . . 8 $/\$ $\$ $\/$ $\/$
28	27	adantl 277	. . . . . . 7 $/\$ $/\$ $\$ $\/$ $\/$
29	11, 28	mpdd 41	. . . . . 6 $/\$ $/\$ $\$ $\/$
30	29	adantl 277	. . . . 5 $/\$ $/\$ $/\$ $\$ $\/$
31	1, 30	rexlimddv 2616	. . . 4 $\/$
32	31	imp 124	. . 3 $/\$ $\/$
33		df-dc 836	. . 3 DECID $\/$
34	32, 33	sylibr 134	. 2 $/\$ DECID
35	34	ralrimiva 2567	1 DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 709 DECID wdc 835

wceq 1364

wcel 2164

wne 2364

wral 2472

wrex 2473 $\$ cdif 3150

cin 3152

c0 3446

com 4622

wf 5250

cfv 5254 (class class class)co 5918

cmap 6702

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620

This theorem depends on definitions: df-bi 117 df-dc 836 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-ral 2477 df-rex 2478 df-v 2762 df-sbc 2986 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-br 4030 df-opab 4091 df-id 4324 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-fv 5262 df-ov 5921 df-oprab 5922 df-mpo 5923 df-map 6704

This theorem is referenced by: bj-charfunbi 15303

W3C validator