ismkvnex - Intuitionistic Logic Explorer

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

Theorem ismkvnex 7077

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 5460	. . . . . . . . 9 $\$ $\$
2	1	eqeq1d 2163	. . . . . . . 8 $\$ $\$
3	2	ralbidv 2454	. . . . . . 7 $\$ $\$
4	3	notbid 657	. . . . . 6 $\$ $\$
5	1	eqeq1d 2163	. . . . . . 7 $\$ $\$
6	5	rexbidv 2455	. . . . . 6 $\$ $\$
7	4, 6	imbi12d 233	. . . . 5 $\$ $\$ $\$
8		elex 2720	. . . . . . 7 Markov
9		ismkvmap 7076	. . . . . . . 8 Markov
10	9	biimpd 143	. . . . . . 7 Markov
11	8, 10	mpcom 36	. . . . . 6 Markov
12	11	adantr 274	. . . . 5 Markov $/\$
13		elmapi 6604	. . . . . . . . . 10
14	13	adantl 275	. . . . . . . . 9 Markov $/\$
15	14	ffvelrnda 5595	. . . . . . . 8 Markov $/\$ $/\$
16		2oconcl 6376	. . . . . . . 8 $\$
17	15, 16	syl 14	. . . . . . 7 Markov $/\$ $/\$ $\$
18	17	fmpttd 5615	. . . . . 6 Markov $/\$ $\$
19		2onn 6457	. . . . . . . 8
20	19	a1i 9	. . . . . . 7 Markov $/\$
21		simpl 108	. . . . . . 7 Markov $/\$ Markov
22	20, 21	elmapd 6596	. . . . . 6 Markov $/\$ $\$ $\$
23	18, 22	mpbird 166	. . . . 5 Markov $/\$ $\$
24	7, 12, 23	rspcdva 2818	. . . 4 Markov $/\$ $\$ $\$
25		eqid 2154	. . . . . . . . . 10 $\$ $\$
26		fveq2 5461	. . . . . . . . . . 11
27	26	difeq2d 3221	. . . . . . . . . 10 $\$ $\$
28		simpr 109	. . . . . . . . . 10 Markov $/\$ $/\$
29		1oex 6361	. . . . . . . . . . 11
30		difexg 4101	. . . . . . . . . . 11 $\$
31	29, 30	mp1i 10	. . . . . . . . . 10 Markov $/\$ $/\$ $\$
32	25, 27, 28, 31	fvmptd3 5554	. . . . . . . . 9 Markov $/\$ $/\$ $\$ $\$
33	32	eqeq1d 2163	. . . . . . . 8 Markov $/\$ $/\$ $\$ $\$
34		difeq2 3215	. . . . . . . . . . . 12 $\$ $\$
35		dif0 3460	. . . . . . . . . . . 12 $\$
36	34, 35	eqtrdi 2203	. . . . . . . . . . 11 $\$
37	36	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$ $\$
38		1n0 6369	. . . . . . . . . . . . 13
39	38	nesymi 2370	. . . . . . . . . . . 12
40		eqeq1 2161	. . . . . . . . . . . 12
41	39, 40	mtbiri 665	. . . . . . . . . . 11
42	41	adantl 275	. . . . . . . . . 10 Markov $/\$ $/\$ $/\$
43	37, 42	2thd 174	. . . . . . . . 9 Markov $/\$ $/\$ $/\$ $\$
44		difid 3458	. . . . . . . . . . . . . 14 $\$
45	44	eqeq1i 2162	. . . . . . . . . . . . 13 $\$
46	39, 45	mtbir 661	. . . . . . . . . . . 12 $\$
47		difeq2 3215	. . . . . . . . . . . . 13 $\$ $\$
48	47	eqeq1d 2163	. . . . . . . . . . . 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 5595	. . . . . . . . . . 11 Markov $/\$ $/\$
55		df2o3 6367	. . . . . . . . . . 11
56	54, 55	eleqtrdi 2247	. . . . . . . . . 10 Markov $/\$ $/\$
57		elpri 3579	. . . . . . . . . 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 2450	. . . . . 6 Markov $/\$ $\$
62	61	notbid 657	. . . . 5 Markov $/\$ $\$
63		ralnex 2442	. . . . . 6
64	63	notbii 658	. . . . 5
65	62, 64	bitrdi 195	. . . 4 Markov $/\$ $\$
66	32	eqeq1d 2163	. . . . . 6 Markov $/\$ $/\$ $\$ $\$
67	35	eqeq1i 2162	. . . . . . . . . . 11 $\$
68	38, 67	nemtbir 2413	. . . . . . . . . 10 $\$
69	34	eqeq1d 2163	. . . . . . . . . 10 $\$ $\$
70	68, 69	mtbiri 665	. . . . . . . . 9 $\$
71	70	adantl 275	. . . . . . . 8 Markov $/\$ $/\$ $/\$ $\$
72	71, 42	2falsed 692	. . . . . . 7 Markov $/\$ $/\$ $/\$ $\$
73	47, 44	eqtrdi 2203	. . . . . . . . 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 2451	. . . 4 Markov $/\$ $\$
80	24, 65, 79	3imtr3d 201	. . 3 Markov $/\$
81	80	ralrimiva 2527	. 2 Markov
82		elex 2720	. . . . 5
83	82	adantr 274	. . . 4 $/\$
84		fveq1 5460	. . . . . . . . . . . 12 $\$ $\$
85	84	eqeq1d 2163	. . . . . . . . . . 11 $\$ $\$
86	85	rexbidv 2455	. . . . . . . . . 10 $\$ $\$
87	86	notbid 657	. . . . . . . . 9 $\$ $\$
88	87	notbid 657	. . . . . . . 8 $\$ $\$
89	88, 86	imbi12d 233	. . . . . . 7 $\$ $\$ $\$
90		simplr 520	. . . . . . 7 $/\$ $/\$
91		elmapi 6604	. . . . . . . . . . . 12
92	91	adantl 275	. . . . . . . . . . 11 $/\$ $/\$
93	92	ffvelrnda 5595	. . . . . . . . . 10 $/\$ $/\$ $/\$
94		2oconcl 6376	. . . . . . . . . 10 $\$
95	93, 94	syl 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
96	95	fmpttd 5615	. . . . . . . 8 $/\$ $/\$ $\$
97	19	a1i 9	. . . . . . . . 9 $/\$ $/\$
98		simpll 519	. . . . . . . . 9 $/\$ $/\$
99	97, 98	elmapd 6596	. . . . . . . 8 $/\$ $/\$ $\$ $\$
100	96, 99	mpbird 166	. . . . . . 7 $/\$ $/\$ $\$
101	89, 90, 100	rspcdva 2818	. . . . . 6 $/\$ $/\$ $\$ $\$
102		ralnex 2442	. . . . . . . 8 $\$ $\$
103	102	notbii 658	. . . . . . 7 $\$ $\$
104		nfv 1505	. . . . . . . . . . 11
105		nfcv 2296	. . . . . . . . . . . 12
106		nfre1 2497	. . . . . . . . . . . . . . 15
107	106	nfn 1635	. . . . . . . . . . . . . 14
108	107	nfn 1635	. . . . . . . . . . . . 13
109	108, 106	nfim 1549	. . . . . . . . . . . 12
110	105, 109	nfralxy 2492	. . . . . . . . . . 11
111	104, 110	nfan 1542	. . . . . . . . . 10 $/\$
112		nfv 1505	. . . . . . . . . 10
113	111, 112	nfan 1542	. . . . . . . . 9 $/\$ $/\$
114		eqid 2154	. . . . . . . . . . . . 13 $\$ $\$
115		fveq2 5461	. . . . . . . . . . . . . 14
116	115	difeq2d 3221	. . . . . . . . . . . . 13 $\$ $\$
117		simpr 109	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118		difexg 4101	. . . . . . . . . . . . . 14 $\$
119	29, 118	mp1i 10	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
120	114, 116, 117, 119	fvmptd3 5554	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
121	120	eqeq1d 2163	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
122	121	notbid 657	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
123		difeq2 3215	. . . . . . . . . . . . . . 15 $\$ $\$
124	123, 35	eqtrdi 2203	. . . . . . . . . . . . . 14 $\$
125	124	adantl 275	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
126	125	notnotd 620	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
127		eqeq1 2161	. . . . . . . . . . . . . 14
128	39, 127	mtbiri 665	. . . . . . . . . . . . 13
129	128	adantl 275	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
130	126, 129	2falsed 692	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$
131		difeq2 3215	. . . . . . . . . . . . . . 15 $\$ $\$
132	131	eqeq1d 2163	. . . . . . . . . . . . . 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 5596	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	138, 55	eleqtrdi 2247	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
140		elpri 3579	. . . . . . . . . . . 12 $\/$
141	139, 140	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\/$
142	130, 136, 141	mpjaodan 788	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$
143	122, 142	bitrd 187	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
144	113, 143	ralbida 2448	. . . . . . . 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 2449	. . . . . 6 $/\$ $/\$ $\$
154	101, 146, 153	3imtr3d 201	. . . . 5 $/\$ $/\$
155	154	ralrimiva 2527	. . . 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 2125

wral 2432

wrex 2433

cvv 2709 $\$ cdif 3095

c0 3390

cpr 3557

cmpt 4021

com 4543

wf 5159

cfv 5163 (class class class)co 5814

c1o 6346

c2o 6347

cmap 6582 Markovcmarkov 7073

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 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-sep 4078 ax-nul 4086 ax-pow 4130 ax-pr 4164 ax-un 4388 ax-setind 4490

This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-ral 2437 df-rex 2438 df-rab 2441 df-v 2711 df-sbc 2934 df-csb 3028 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-nul 3391 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-int 3804 df-br 3962 df-opab 4022 df-mpt 4023 df-tr 4059 df-id 4248 df-iord 4321 df-on 4323 df-suc 4326 df-iom 4544 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-rn 4590 df-res 4591 df-ima 4592 df-iota 5128 df-fun 5165 df-fn 5166 df-f 5167 df-fv 5171 df-ov 5817 df-oprab 5818 df-mpo 5819 df-1o 6353 df-2o 6354 df-map 6584 df-markov 7074

This theorem is referenced by: subctctexmid 13512

W3C validator