ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7037

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 5428	. . . . . . . . 9 $\$ $\$
2	1	eqeq1d 2149	. . . . . . . 8 $\$ $\$
3	2	ralbidv 2438	. . . . . . 7 $\$ $\$
4	3	notbid 657	. . . . . 6 $\$ $\$
5	1	eqeq1d 2149	. . . . . . 7 $\$ $\$
6	5	rexbidv 2439	. . . . . 6 $\$ $\$
7	4, 6	imbi12d 233	. . . . 5 $\$ $\$ $\$
8		elex 2700	. . . . . . 7 Markov
9		ismkvmap 7036	. . . . . . . 8 Markov
10	9	biimpd 143	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 274	. . . . 5 Markov $/\$
13		elmapi 6572	. . . . . . . . . 10
14	13	adantl 275	. . . . . . . . 9 Markov $/\$
15	14	ffvelrnda 5563	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6344	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5583	. . . . . 6 Markov $/\$ $\$
19		2onn 6425	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 108	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6564	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 166	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2798	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2140	. . . . . . . . . 10 $\$ $\$
26		fveq2 5429	. . . . . . . . . . 11
27	26	difeq2d 3199	. . . . . . . . . 10 $\$ $\$
28		simpr 109	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6329	. . . . . . . . . . 11
30		difexg 4077	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5522	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2149	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3193	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3438	. . . . . . . . . . . 12 $\$
36	34, 35	eqtrdi 2189	. . . . . . . . . . 11 $\$
37	36	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6337	. . . . . . . . . . . . 13
39	38	nesymi 2355	. . . . . . . . . . . 12
40		eqeq1 2147	. . . . . . . . . . . 12
41	39, 40	mtbiri 665	. . . . . . . . . . 11
42	41	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
43	37, 42	2thd 174	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
44		difid 3436	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2148	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 661	. . . . . . . . . . . 12 $\$
47		difeq2 3193	. . . . . . . . . . . . 13 $\$ $\$
48	47	eqeq1d 2149	. . . . . . . . . . . 12 $\$ $\$
49	46, 48	mtbiri 665	. . . . . . . . . . 11 $\$
50	49	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
51		notnot 619	. . . . . . . . . . 11
52	51	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
53	50, 52	2falsed 692	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
54	14	ffvelrnda 5563	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6335	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2233	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3555	. . . . . . . . . 10 $\/$
58	56, 57	syl 14	. . . . . . . . 9 Markov $/\$ $/\$ $\/$
59	43, 53, 58	mpjaodan 788	. . . . . . . 8 Markov $/\$ $/\$ $\$
60	33, 59	bitrd 187	. . . . . . 7 Markov $/\$ $/\$ $\$
61	60	ralbidva 2434	. . . . . 6 Markov $/\$ $\$
62	61	notbid 657	. . . . 5 Markov $/\$ $\$
63		ralnex 2427	. . . . . 6
64	63	notbii 658	. . . . 5
65	62, 64	syl6bb 195	. . . 4 Markov $/\$ $\$
66	32	eqeq1d 2149	. . . . . 6 Markov $/\$ $/\$ $\$ $\$
67	35	eqeq1i 2148	. . . . . . . . . . 11 $\$
68	38, 67	nemtbir 2398	. . . . . . . . . 10 $\$
69	34	eqeq1d 2149	. . . . . . . . . 10 $\$ $\$
70	68, 69	mtbiri 665	. . . . . . . . 9 $\$
71	70	adantl 275	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
72	71, 42	2falsed 692	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
73	47, 44	eqtrdi 2189	. . . . . . . . 9 $\$
74	73	adantl 275	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
75		simpr 109	. . . . . . . 8 Markov $/\$ $/\$ $/\$
76	74, 75	2thd 174	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
77	72, 76, 58	mpjaodan 788	. . . . . 6 Markov $/\$ $/\$ $\$
78	66, 77	bitrd 187	. . . . 5 Markov $/\$ $/\$ $\$
79	78	rexbidva 2435	. . . 4 Markov $/\$ $\$
80	24, 65, 79	3imtr3d 201	. . 3 Markov $/\$
81	80	ralrimiva 2508	. 2 Markov
82		elex 2700	. . . . 5
83	82	adantr 274	. . . 4 $/\$
84		fveq1 5428	. . . . . . . . . . . 12 $\$ $\$
85	84	eqeq1d 2149	. . . . . . . . . . 11 $\$ $\$
86	85	rexbidv 2439	. . . . . . . . . 10 $\$ $\$
87	86	notbid 657	. . . . . . . . 9 $\$ $\$
88	87	notbid 657	. . . . . . . 8 $\$ $\$
89	88, 86	imbi12d 233	. . . . . . 7 $\$ $\$ $\$
90		simplr 520	. . . . . . 7 $/\$ $/\$
91		elmapi 6572	. . . . . . . . . . . 12
92	91	adantl 275	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelrnda 5563	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6344	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5583	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 519	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6564	. . . . . . . 8 $/\$ $/\$ $\$ $\$
100	96, 99	mpbird 166	. . . . . . 7 $/\$ $/\$ $\$
101	89, 90, 100	rspcdva 2798	. . . . . 6 $/\$ $/\$ $\$ $\$
102		ralnex 2427	. . . . . . . 8 $\$ $\$
103	102	notbii 658	. . . . . . 7 $\$ $\$
104		nfv 1509	. . . . . . . . . . 11
105		nfcv 2282	. . . . . . . . . . . 12
106		nfre1 2479	. . . . . . . . . . . . . . 15
107	106	nfn 1637	. . . . . . . . . . . . . 14
108	107	nfn 1637	. . . . . . . . . . . . 13
109	108, 106	nfim 1552	. . . . . . . . . . . 12
110	105, 109	nfralxy 2474	. . . . . . . . . . 11
111	104, 110	nfan 1545	. . . . . . . . . 10 $/\$
112		nfv 1509	. . . . . . . . . 10
113	111, 112	nfan 1545	. . . . . . . . 9 $/\$ $/\$
114		eqid 2140	. . . . . . . . . . . . 13 $\$ $\$
115		fveq2 5429	. . . . . . . . . . . . . 14
116	115	difeq2d 3199	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 109	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4077	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5522	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2149	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 657	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3193	. . . . . . . . . . . . . . 15 $\$ $\$
124	123, 35	eqtrdi 2189	. . . . . . . . . . . . . 14 $\$
125	124	adantl 275	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
126	125	notnotd 620	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
127		eqeq1 2147	. . . . . . . . . . . . . 14
128	39, 127	mtbiri 665	. . . . . . . . . . . . 13
129	128	adantl 275	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
130	126, 129	2falsed 692	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
131		difeq2 3193	. . . . . . . . . . . . . . 15 $\$ $\$
132	131	eqeq1d 2149	. . . . . . . . . . . . . 14 $\$ $\$
133	46, 132	mtbiri 665	. . . . . . . . . . . . 13 $\$
134	133	adantl 275	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
135		simpr 109	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
136	134, 135	2thd 174	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
137	91	ad2antlr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
138	137, 117	ffvelrnd 5564	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2233	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3555	. . . . . . . . . . . 12 $\/$
141	139, 140	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
142	130, 136, 141	mpjaodan 788	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$
143	122, 142	bitrd 187	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
144	113, 143	ralbida 2432	. . . . . . . 8 $/\$ $/\$ $\$
145	144	notbid 657	. . . . . . 7 $/\$ $/\$ $\$
146	103, 145	bitr3id 193	. . . . . 6 $/\$ $/\$ $\$
147		simpr 109	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
148	125, 147	2thd 174	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
149	128, 135	nsyl3 616	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
150	134, 149	2falsed 692	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
151	148, 150, 141	mpjaodan 788	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
152	121, 151	bitrd 187	. . . . . . 7 $/\$ $/\$ $/\$ $\$
153	113, 152	rexbida 2433	. . . . . 6 $/\$ $/\$ $\$
154	101, 146, 153	3imtr3d 201	. . . . 5 $/\$ $/\$
155	154	ralrimiva 2508	. . . 4 $/\$
156	9	biimprd 157	. . . 4 Markov
157	83, 155, 156	sylc 62	. . 3 $/\$ Markov
158	157	ex 114	. 2 Markov
159	81, 158	impbid2 142	1 Markov

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698

