ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7029

Description: The predicate of being Markov stated in terms of double negation and comparison with

. (Contributed by Jim Kingdon, 29-Nov-2023.)

**Assertion**
Ref	Expression
ismkvnex	Markov

Distinct variable groups:

Proof of Theorem ismkvnex Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq1 5420	. . . . . . . . 9 $\$ $\$
2	1	eqeq1d 2148	. . . . . . . 8 $\$ $\$
3	2	ralbidv 2437	. . . . . . 7 $\$ $\$
4	3	notbid 656	. . . . . 6 $\$ $\$
5	1	eqeq1d 2148	. . . . . . 7 $\$ $\$
6	5	rexbidv 2438	. . . . . 6 $\$ $\$
7	4, 6	imbi12d 233	. . . . 5 $\$ $\$ $\$
8		elex 2697	. . . . . . 7 Markov
9		ismkvmap 7028	. . . . . . . 8 Markov
10	9	biimpd 143	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 274	. . . . 5 Markov $/\$
13		elmapi 6564	. . . . . . . . . 10
14	13	adantl 275	. . . . . . . . 9 Markov $/\$
15	14	ffvelrnda 5555	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6336	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5575	. . . . . 6 Markov $/\$ $\$
19		2onn 6417	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 108	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6556	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 166	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2794	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2139	. . . . . . . . . 10 $\$ $\$
26		fveq2 5421	. . . . . . . . . . 11
27	26	difeq2d 3194	. . . . . . . . . 10 $\$ $\$
28		simpr 109	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6321	. . . . . . . . . . 11
30		difexg 4069	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5514	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2148	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3188	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3433	. . . . . . . . . . . 12 $\$
36	34, 35	syl6eq 2188	. . . . . . . . . . 11 $\$
37	36	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6329	. . . . . . . . . . . . 13
39	38	nesymi 2354	. . . . . . . . . . . 12
40		eqeq1 2146	. . . . . . . . . . . 12
41	39, 40	mtbiri 664	. . . . . . . . . . 11
42	41	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
43	37, 42	2thd 174	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
44		difid 3431	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2147	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 660	. . . . . . . . . . . 12 $\$
47		difeq2 3188	. . . . . . . . . . . . 13 $\$ $\$
48	47	eqeq1d 2148	. . . . . . . . . . . 12 $\$ $\$
49	46, 48	mtbiri 664	. . . . . . . . . . 11 $\$
50	49	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
51		notnot 618	. . . . . . . . . . 11
52	51	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
53	50, 52	2falsed 691	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
54	14	ffvelrnda 5555	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6327	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2232	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3550	. . . . . . . . . 10 $\/$
58	56, 57	syl 14	. . . . . . . . 9 Markov $/\$ $/\$ $\/$
59	43, 53, 58	mpjaodan 787	. . . . . . . 8 Markov $/\$ $/\$ $\$
60	33, 59	bitrd 187	. . . . . . 7 Markov $/\$ $/\$ $\$
61	60	ralbidva 2433	. . . . . 6 Markov $/\$ $\$
62	61	notbid 656	. . . . 5 Markov $/\$ $\$
63		ralnex 2426	. . . . . 6
64	63	notbii 657	. . . . 5
65	62, 64	syl6bb 195	. . . 4 Markov $/\$ $\$
66	32	eqeq1d 2148	. . . . . 6 Markov $/\$ $/\$ $\$ $\$
67	35	eqeq1i 2147	. . . . . . . . . . 11 $\$
68	38, 67	nemtbir 2397	. . . . . . . . . 10 $\$
69	34	eqeq1d 2148	. . . . . . . . . 10 $\$ $\$
70	68, 69	mtbiri 664	. . . . . . . . 9 $\$
71	70	adantl 275	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
72	71, 42	2falsed 691	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
73	47, 44	syl6eq 2188	. . . . . . . . 9 $\$
74	73	adantl 275	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
75		simpr 109	. . . . . . . 8 Markov $/\$ $/\$ $/\$
76	74, 75	2thd 174	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
77	72, 76, 58	mpjaodan 787	. . . . . 6 Markov $/\$ $/\$ $\$
78	66, 77	bitrd 187	. . . . 5 Markov $/\$ $/\$ $\$
79	78	rexbidva 2434	. . . 4 Markov $/\$ $\$
80	24, 65, 79	3imtr3d 201	. . 3 Markov $/\$
81	80	ralrimiva 2505	. 2 Markov
82		elex 2697	. . . . 5
83	82	adantr 274	. . . 4 $/\$
84		fveq1 5420	. . . . . . . . . . . 12 $\$ $\$
85	84	eqeq1d 2148	. . . . . . . . . . 11 $\$ $\$
86	85	rexbidv 2438	. . . . . . . . . 10 $\$ $\$
87	86	notbid 656	. . . . . . . . 9 $\$ $\$
88	87	notbid 656	. . . . . . . 8 $\$ $\$
89	88, 86	imbi12d 233	. . . . . . 7 $\$ $\$ $\$
90		simplr 519	. . . . . . 7 $/\$ $/\$
91		elmapi 6564	. . . . . . . . . . . 12
92	91	adantl 275	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelrnda 5555	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6336	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5575	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 518	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6556	. . . . . . . 8 $/\$ $/\$ $\$ $\$
100	96, 99	mpbird 166	. . . . . . 7 $/\$ $/\$ $\$
101	89, 90, 100	rspcdva 2794	. . . . . 6 $/\$ $/\$ $\$ $\$
102		ralnex 2426	. . . . . . . 8 $\$ $\$
103	102	notbii 657	. . . . . . 7 $\$ $\$
104		nfv 1508	. . . . . . . . . . 11
105		nfcv 2281	. . . . . . . . . . . 12
106		nfre1 2476	. . . . . . . . . . . . . . 15
107	106	nfn 1636	. . . . . . . . . . . . . 14
108	107	nfn 1636	. . . . . . . . . . . . 13
109	108, 106	nfim 1551	. . . . . . . . . . . 12
110	105, 109	nfralxy 2471	. . . . . . . . . . 11
111	104, 110	nfan 1544	. . . . . . . . . 10 $/\$
112		nfv 1508	. . . . . . . . . 10
113	111, 112	nfan 1544	. . . . . . . . 9 $/\$ $/\$
114		eqid 2139	. . . . . . . . . . . . 13 $\$ $\$
115		fveq2 5421	. . . . . . . . . . . . . 14
116	115	difeq2d 3194	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 109	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4069	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5514	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2148	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 656	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3188	. . . . . . . . . . . . . . 15 $\$ $\$
124	123, 35	syl6eq 2188	. . . . . . . . . . . . . 14 $\$
125	124	adantl 275	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
126	125	notnotd 619	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
127		eqeq1 2146	. . . . . . . . . . . . . 14
128	39, 127	mtbiri 664	. . . . . . . . . . . . 13
129	128	adantl 275	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
130	126, 129	2falsed 691	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
131		difeq2 3188	. . . . . . . . . . . . . . 15 $\$ $\$
132	131	eqeq1d 2148	. . . . . . . . . . . . . 14 $\$ $\$
133	46, 132	mtbiri 664	. . . . . . . . . . . . 13 $\$
134	133	adantl 275	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
135		simpr 109	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
136	134, 135	2thd 174	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
137	91	ad2antlr 480	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
138	137, 117	ffvelrnd 5556	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3550	. . . . . . . . . . . 12 $\/$
141	139, 140	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
142	130, 136, 141	mpjaodan 787	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$
143	122, 142	bitrd 187	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
144	113, 143	ralbida 2431	. . . . . . . 8 $/\$ $/\$ $\$
145	144	notbid 656	. . . . . . 7 $/\$ $/\$ $\$
146	103, 145	syl5bbr 193	. . . . . 6 $/\$ $/\$ $\$
147		simpr 109	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
148	125, 147	2thd 174	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
149	128, 135	nsyl3 615	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
150	134, 149	2falsed 691	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
151	148, 150, 141	mpjaodan 787	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
152	121, 151	bitrd 187	. . . . . . 7 $/\$ $/\$ $/\$ $\$
153	113, 152	rexbida 2432	. . . . . 6 $/\$ $/\$ $\$
154	101, 146, 153	3imtr3d 201	. . . . 5 $/\$ $/\$
155	154	ralrimiva 2505	. . . 4 $/\$
156	9	biimprd 157	. . . 4 Markov
157	83, 155, 156	sylc 62	. . 3 $/\$ Markov
158	157	ex 114	. 2 Markov
159	81, 158	impbid2 142	1 Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 697

wceq 1331

wcel 1480

wral 2416

wrex 2417

cvv 2686 $\$ cdif 3068

c0 3363

cpr 3528

cmpt 3989

com 4504

wf 5119

cfv 5123 (class class class)co 5774

c1o 6306

c2o 6307

cmap 6542 Markovcmarkov 7025

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 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452

This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-ral 2421 df-rex 2422 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-nul 3364 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-int 3772 df-br 3930 df-opab 3990 df-mpt 3991 df-tr 4027 df-id 4215 df-iord 4288 df-on 4290 df-suc 4293 df-iom 4505 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-res 4551 df-ima 4552 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-fv 5131 df-ov 5777 df-oprab 5778 df-mpo 5779 df-1o 6313 df-2o 6314 df-map 6544 df-markov 7026

This theorem is referenced by: subctctexmid 13196

W3C validator