ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7214

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 5553	. . . . . . . . 9 $\$ $\$
2	1	eqeq1d 2202	. . . . . . . 8 $\$ $\$
3	2	ralbidv 2494	. . . . . . 7 $\$ $\$
4	3	notbid 668	. . . . . 6 $\$ $\$
5	1	eqeq1d 2202	. . . . . . 7 $\$ $\$
6	5	rexbidv 2495	. . . . . 6 $\$ $\$
7	4, 6	imbi12d 234	. . . . 5 $\$ $\$ $\$
8		elex 2771	. . . . . . 7 Markov
9		ismkvmap 7213	. . . . . . . 8 Markov
10	9	biimpd 144	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 276	. . . . 5 Markov $/\$
13		elmapi 6724	. . . . . . . . . 10
14	13	adantl 277	. . . . . . . . 9 Markov $/\$
15	14	ffvelcdmda 5693	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6492	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5713	. . . . . 6 Markov $/\$ $\$
19		2onn 6574	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 109	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6716	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 167	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2869	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2193	. . . . . . . . . 10 $\$ $\$
26		fveq2 5554	. . . . . . . . . . 11
27	26	difeq2d 3277	. . . . . . . . . 10 $\$ $\$
28		simpr 110	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6477	. . . . . . . . . . 11
30		difexg 4170	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5651	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2202	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3271	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3517	. . . . . . . . . . . 12 $\$
36	34, 35	eqtrdi 2242	. . . . . . . . . . 11 $\$
37	36	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6485	. . . . . . . . . . . . 13
39	38	nesymi 2410	. . . . . . . . . . . 12
40		eqeq1 2200	. . . . . . . . . . . 12
41	39, 40	mtbiri 676	. . . . . . . . . . 11
42	41	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
43	37, 42	2thd 175	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
44		difid 3515	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2201	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 672	. . . . . . . . . . . 12 $\$
47		difeq2 3271	. . . . . . . . . . . . 13 $\$ $\$
48	47	eqeq1d 2202	. . . . . . . . . . . 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 5693	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6483	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2286	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3641	. . . . . . . . . 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 2490	. . . . . 6 Markov $/\$ $\$
62	61	notbid 668	. . . . 5 Markov $/\$ $\$
63		ralnex 2482	. . . . . 6
64	63	notbii 669	. . . . 5
65	62, 64	bitrdi 196	. . . 4 Markov $/\$ $\$
66	32	eqeq1d 2202	. . . . . 6 Markov $/\$ $/\$ $\$ $\$
67	35	eqeq1i 2201	. . . . . . . . . . 11 $\$
68	38, 67	nemtbir 2453	. . . . . . . . . 10 $\$
69	34	eqeq1d 2202	. . . . . . . . . 10 $\$ $\$
70	68, 69	mtbiri 676	. . . . . . . . 9 $\$
71	70	adantl 277	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
72	71, 42	2falsed 703	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
73	47, 44	eqtrdi 2242	. . . . . . . . 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 2491	. . . 4 Markov $/\$ $\$
80	24, 65, 79	3imtr3d 202	. . 3 Markov $/\$
81	80	ralrimiva 2567	. 2 Markov
82		elex 2771	. . . . 5
83	82	adantr 276	. . . 4 $/\$
84		fveq1 5553	. . . . . . . . . . . 12 $\$ $\$
85	84	eqeq1d 2202	. . . . . . . . . . 11 $\$ $\$
86	85	rexbidv 2495	. . . . . . . . . 10 $\$ $\$
87	86	notbid 668	. . . . . . . . 9 $\$ $\$
88	87	notbid 668	. . . . . . . 8 $\$ $\$
89	88, 86	imbi12d 234	. . . . . . 7 $\$ $\$ $\$
90		simplr 528	. . . . . . 7 $/\$ $/\$
91		elmapi 6724	. . . . . . . . . . . 12
92	91	adantl 277	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelcdmda 5693	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6492	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5713	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 527	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6716	. . . . . . . 8 $/\$ $/\$ $\$ $\$
100	96, 99	mpbird 167	. . . . . . 7 $/\$ $/\$ $\$
101	89, 90, 100	rspcdva 2869	. . . . . 6 $/\$ $/\$ $\$ $\$
102		ralnex 2482	. . . . . . . 8 $\$ $\$
103	102	notbii 669	. . . . . . 7 $\$ $\$
104		nfv 1539	. . . . . . . . . . 11
105		nfcv 2336	. . . . . . . . . . . 12
106		nfre1 2537	. . . . . . . . . . . . . . 15
107	106	nfn 1669	. . . . . . . . . . . . . 14
108	107	nfn 1669	. . . . . . . . . . . . 13
109	108, 106	nfim 1583	. . . . . . . . . . . 12
110	105, 109	nfralxy 2532	. . . . . . . . . . 11
111	104, 110	nfan 1576	. . . . . . . . . 10 $/\$
112		nfv 1539	. . . . . . . . . 10
113	111, 112	nfan 1576	. . . . . . . . 9 $/\$ $/\$
114		eqid 2193	. . . . . . . . . . . . 13 $\$ $\$
115		fveq2 5554	. . . . . . . . . . . . . 14
116	115	difeq2d 3277	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4170	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5651	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2202	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 668	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3271	. . . . . . . . . . . . . . 15 $\$ $\$
124	123, 35	eqtrdi 2242	. . . . . . . . . . . . . 14 $\$
125	124	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
126	125	notnotd 631	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
127		eqeq1 2200	. . . . . . . . . . . . . 14
128	39, 127	mtbiri 676	. . . . . . . . . . . . 13
129	128	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
130	126, 129	2falsed 703	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
131		difeq2 3271	. . . . . . . . . . . . . . 15 $\$ $\$
132	131	eqeq1d 2202	. . . . . . . . . . . . . 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 5694	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2286	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3641	. . . . . . . . . . . 12 $\/$
141	139, 140	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
142	130, 136, 141	mpjaodan 799	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$
143	122, 142	bitrd 188	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
144	113, 143	ralbida 2488	. . . . . . . 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 2489	. . . . . 6 $/\$ $/\$ $\$
154	101, 146, 153	3imtr3d 202	. . . . 5 $/\$ $/\$
155	154	ralrimiva 2567	. . . 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 2164

wral 2472

wrex 2473

cvv 2760 $\$ cdif 3150

c0 3446

cpr 3619

cmpt 4090

com 4622

wf 5250

cfv 5254 (class class class)co 5918

c1o 6462

c2o 6463

cmap 6702 Markovcmarkov 7210

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-ral 2477 df-rex 2478 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-iord 4397 df-on 4399 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-fv 5262 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1o 6469 df-2o 6470 df-map 6704 df-markov 7211

This theorem is referenced by: subctctexmid 15491

W3C validator