ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7318

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 5625	. . . . . . . . 9 $\$ $\$
2	1	eqeq1d 2238	. . . . . . . 8 $\$ $\$
3	2	ralbidv 2530	. . . . . . 7 $\$ $\$
4	3	notbid 671	. . . . . 6 $\$ $\$
5	1	eqeq1d 2238	. . . . . . 7 $\$ $\$
6	5	rexbidv 2531	. . . . . 6 $\$ $\$
7	4, 6	imbi12d 234	. . . . 5 $\$ $\$ $\$
8		elex 2811	. . . . . . 7 Markov
9		ismkvmap 7317	. . . . . . . 8 Markov
10	9	biimpd 144	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 276	. . . . 5 Markov $/\$
13		elmapi 6815	. . . . . . . . . 10
14	13	adantl 277	. . . . . . . . 9 Markov $/\$
15	14	ffvelcdmda 5769	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6583	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5789	. . . . . 6 Markov $/\$ $\$
19		2onn 6665	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 109	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6807	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 167	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2912	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2229	. . . . . . . . . 10 $\$ $\$
26		fveq2 5626	. . . . . . . . . . 11
27	26	difeq2d 3322	. . . . . . . . . 10 $\$ $\$
28		simpr 110	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6568	. . . . . . . . . . 11
30		difexg 4224	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5727	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2238	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3316	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3562	. . . . . . . . . . . 12 $\$
36	34, 35	eqtrdi 2278	. . . . . . . . . . 11 $\$
37	36	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6576	. . . . . . . . . . . . 13
39	38	nesymi 2446	. . . . . . . . . . . 12
40		eqeq1 2236	. . . . . . . . . . . 12
41	39, 40	mtbiri 679	. . . . . . . . . . 11
42	41	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
43	37, 42	2thd 175	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
44		difid 3560	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2237	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 675	. . . . . . . . . . . 12 $\$
47		difeq2 3316	. . . . . . . . . . . . 13 $\$ $\$
48	47	eqeq1d 2238	. . . . . . . . . . . 12 $\$ $\$
49	46, 48	mtbiri 679	. . . . . . . . . . 11 $\$
50	49	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
51		notnot 632	. . . . . . . . . . 11
52	51	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
53	50, 52	2falsed 707	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
54	14	ffvelcdmda 5769	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6574	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2322	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3689	. . . . . . . . . 10 $\/$
58	56, 57	syl 14	. . . . . . . . 9 Markov $/\$ $/\$ $\/$
59	43, 53, 58	mpjaodan 803	. . . . . . . 8 Markov $/\$ $/\$ $\$
60	33, 59	bitrd 188	. . . . . . 7 Markov $/\$ $/\$ $\$
61	60	ralbidva 2526	. . . . . 6 Markov $/\$ $\$
62	61	notbid 671	. . . . 5 Markov $/\$ $\$
63		ralnex 2518	. . . . . 6
64	63	notbii 672	. . . . 5
65	62, 64	bitrdi 196	. . . 4 Markov $/\$ $\$
66	32	eqeq1d 2238	. . . . . 6 Markov $/\$ $/\$ $\$ $\$
67	35	eqeq1i 2237	. . . . . . . . . . 11 $\$
68	38, 67	nemtbir 2489	. . . . . . . . . 10 $\$
69	34	eqeq1d 2238	. . . . . . . . . 10 $\$ $\$
70	68, 69	mtbiri 679	. . . . . . . . 9 $\$
71	70	adantl 277	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
72	71, 42	2falsed 707	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
73	47, 44	eqtrdi 2278	. . . . . . . . 9 $\$
74	73	adantl 277	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
75		simpr 110	. . . . . . . 8 Markov $/\$ $/\$ $/\$
76	74, 75	2thd 175	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
77	72, 76, 58	mpjaodan 803	. . . . . 6 Markov $/\$ $/\$ $\$
78	66, 77	bitrd 188	. . . . 5 Markov $/\$ $/\$ $\$
79	78	rexbidva 2527	. . . 4 Markov $/\$ $\$
80	24, 65, 79	3imtr3d 202	. . 3 Markov $/\$
81	80	ralrimiva 2603	. 2 Markov
82		elex 2811	. . . . 5
83	82	adantr 276	. . . 4 $/\$
84		fveq1 5625	. . . . . . . . . . . 12 $\$ $\$
85	84	eqeq1d 2238	. . . . . . . . . . 11 $\$ $\$
86	85	rexbidv 2531	. . . . . . . . . 10 $\$ $\$
87	86	notbid 671	. . . . . . . . 9 $\$ $\$
88	87	notbid 671	. . . . . . . 8 $\$ $\$
89	88, 86	imbi12d 234	. . . . . . 7 $\$ $\$ $\$
90		simplr 528	. . . . . . 7 $/\$ $/\$
91		elmapi 6815	. . . . . . . . . . . 12
92	91	adantl 277	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelcdmda 5769	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6583	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5789	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 527	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6807	. . . . . . . 8 $/\$ $/\$ $\$ $\$
100	96, 99	mpbird 167	. . . . . . 7 $/\$ $/\$ $\$
101	89, 90, 100	rspcdva 2912	. . . . . 6 $/\$ $/\$ $\$ $\$
102		ralnex 2518	. . . . . . . 8 $\$ $\$
103	102	notbii 672	. . . . . . 7 $\$ $\$
104		nfv 1574	. . . . . . . . . . 11
105		nfcv 2372	. . . . . . . . . . . 12
106		nfre1 2573	. . . . . . . . . . . . . . 15
107	106	nfn 1704	. . . . . . . . . . . . . 14
108	107	nfn 1704	. . . . . . . . . . . . 13
109	108, 106	nfim 1618	. . . . . . . . . . . 12
110	105, 109	nfralxy 2568	. . . . . . . . . . 11
111	104, 110	nfan 1611	. . . . . . . . . 10 $/\$
112		nfv 1574	. . . . . . . . . 10
113	111, 112	nfan 1611	. . . . . . . . 9 $/\$ $/\$
114		eqid 2229	. . . . . . . . . . . . 13 $\$ $\$
115		fveq2 5626	. . . . . . . . . . . . . 14
116	115	difeq2d 3322	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4224	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5727	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2238	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 671	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3316	. . . . . . . . . . . . . . 15 $\$ $\$
124	123, 35	eqtrdi 2278	. . . . . . . . . . . . . 14 $\$
125	124	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
126	125	notnotd 633	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
127		eqeq1 2236	. . . . . . . . . . . . . 14
128	39, 127	mtbiri 679	. . . . . . . . . . . . 13
129	128	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
130	126, 129	2falsed 707	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
131		difeq2 3316	. . . . . . . . . . . . . . 15 $\$ $\$
132	131	eqeq1d 2238	. . . . . . . . . . . . . 14 $\$ $\$
133	46, 132	mtbiri 679	. . . . . . . . . . . . 13 $\$
134	133	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
135		simpr 110	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
136	134, 135	2thd 175	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
137	91	ad2antlr 489	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
138	137, 117	ffvelcdmd 5770	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2322	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3689	. . . . . . . . . . . 12 $\/$
141	139, 140	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
142	130, 136, 141	mpjaodan 803	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$
143	122, 142	bitrd 188	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
144	113, 143	ralbida 2524	. . . . . . . 8 $/\$ $/\$ $\$
145	144	notbid 671	. . . . . . 7 $/\$ $/\$ $\$
146	103, 145	bitr3id 194	. . . . . 6 $/\$ $/\$ $\$
147		simpr 110	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
148	125, 147	2thd 175	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
149	128, 135	nsyl3 629	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
150	134, 149	2falsed 707	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
151	148, 150, 141	mpjaodan 803	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
152	121, 151	bitrd 188	. . . . . . 7 $/\$ $/\$ $/\$ $\$
153	113, 152	rexbida 2525	. . . . . 6 $/\$ $/\$ $\$
154	101, 146, 153	3imtr3d 202	. . . . 5 $/\$ $/\$
155	154	ralrimiva 2603	. . . 4 $/\$
156	9	biimprd 158	. . . 4 Markov
157	83, 155, 156	sylc 62	. . 3 $/\$ Markov
158	157	ex 115	. 2 Markov
159	81, 158	impbid2 143	1 Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 713

wceq 1395

wcel 2200

wral 2508

wrex 2509

cvv 2799 $\$ cdif 3194

c0 3491

cpr 3667

cmpt 4144

com 4681

wf 5313

cfv 5317 (class class class)co 6000

c1o 6553

c2o 6554

cmap 6793 Markovcmarkov 7314

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4523 ax-setind 4628

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-ral 2513 df-rex 2514 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4383 df-iord 4456 df-on 4458 df-suc 4461 df-iom 4682 df-xp 4724 df-rel 4725 df-cnv 4726 df-co 4727 df-dm 4728 df-rn 4729 df-res 4730 df-ima 4731 df-iota 5277 df-fun 5319 df-fn 5320 df-f 5321 df-fv 5325 df-ov 6003 df-oprab 6004 df-mpo 6005 df-1o 6560 df-2o 6561 df-map 6795 df-markov 7315

This theorem is referenced by: subctctexmid 16325

W3C validator