ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7119

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 5485	. . . . . . . . 9 $\$ $\$
2	1	eqeq1d 2174	. . . . . . . 8 $\$ $\$
3	2	ralbidv 2466	. . . . . . 7 $\$ $\$
4	3	notbid 657	. . . . . 6 $\$ $\$
5	1	eqeq1d 2174	. . . . . . 7 $\$ $\$
6	5	rexbidv 2467	. . . . . 6 $\$ $\$
7	4, 6	imbi12d 233	. . . . 5 $\$ $\$ $\$
8		elex 2737	. . . . . . 7 Markov
9		ismkvmap 7118	. . . . . . . 8 Markov
10	9	biimpd 143	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 274	. . . . 5 Markov $/\$
13		elmapi 6636	. . . . . . . . . 10
14	13	adantl 275	. . . . . . . . 9 Markov $/\$
15	14	ffvelrnda 5620	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6407	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5640	. . . . . 6 Markov $/\$ $\$
19		2onn 6489	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 108	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6628	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 166	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2835	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2165	. . . . . . . . . 10 $\$ $\$
26		fveq2 5486	. . . . . . . . . . 11
27	26	difeq2d 3240	. . . . . . . . . 10 $\$ $\$
28		simpr 109	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6392	. . . . . . . . . . 11
30		difexg 4123	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5579	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2174	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3234	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3479	. . . . . . . . . . . 12 $\$
36	34, 35	eqtrdi 2215	. . . . . . . . . . 11 $\$
37	36	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6400	. . . . . . . . . . . . 13
39	38	nesymi 2382	. . . . . . . . . . . 12
40		eqeq1 2172	. . . . . . . . . . . 12
41	39, 40	mtbiri 665	. . . . . . . . . . 11
42	41	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
43	37, 42	2thd 174	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
44		difid 3477	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2173	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 661	. . . . . . . . . . . 12 $\$
47		difeq2 3234	. . . . . . . . . . . . 13 $\$ $\$
48	47	eqeq1d 2174	. . . . . . . . . . . 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 5620	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6398	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2259	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3599	. . . . . . . . . 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 2462	. . . . . 6 Markov $/\$ $\$
62	61	notbid 657	. . . . 5 Markov $/\$ $\$
63		ralnex 2454	. . . . . 6
64	63	notbii 658	. . . . 5
65	62, 64	bitrdi 195	. . . 4 Markov $/\$ $\$
66	32	eqeq1d 2174	. . . . . 6 Markov $/\$ $/\$ $\$ $\$
67	35	eqeq1i 2173	. . . . . . . . . . 11 $\$
68	38, 67	nemtbir 2425	. . . . . . . . . 10 $\$
69	34	eqeq1d 2174	. . . . . . . . . 10 $\$ $\$
70	68, 69	mtbiri 665	. . . . . . . . 9 $\$
71	70	adantl 275	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
72	71, 42	2falsed 692	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
73	47, 44	eqtrdi 2215	. . . . . . . . 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 2463	. . . 4 Markov $/\$ $\$
80	24, 65, 79	3imtr3d 201	. . 3 Markov $/\$
81	80	ralrimiva 2539	. 2 Markov
82		elex 2737	. . . . 5
83	82	adantr 274	. . . 4 $/\$
84		fveq1 5485	. . . . . . . . . . . 12 $\$ $\$
85	84	eqeq1d 2174	. . . . . . . . . . 11 $\$ $\$
86	85	rexbidv 2467	. . . . . . . . . 10 $\$ $\$
87	86	notbid 657	. . . . . . . . 9 $\$ $\$
88	87	notbid 657	. . . . . . . 8 $\$ $\$
89	88, 86	imbi12d 233	. . . . . . 7 $\$ $\$ $\$
90		simplr 520	. . . . . . 7 $/\$ $/\$
91		elmapi 6636	. . . . . . . . . . . 12
92	91	adantl 275	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelrnda 5620	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6407	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5640	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 519	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6628	. . . . . . . 8 $/\$ $/\$ $\$ $\$
100	96, 99	mpbird 166	. . . . . . 7 $/\$ $/\$ $\$
101	89, 90, 100	rspcdva 2835	. . . . . 6 $/\$ $/\$ $\$ $\$
102		ralnex 2454	. . . . . . . 8 $\$ $\$
103	102	notbii 658	. . . . . . 7 $\$ $\$
104		nfv 1516	. . . . . . . . . . 11
105		nfcv 2308	. . . . . . . . . . . 12
106		nfre1 2509	. . . . . . . . . . . . . . 15
107	106	nfn 1646	. . . . . . . . . . . . . 14
108	107	nfn 1646	. . . . . . . . . . . . 13
109	108, 106	nfim 1560	. . . . . . . . . . . 12
110	105, 109	nfralxy 2504	. . . . . . . . . . 11
111	104, 110	nfan 1553	. . . . . . . . . 10 $/\$
112		nfv 1516	. . . . . . . . . 10
113	111, 112	nfan 1553	. . . . . . . . 9 $/\$ $/\$
114		eqid 2165	. . . . . . . . . . . . 13 $\$ $\$
115		fveq2 5486	. . . . . . . . . . . . . 14
116	115	difeq2d 3240	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 109	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4123	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5579	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2174	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 657	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3234	. . . . . . . . . . . . . . 15 $\$ $\$
124	123, 35	eqtrdi 2215	. . . . . . . . . . . . . 14 $\$
125	124	adantl 275	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
126	125	notnotd 620	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
127		eqeq1 2172	. . . . . . . . . . . . . 14
128	39, 127	mtbiri 665	. . . . . . . . . . . . 13
129	128	adantl 275	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
130	126, 129	2falsed 692	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
131		difeq2 3234	. . . . . . . . . . . . . . 15 $\$ $\$
132	131	eqeq1d 2174	. . . . . . . . . . . . . 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 5621	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2259	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3599	. . . . . . . . . . . 12 $\/$
141	139, 140	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
142	130, 136, 141	mpjaodan 788	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$
143	122, 142	bitrd 187	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
144	113, 143	ralbida 2460	. . . . . . . 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 2461	. . . . . 6 $/\$ $/\$ $\$
154	101, 146, 153	3imtr3d 201	. . . . 5 $/\$ $/\$
155	154	ralrimiva 2539	. . . 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 1343

wcel 2136

wral 2444

wrex 2445

cvv 2726 $\$ cdif 3113

c0 3409

cpr 3577

cmpt 4043

com 4567

wf 5184

cfv 5188 (class class class)co 5842

c1o 6377

c2o 6378

cmap 6614 Markovcmarkov 7115

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 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514

This theorem depends on definitions: df-bi 116 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-ral 2449 df-rex 2450 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-iord 4344 df-on 4346 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-fv 5196 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1o 6384 df-2o 6385 df-map 6616 df-markov 7116

This theorem is referenced by: subctctexmid 13881

W3C validator