wceq 1332

wcel 1481

wral 2417

wrex 2418

cvv 2689 $\$ cdif 3073

c0 3368

cpr 3533

cmpt 3997

com 4512

wf 5127

cfv 5131 (class class class)co 5782

c1o 6314

c2o 6315

cmap 6550 Markovcmarkov 7033

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-13 1492 ax-14 1493 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-sep 4054 ax-nul 4062 ax-pow 4106 ax-pr 4139 ax-un 4363 ax-setind 4460

This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ne 2310 df-ral 2422 df-rex 2423 df-rab 2426 df-v 2691 df-sbc 2914 df-csb 3008 df-dif 3078 df-un 3080 df-in 3082 df-ss 3089 df-nul 3369 df-pw 3517 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-int 3780 df-br 3938 df-opab 3998 df-mpt 3999 df-tr 4035 df-id 4223 df-iord 4296 df-on 4298 df-suc 4301 df-iom 4513 df-xp 4553 df-rel 4554 df-cnv 4555 df-co 4556 df-dm 4557 df-rn 4558 df-res 4559 df-ima 4560 df-iota 5096 df-fun 5133 df-fn 5134 df-f 5135 df-fv 5139 df-ov 5785 df-oprab 5786 df-mpo 5787 df-1o 6321 df-2o 6322 df-map 6552 df-markov 7034

This theorem is referenced by: subctctexmid 13369

W3C validator