ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7272

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 5588	. . . . . . . . 9 $\$ $\$
2	1	eqeq1d 2215	. . . . . . . 8 $\$ $\$
3	2	ralbidv 2507	. . . . . . 7 $\$ $\$
4	3	notbid 669	. . . . . 6 $\$ $\$
5	1	eqeq1d 2215	. . . . . . 7 $\$ $\$
6	5	rexbidv 2508	. . . . . 6 $\$ $\$
7	4, 6	imbi12d 234	. . . . 5 $\$ $\$ $\$
8		elex 2785	. . . . . . 7 Markov
9		ismkvmap 7271	. . . . . . . 8 Markov
10	9	biimpd 144	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 276	. . . . 5 Markov $/\$
13		elmapi 6770	. . . . . . . . . 10
14	13	adantl 277	. . . . . . . . 9 Markov $/\$
15	14	ffvelcdmda 5728	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6538	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5748	. . . . . 6 Markov $/\$ $\$
19		2onn 6620	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 109	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6762	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 167	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2886	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2206	. . . . . . . . . 10 $\$ $\$
26		fveq2 5589	. . . . . . . . . . 11
27	26	difeq2d 3295	. . . . . . . . . 10 $\$ $\$
28		simpr 110	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6523	. . . . . . . . . . 11
30		difexg 4193	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5686	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2215	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3289	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3535	. . . . . . . . . . . 12 $\$
36	34, 35	eqtrdi 2255	. . . . . . . . . . 11 $\$
37	36	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6531	. . . . . . . . . . . . 13
39	38	nesymi 2423	. . . . . . . . . . . 12
40		eqeq1 2213	. . . . . . . . . . . 12
41	39, 40	mtbiri 677	. . . . . . . . . . 11
42	41	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
43	37, 42	2thd 175	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
44		difid 3533	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2214	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 673	. . . . . . . . . . . 12 $\$
47		difeq2 3289	. . . . . . . . . . . . 13 $\$ $\$
48	47	eqeq1d 2215	. . . . . . . . . . . 12 $\$ $\$
49	46, 48	mtbiri 677	. . . . . . . . . . 11 $\$
50	49	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
51		notnot 630	. . . . . . . . . . 11
52	51	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
53	50, 52	2falsed 704	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
54	14	ffvelcdmda 5728	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6529	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2299	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3661	. . . . . . . . . 10 $\/$
58	56, 57	syl 14	. . . . . . . . 9 Markov $/\$ $/\$ $\/$
59	43, 53, 58	mpjaodan 800	. . . . . . . 8 Markov $/\$ $/\$ $\$
60	33, 59	bitrd 188	. . . . . . 7 Markov $/\$ $/\$ $\$
61	60	ralbidva 2503	. . . . . 6 Markov $/\$ $\$
62	61	notbid 669	. . . . 5 Markov $/\$ $\$
63		ralnex 2495	. . . . . 6
64	63	notbii 670	. . . . 5
65	62, 64	bitrdi 196	. . . 4 Markov $/\$ $\$
66	32	eqeq1d 2215	. . . . . 6 Markov $/\$ $/\$ $\$ $\$
67	35	eqeq1i 2214	. . . . . . . . . . 11 $\$
68	38, 67	nemtbir 2466	. . . . . . . . . 10 $\$
69	34	eqeq1d 2215	. . . . . . . . . 10 $\$ $\$
70	68, 69	mtbiri 677	. . . . . . . . 9 $\$
71	70	adantl 277	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
72	71, 42	2falsed 704	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
73	47, 44	eqtrdi 2255	. . . . . . . . 9 $\$
74	73	adantl 277	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
75		simpr 110	. . . . . . . 8 Markov $/\$ $/\$ $/\$
76	74, 75	2thd 175	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
77	72, 76, 58	mpjaodan 800	. . . . . 6 Markov $/\$ $/\$ $\$
78	66, 77	bitrd 188	. . . . 5 Markov $/\$ $/\$ $\$
79	78	rexbidva 2504	. . . 4 Markov $/\$ $\$
80	24, 65, 79	3imtr3d 202	. . 3 Markov $/\$
81	80	ralrimiva 2580	. 2 Markov
82		elex 2785	. . . . 5
83	82	adantr 276	. . . 4 $/\$
84		fveq1 5588	. . . . . . . . . . . 12 $\$ $\$
85	84	eqeq1d 2215	. . . . . . . . . . 11 $\$ $\$
86	85	rexbidv 2508	. . . . . . . . . 10 $\$ $\$
87	86	notbid 669	. . . . . . . . 9 $\$ $\$
88	87	notbid 669	. . . . . . . 8 $\$ $\$
89	88, 86	imbi12d 234	. . . . . . 7 $\$ $\$ $\$
90		simplr 528	. . . . . . 7 $/\$ $/\$
91		elmapi 6770	. . . . . . . . . . . 12
92	91	adantl 277	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelcdmda 5728	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6538	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5748	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 527	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6762	. . . . . . . 8 $/\$ $/\$ $\$ $\$
100	96, 99	mpbird 167	. . . . . . 7 $/\$ $/\$ $\$
101	89, 90, 100	rspcdva 2886	. . . . . 6 $/\$ $/\$ $\$ $\$
102		ralnex 2495	. . . . . . . 8 $\$ $\$
103	102	notbii 670	. . . . . . 7 $\$ $\$
104		nfv 1552	. . . . . . . . . . 11
105		nfcv 2349	. . . . . . . . . . . 12
106		nfre1 2550	. . . . . . . . . . . . . . 15
107	106	nfn 1682	. . . . . . . . . . . . . 14
108	107	nfn 1682	. . . . . . . . . . . . 13
109	108, 106	nfim 1596	. . . . . . . . . . . 12
110	105, 109	nfralxy 2545	. . . . . . . . . . 11
111	104, 110	nfan 1589	. . . . . . . . . 10 $/\$
112		nfv 1552	. . . . . . . . . 10
113	111, 112	nfan 1589	. . . . . . . . 9 $/\$ $/\$
114		eqid 2206	. . . . . . . . . . . . 13 $\$ $\$
115		fveq2 5589	. . . . . . . . . . . . . 14
116	115	difeq2d 3295	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4193	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5686	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2215	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 669	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3289	. . . . . . . . . . . . . . 15 $\$ $\$
124	123, 35	eqtrdi 2255	. . . . . . . . . . . . . 14 $\$
125	124	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
126	125	notnotd 631	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
127		eqeq1 2213	. . . . . . . . . . . . . 14
128	39, 127	mtbiri 677	. . . . . . . . . . . . 13
129	128	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
130	126, 129	2falsed 704	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
131		difeq2 3289	. . . . . . . . . . . . . . 15 $\$ $\$
132	131	eqeq1d 2215	. . . . . . . . . . . . . 14 $\$ $\$
133	46, 132	mtbiri 677	. . . . . . . . . . . . 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 5729	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2299	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3661	. . . . . . . . . . . 12 $\/$
141	139, 140	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
142	130, 136, 141	mpjaodan 800	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$
143	122, 142	bitrd 188	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
144	113, 143	ralbida 2501	. . . . . . . 8 $/\$ $/\$ $\$
145	144	notbid 669	. . . . . . 7 $/\$ $/\$ $\$
146	103, 145	bitr3id 194	. . . . . 6 $/\$ $/\$ $\$
147		simpr 110	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
148	125, 147	2thd 175	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
149	128, 135	nsyl3 627	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
150	134, 149	2falsed 704	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
151	148, 150, 141	mpjaodan 800	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
152	121, 151	bitrd 188	. . . . . . 7 $/\$ $/\$ $/\$ $\$
153	113, 152	rexbida 2502	. . . . . 6 $/\$ $/\$ $\$
154	101, 146, 153	3imtr3d 202	. . . . 5 $/\$ $/\$
155	154	ralrimiva 2580	. . . 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 710

wceq 1373

wcel 2177

wral 2485

wrex 2486

cvv 2773 $\$ cdif 3167

c0 3464

cpr 3639

cmpt 4113

com 4646

wf 5276

cfv 5280 (class class class)co 5957

c1o 6508

c2o 6509

cmap 6748 Markovcmarkov 7268

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4170 ax-nul 4178 ax-pow 4226 ax-pr 4261 ax-un 4488 ax-setind 4593

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-ral 2490 df-rex 2491 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3857 df-int 3892 df-br 4052 df-opab 4114 df-mpt 4115 df-tr 4151 df-id 4348 df-iord 4421 df-on 4423 df-suc 4426 df-iom 4647 df-xp 4689 df-rel 4690 df-cnv 4691 df-co 4692 df-dm 4693 df-rn 4694 df-res 4695 df-ima 4696 df-iota 5241 df-fun 5282 df-fn 5283 df-f 5284 df-fv 5288 df-ov 5960 df-oprab 5961 df-mpo 5962 df-1o 6515 df-2o 6516 df-map 6750 df-markov 7269

This theorem is referenced by: subctctexmid 16078

W3C validator