ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7283

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 5598	. . . . . . . . 9 $\$ $\$
2	1	eqeq1d 2216	. . . . . . . 8 $\$ $\$
3	2	ralbidv 2508	. . . . . . 7 $\$ $\$
4	3	notbid 669	. . . . . 6 $\$ $\$
5	1	eqeq1d 2216	. . . . . . 7 $\$ $\$
6	5	rexbidv 2509	. . . . . 6 $\$ $\$
7	4, 6	imbi12d 234	. . . . 5 $\$ $\$ $\$
8		elex 2788	. . . . . . 7 Markov
9		ismkvmap 7282	. . . . . . . 8 Markov
10	9	biimpd 144	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 276	. . . . 5 Markov $/\$
13		elmapi 6780	. . . . . . . . . 10
14	13	adantl 277	. . . . . . . . 9 Markov $/\$
15	14	ffvelcdmda 5738	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6548	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5758	. . . . . 6 Markov $/\$ $\$
19		2onn 6630	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 109	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6772	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 167	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2889	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2207	. . . . . . . . . 10 $\$ $\$
26		fveq2 5599	. . . . . . . . . . 11
27	26	difeq2d 3299	. . . . . . . . . 10 $\$ $\$
28		simpr 110	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6533	. . . . . . . . . . 11
30		difexg 4201	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5696	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2216	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3293	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3539	. . . . . . . . . . . 12 $\$
36	34, 35	eqtrdi 2256	. . . . . . . . . . 11 $\$
37	36	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6541	. . . . . . . . . . . . 13
39	38	nesymi 2424	. . . . . . . . . . . 12
40		eqeq1 2214	. . . . . . . . . . . 12
41	39, 40	mtbiri 677	. . . . . . . . . . 11
42	41	adantl 277	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
43	37, 42	2thd 175	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
44		difid 3537	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2215	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 673	. . . . . . . . . . . 12 $\$
47		difeq2 3293	. . . . . . . . . . . . 13 $\$ $\$
48	47	eqeq1d 2216	. . . . . . . . . . . 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 5738	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6539	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2300	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3666	. . . . . . . . . 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 2504	. . . . . 6 Markov $/\$ $\$
62	61	notbid 669	. . . . 5 Markov $/\$ $\$
63		ralnex 2496	. . . . . 6
64	63	notbii 670	. . . . 5
65	62, 64	bitrdi 196	. . . 4 Markov $/\$ $\$
66	32	eqeq1d 2216	. . . . . 6 Markov $/\$ $/\$ $\$ $\$
67	35	eqeq1i 2215	. . . . . . . . . . 11 $\$
68	38, 67	nemtbir 2467	. . . . . . . . . 10 $\$
69	34	eqeq1d 2216	. . . . . . . . . 10 $\$ $\$
70	68, 69	mtbiri 677	. . . . . . . . 9 $\$
71	70	adantl 277	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
72	71, 42	2falsed 704	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
73	47, 44	eqtrdi 2256	. . . . . . . . 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 2505	. . . 4 Markov $/\$ $\$
80	24, 65, 79	3imtr3d 202	. . 3 Markov $/\$
81	80	ralrimiva 2581	. 2 Markov
82		elex 2788	. . . . 5
83	82	adantr 276	. . . 4 $/\$
84		fveq1 5598	. . . . . . . . . . . 12 $\$ $\$
85	84	eqeq1d 2216	. . . . . . . . . . 11 $\$ $\$
86	85	rexbidv 2509	. . . . . . . . . 10 $\$ $\$
87	86	notbid 669	. . . . . . . . 9 $\$ $\$
88	87	notbid 669	. . . . . . . 8 $\$ $\$
89	88, 86	imbi12d 234	. . . . . . 7 $\$ $\$ $\$
90		simplr 528	. . . . . . 7 $/\$ $/\$
91		elmapi 6780	. . . . . . . . . . . 12
92	91	adantl 277	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelcdmda 5738	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6548	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5758	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 527	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6772	. . . . . . . 8 $/\$ $/\$ $\$ $\$
100	96, 99	mpbird 167	. . . . . . 7 $/\$ $/\$ $\$
101	89, 90, 100	rspcdva 2889	. . . . . 6 $/\$ $/\$ $\$ $\$
102		ralnex 2496	. . . . . . . 8 $\$ $\$
103	102	notbii 670	. . . . . . 7 $\$ $\$
104		nfv 1552	. . . . . . . . . . 11
105		nfcv 2350	. . . . . . . . . . . 12
106		nfre1 2551	. . . . . . . . . . . . . . 15
107	106	nfn 1682	. . . . . . . . . . . . . 14
108	107	nfn 1682	. . . . . . . . . . . . 13
109	108, 106	nfim 1596	. . . . . . . . . . . 12
110	105, 109	nfralxy 2546	. . . . . . . . . . 11
111	104, 110	nfan 1589	. . . . . . . . . 10 $/\$
112		nfv 1552	. . . . . . . . . 10
113	111, 112	nfan 1589	. . . . . . . . 9 $/\$ $/\$
114		eqid 2207	. . . . . . . . . . . . 13 $\$ $\$
115		fveq2 5599	. . . . . . . . . . . . . 14
116	115	difeq2d 3299	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4201	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5696	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2216	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 669	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3293	. . . . . . . . . . . . . . 15 $\$ $\$
124	123, 35	eqtrdi 2256	. . . . . . . . . . . . . 14 $\$
125	124	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
126	125	notnotd 631	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
127		eqeq1 2214	. . . . . . . . . . . . . 14
128	39, 127	mtbiri 677	. . . . . . . . . . . . 13
129	128	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
130	126, 129	2falsed 704	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
131		difeq2 3293	. . . . . . . . . . . . . . 15 $\$ $\$
132	131	eqeq1d 2216	. . . . . . . . . . . . . 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 5739	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2300	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3666	. . . . . . . . . . . 12 $\/$
141	139, 140	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
142	130, 136, 141	mpjaodan 800	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$
143	122, 142	bitrd 188	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
144	113, 143	ralbida 2502	. . . . . . . 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 2503	. . . . . 6 $/\$ $/\$ $\$
154	101, 146, 153	3imtr3d 202	. . . . 5 $/\$ $/\$
155	154	ralrimiva 2581	. . . 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 2178

wral 2486

wrex 2487

cvv 2776 $\$ cdif 3171

c0 3468

cpr 3644

cmpt 4121

com 4656

wf 5286

cfv 5290 (class class class)co 5967

c1o 6518

c2o 6519

cmap 6758 Markovcmarkov 7279

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 2180 ax-14 2181 ax-ext 2189 ax-sep 4178 ax-nul 4186 ax-pow 4234 ax-pr 4269 ax-un 4498 ax-setind 4603

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 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-ral 2491 df-rex 2492 df-rab 2495 df-v 2778 df-sbc 3006 df-csb 3102 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-nul 3469 df-pw 3628 df-sn 3649 df-pr 3650 df-op 3652 df-uni 3865 df-int 3900 df-br 4060 df-opab 4122 df-mpt 4123 df-tr 4159 df-id 4358 df-iord 4431 df-on 4433 df-suc 4436 df-iom 4657 df-xp 4699 df-rel 4700 df-cnv 4701 df-co 4702 df-dm 4703 df-rn 4704 df-res 4705 df-ima 4706 df-iota 5251 df-fun 5292 df-fn 5293 df-f 5294 df-fv 5298 df-ov 5970 df-oprab 5971 df-mpo 5972 df-1o 6525 df-2o 6526 df-map 6760 df-markov 7280

This theorem is referenced by: subctctexmid 16139

W3C validator