ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7221

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 5557	. . . . . . . . 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 7220	. . . . . . . 8 Markov
10	9	biimpd 144	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 276	. . . . 5 Markov $/\$
13		elmapi 6729	. . . . . . . . . 10
14	13	adantl 277	. . . . . . . . 9 Markov $/\$
15	14	ffvelcdmda 5697	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6497	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5717	. . . . . 6 Markov $/\$ $\$
19		2onn 6579	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 109	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6721	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 167	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2873	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2196	. . . . . . . . . 10 $\$ $\$
26		fveq2 5558	. . . . . . . . . . 11
27	26	difeq2d 3281	. . . . . . . . . 10 $\$ $\$
28		simpr 110	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6482	. . . . . . . . . . 11
30		difexg 4174	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5655	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2205	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3275	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3521	. . . . . . . . . . . 12 $\$
36	34, 35	eqtrdi 2245	. . . . . . . . . . 11 $\$
37	36	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6490	. . . . . . . . . . . . 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 3519	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2204	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 672	. . . . . . . . . . . 12 $\$
47		difeq2 3275	. . . . . . . . . . . . 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 5697	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6488	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2289	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3645	. . . . . . . . . 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 5557	. . . . . . . . . . . 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 6729	. . . . . . . . . . . 12
92	91	adantl 277	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelcdmda 5697	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6497	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5717	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 527	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6721	. . . . . . . 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 5558	. . . . . . . . . . . . . 14
116	115	difeq2d 3281	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4174	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5655	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2205	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 668	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3275	. . . . . . . . . . . . . . 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 3275	. . . . . . . . . . . . . . 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 5698	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2289	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3645	. . . . . . . . . . . 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 3450

cpr 3623

cmpt 4094

com 4626

wf 5254

cfv 5258 (class class class)co 5922

c1o 6467

c2o 6468

cmap 6707 Markovcmarkov 7217

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 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573

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 3451 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-iord 4401 df-on 4403 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-fv 5266 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1o 6474 df-2o 6475 df-map 6709 df-markov 7218

This theorem is referenced by: subctctexmid 15645

W3C validator