ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7147

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 5510	. . . . . . . . 9 $\$ $\$
2	1	eqeq1d 2186	. . . . . . . 8 $\$ $\$
3	2	ralbidv 2477	. . . . . . 7 $\$ $\$
4	3	notbid 667	. . . . . 6 $\$ $\$
5	1	eqeq1d 2186	. . . . . . 7 $\$ $\$
6	5	rexbidv 2478	. . . . . 6 $\$ $\$
7	4, 6	imbi12d 234	. . . . 5 $\$ $\$ $\$
8		elex 2748	. . . . . . 7 Markov
9		ismkvmap 7146	. . . . . . . 8 Markov
10	9	biimpd 144	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 276	. . . . 5 Markov $/\$
13		elmapi 6664	. . . . . . . . . 10
14	13	adantl 277	. . . . . . . . 9 Markov $/\$
15	14	ffvelcdmda 5647	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6434	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5667	. . . . . 6 Markov $/\$ $\$
19		2onn 6516	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 109	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6656	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 167	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2846	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2177	. . . . . . . . . 10 $\$ $\$
26		fveq2 5511	. . . . . . . . . . 11
27	26	difeq2d 3253	. . . . . . . . . 10 $\$ $\$
28		simpr 110	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6419	. . . . . . . . . . 11
30		difexg 4141	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5605	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2186	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3247	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3493	. . . . . . . . . . . 12 $\$
36	34, 35	eqtrdi 2226	. . . . . . . . . . 11 $\$
37	36	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6427	. . . . . . . . . . . . 13
39	38	nesymi 2393	. . . . . . . . . . . 12
40		eqeq1 2184	. . . . . . . . . . . 12
41	39, 40	mtbiri 675	. . . . . . . . . . 11
42	41	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
43	37, 42	2thd 175	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
44		difid 3491	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2185	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 671	. . . . . . . . . . . 12 $\$
47		difeq2 3247	. . . . . . . . . . . . 13 $\$ $\$
48	47	eqeq1d 2186	. . . . . . . . . . . 12 $\$ $\$
49	46, 48	mtbiri 675	. . . . . . . . . . 11 $\$
50	49	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
51		notnot 629	. . . . . . . . . . 11
52	51	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
53	50, 52	2falsed 702	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
54	14	ffvelcdmda 5647	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6425	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2270	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3614	. . . . . . . . . 10 $\/$
58	56, 57	syl 14	. . . . . . . . 9 Markov $/\$ $/\$ $\/$
59	43, 53, 58	mpjaodan 798	. . . . . . . 8 Markov $/\$ $/\$ $\$
60	33, 59	bitrd 188	. . . . . . 7 Markov $/\$ $/\$ $\$
61	60	ralbidva 2473	. . . . . 6 Markov $/\$ $\$
62	61	notbid 667	. . . . 5 Markov $/\$ $\$
63		ralnex 2465	. . . . . 6
64	63	notbii 668	. . . . 5
65	62, 64	bitrdi 196	. . . 4 Markov $/\$ $\$
66	32	eqeq1d 2186	. . . . . 6 Markov $/\$ $/\$ $\$ $\$
67	35	eqeq1i 2185	. . . . . . . . . . 11 $\$
68	38, 67	nemtbir 2436	. . . . . . . . . 10 $\$
69	34	eqeq1d 2186	. . . . . . . . . 10 $\$ $\$
70	68, 69	mtbiri 675	. . . . . . . . 9 $\$
71	70	adantl 277	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
72	71, 42	2falsed 702	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
73	47, 44	eqtrdi 2226	. . . . . . . . 9 $\$
74	73	adantl 277	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
75		simpr 110	. . . . . . . 8 Markov $/\$ $/\$ $/\$
76	74, 75	2thd 175	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
77	72, 76, 58	mpjaodan 798	. . . . . 6 Markov $/\$ $/\$ $\$
78	66, 77	bitrd 188	. . . . 5 Markov $/\$ $/\$ $\$
79	78	rexbidva 2474	. . . 4 Markov $/\$ $\$
80	24, 65, 79	3imtr3d 202	. . 3 Markov $/\$
81	80	ralrimiva 2550	. 2 Markov
82		elex 2748	. . . . 5
83	82	adantr 276	. . . 4 $/\$
84		fveq1 5510	. . . . . . . . . . . 12 $\$ $\$
85	84	eqeq1d 2186	. . . . . . . . . . 11 $\$ $\$
86	85	rexbidv 2478	. . . . . . . . . 10 $\$ $\$
87	86	notbid 667	. . . . . . . . 9 $\$ $\$
88	87	notbid 667	. . . . . . . 8 $\$ $\$
89	88, 86	imbi12d 234	. . . . . . 7 $\$ $\$ $\$
90		simplr 528	. . . . . . 7 $/\$ $/\$
91		elmapi 6664	. . . . . . . . . . . 12
92	91	adantl 277	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelcdmda 5647	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6434	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5667	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 527	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6656	. . . . . . . 8 $/\$ $/\$ $\$ $\$
100	96, 99	mpbird 167	. . . . . . 7 $/\$ $/\$ $\$
101	89, 90, 100	rspcdva 2846	. . . . . 6 $/\$ $/\$ $\$ $\$
102		ralnex 2465	. . . . . . . 8 $\$ $\$
103	102	notbii 668	. . . . . . 7 $\$ $\$
104		nfv 1528	. . . . . . . . . . 11
105		nfcv 2319	. . . . . . . . . . . 12
106		nfre1 2520	. . . . . . . . . . . . . . 15
107	106	nfn 1658	. . . . . . . . . . . . . 14
108	107	nfn 1658	. . . . . . . . . . . . 13
109	108, 106	nfim 1572	. . . . . . . . . . . 12
110	105, 109	nfralxy 2515	. . . . . . . . . . 11
111	104, 110	nfan 1565	. . . . . . . . . 10 $/\$
112		nfv 1528	. . . . . . . . . 10
113	111, 112	nfan 1565	. . . . . . . . 9 $/\$ $/\$
114		eqid 2177	. . . . . . . . . . . . 13 $\$ $\$
115		fveq2 5511	. . . . . . . . . . . . . 14
116	115	difeq2d 3253	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4141	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5605	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2186	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 667	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3247	. . . . . . . . . . . . . . 15 $\$ $\$
124	123, 35	eqtrdi 2226	. . . . . . . . . . . . . 14 $\$
125	124	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
126	125	notnotd 630	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
127		eqeq1 2184	. . . . . . . . . . . . . 14
128	39, 127	mtbiri 675	. . . . . . . . . . . . 13
129	128	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
130	126, 129	2falsed 702	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
131		difeq2 3247	. . . . . . . . . . . . . . 15 $\$ $\$
132	131	eqeq1d 2186	. . . . . . . . . . . . . 14 $\$ $\$
133	46, 132	mtbiri 675	. . . . . . . . . . . . 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 5648	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2270	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3614	. . . . . . . . . . . 12 $\/$
141	139, 140	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
142	130, 136, 141	mpjaodan 798	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$
143	122, 142	bitrd 188	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
144	113, 143	ralbida 2471	. . . . . . . 8 $/\$ $/\$ $\$
145	144	notbid 667	. . . . . . 7 $/\$ $/\$ $\$
146	103, 145	bitr3id 194	. . . . . 6 $/\$ $/\$ $\$
147		simpr 110	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
148	125, 147	2thd 175	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
149	128, 135	nsyl3 626	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
150	134, 149	2falsed 702	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
151	148, 150, 141	mpjaodan 798	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
152	121, 151	bitrd 188	. . . . . . 7 $/\$ $/\$ $/\$ $\$
153	113, 152	rexbida 2472	. . . . . 6 $/\$ $/\$ $\$
154	101, 146, 153	3imtr3d 202	. . . . 5 $/\$ $/\$
155	154	ralrimiva 2550	. . . 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 708

wceq 1353

wcel 2148

wral 2455

wrex 2456

cvv 2737 $\$ cdif 3126

c0 3422

cpr 3592

cmpt 4061

com 4586

wf 5208

cfv 5212 (class class class)co 5869

c1o 6404

c2o 6405

cmap 6642 Markovcmarkov 7143

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533

This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4290 df-iord 4363 df-on 4365 df-suc 4368 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-fv 5220 df-ov 5872 df-oprab 5873 df-mpo 5874 df-1o 6411 df-2o 6412 df-map 6644 df-markov 7144

This theorem is referenced by: subctctexmid 14406

W3C validator