ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7230

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 5560	. . . . . . . . 9 $\$ $\$
2	1	eqeq1d 2205	. . . . . . . 8 $\$ $\$
3	2	ralbidv 2497	. . . . . . 7 $\$ $\$
4	3	notbid 668	. . . . . 6 $\$ $\$
5	1	eqeq1d 2205	. . . . . . 7 $\$ $\$
6	5	rexbidv 2498	. . . . . 6 $\$ $\$
7	4, 6	imbi12d 234	. . . . 5 $\$ $\$ $\$
8		elex 2774	. . . . . . 7 Markov
9		ismkvmap 7229	. . . . . . . 8 Markov
10	9	biimpd 144	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 276	. . . . 5 Markov $/\$
13		elmapi 6738	. . . . . . . . . 10
14	13	adantl 277	. . . . . . . . 9 Markov $/\$
15	14	ffvelcdmda 5700	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6506	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5720	. . . . . 6 Markov $/\$ $\$
19		2onn 6588	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 109	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6730	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 167	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2873	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2196	. . . . . . . . . 10 $\$ $\$
26		fveq2 5561	. . . . . . . . . . 11
27	26	difeq2d 3282	. . . . . . . . . 10 $\$ $\$
28		simpr 110	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6491	. . . . . . . . . . 11
30		difexg 4175	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5658	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2205	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3276	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3522	. . . . . . . . . . . 12 $\$
36	34, 35	eqtrdi 2245	. . . . . . . . . . 11 $\$
37	36	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6499	. . . . . . . . . . . . 13
39	38	nesymi 2413	. . . . . . . . . . . 12
40		eqeq1 2203	. . . . . . . . . . . 12
41	39, 40	mtbiri 676	. . . . . . . . . . 11
42	41	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
43	37, 42	2thd 175	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
44		difid 3520	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2204	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 672	. . . . . . . . . . . 12 $\$
47		difeq2 3276	. . . . . . . . . . . . 13 $\$ $\$
48	47	eqeq1d 2205	. . . . . . . . . . . 12 $\$ $\$
49	46, 48	mtbiri 676	. . . . . . . . . . 11 $\$
50	49	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
51		notnot 630	. . . . . . . . . . 11
52	51	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
53	50, 52	2falsed 703	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
54	14	ffvelcdmda 5700	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6497	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2289	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3646	. . . . . . . . . 10 $\/$
58	56, 57	syl 14	. . . . . . . . 9 Markov $/\$ $/\$ $\/$
59	43, 53, 58	mpjaodan 799	. . . . . . . 8 Markov $/\$ $/\$ $\$
60	33, 59	bitrd 188	. . . . . . 7 Markov $/\$ $/\$ $\$
61	60	ralbidva 2493	. . . . . 6 Markov $/\$ $\$
62	61	notbid 668	. . . . 5 Markov $/\$ $\$
63		ralnex 2485	. . . . . 6
64	63	notbii 669	. . . . 5
65	62, 64	bitrdi 196	. . . 4 Markov $/\$ $\$
66	32	eqeq1d 2205	. . . . . 6 Markov $/\$ $/\$ $\$ $\$
67	35	eqeq1i 2204	. . . . . . . . . . 11 $\$
68	38, 67	nemtbir 2456	. . . . . . . . . 10 $\$
69	34	eqeq1d 2205	. . . . . . . . . 10 $\$ $\$
70	68, 69	mtbiri 676	. . . . . . . . 9 $\$
71	70	adantl 277	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
72	71, 42	2falsed 703	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
73	47, 44	eqtrdi 2245	. . . . . . . . 9 $\$
74	73	adantl 277	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
75		simpr 110	. . . . . . . 8 Markov $/\$ $/\$ $/\$
76	74, 75	2thd 175	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
77	72, 76, 58	mpjaodan 799	. . . . . 6 Markov $/\$ $/\$ $\$
78	66, 77	bitrd 188	. . . . 5 Markov $/\$ $/\$ $\$
79	78	rexbidva 2494	. . . 4 Markov $/\$ $\$
80	24, 65, 79	3imtr3d 202	. . 3 Markov $/\$
81	80	ralrimiva 2570	. 2 Markov
82		elex 2774	. . . . 5
83	82	adantr 276	. . . 4 $/\$
84		fveq1 5560	. . . . . . . . . . . 12 $\$ $\$
85	84	eqeq1d 2205	. . . . . . . . . . 11 $\$ $\$
86	85	rexbidv 2498	. . . . . . . . . 10 $\$ $\$
87	86	notbid 668	. . . . . . . . 9 $\$ $\$
88	87	notbid 668	. . . . . . . 8 $\$ $\$
89	88, 86	imbi12d 234	. . . . . . 7 $\$ $\$ $\$
90		simplr 528	. . . . . . 7 $/\$ $/\$
91		elmapi 6738	. . . . . . . . . . . 12
92	91	adantl 277	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelcdmda 5700	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6506	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5720	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 527	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6730	. . . . . . . 8 $/\$ $/\$ $\$ $\$
100	96, 99	mpbird 167	. . . . . . 7 $/\$ $/\$ $\$
101	89, 90, 100	rspcdva 2873	. . . . . 6 $/\$ $/\$ $\$ $\$
102		ralnex 2485	. . . . . . . 8 $\$ $\$
103	102	notbii 669	. . . . . . 7 $\$ $\$
104		nfv 1542	. . . . . . . . . . 11
105		nfcv 2339	. . . . . . . . . . . 12
106		nfre1 2540	. . . . . . . . . . . . . . 15
107	106	nfn 1672	. . . . . . . . . . . . . 14
108	107	nfn 1672	. . . . . . . . . . . . 13
109	108, 106	nfim 1586	. . . . . . . . . . . 12
110	105, 109	nfralxy 2535	. . . . . . . . . . 11
111	104, 110	nfan 1579	. . . . . . . . . 10 $/\$
112		nfv 1542	. . . . . . . . . 10
113	111, 112	nfan 1579	. . . . . . . . 9 $/\$ $/\$
114		eqid 2196	. . . . . . . . . . . . 13 $\$ $\$
115		fveq2 5561	. . . . . . . . . . . . . 14
116	115	difeq2d 3282	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4175	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5658	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2205	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 668	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3276	. . . . . . . . . . . . . . 15 $\$ $\$
124	123, 35	eqtrdi 2245	. . . . . . . . . . . . . 14 $\$
125	124	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
126	125	notnotd 631	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
127		eqeq1 2203	. . . . . . . . . . . . . 14
128	39, 127	mtbiri 676	. . . . . . . . . . . . 13
129	128	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
130	126, 129	2falsed 703	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
131		difeq2 3276	. . . . . . . . . . . . . . 15 $\$ $\$
132	131	eqeq1d 2205	. . . . . . . . . . . . . 14 $\$ $\$
133	46, 132	mtbiri 676	. . . . . . . . . . . . 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 5701	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2289	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3646	. . . . . . . . . . . 12 $\/$
141	139, 140	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
142	130, 136, 141	mpjaodan 799	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$
143	122, 142	bitrd 188	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
144	113, 143	ralbida 2491	. . . . . . . 8 $/\$ $/\$ $\$
145	144	notbid 668	. . . . . . 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 703	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
151	148, 150, 141	mpjaodan 799	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
152	121, 151	bitrd 188	. . . . . . 7 $/\$ $/\$ $/\$ $\$
153	113, 152	rexbida 2492	. . . . . 6 $/\$ $/\$ $\$
154	101, 146, 153	3imtr3d 202	. . . . 5 $/\$ $/\$
155	154	ralrimiva 2570	. . . 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 709

wceq 1364

wcel 2167

wral 2475

wrex 2476

cvv 2763 $\$ cdif 3154

c0 3451

cpr 3624

cmpt 4095

com 4627

wf 5255

cfv 5259 (class class class)co 5925

c1o 6476

c2o 6477

cmap 6716 Markovcmarkov 7226

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-ral 2480 df-rex 2481 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-iord 4402 df-on 4404 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-fv 5267 df-ov 5928 df-oprab 5929 df-mpo 5930 df-1o 6483 df-2o 6484 df-map 6718 df-markov 7227

This theorem is referenced by: subctctexmid 15731

W3C validator