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

Theorem ismkvnex 6995
Description: The predicate of being Markov stated in terms of double negation and comparison with  1o. (Contributed by Jim Kingdon, 29-Nov-2023.)
Assertion
Ref Expression
ismkvnex  |-  ( A  e.  V  ->  ( A  e. Markov  <->  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) ) )
Distinct variable groups:    A, f, x   
f, V, x

Proof of Theorem ismkvnex
Dummy variables  g  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq1 5386 . . . . . . . . 9  |-  ( g  =  ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) )  -> 
( g `  x
)  =  ( ( z  e.  A  |->  ( 1o  \  ( f `
 z ) ) ) `  x ) )
21eqeq1d 2124 . . . . . . . 8  |-  ( g  =  ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) )  -> 
( ( g `  x )  =  1o  <->  ( ( z  e.  A  |->  ( 1o  \  (
f `  z )
) ) `  x
)  =  1o ) )
32ralbidv 2412 . . . . . . 7  |-  ( g  =  ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) )  -> 
( A. x  e.  A  ( g `  x )  =  1o  <->  A. x  e.  A  ( ( z  e.  A  |->  ( 1o  \  (
f `  z )
) ) `  x
)  =  1o ) )
43notbid 639 . . . . . 6  |-  ( g  =  ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) )  -> 
( -.  A. x  e.  A  ( g `  x )  =  1o  <->  -. 
A. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  1o ) )
51eqeq1d 2124 . . . . . . 7  |-  ( g  =  ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) )  -> 
( ( g `  x )  =  (/)  <->  (
( z  e.  A  |->  ( 1o  \  (
f `  z )
) ) `  x
)  =  (/) ) )
65rexbidv 2413 . . . . . 6  |-  ( g  =  ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) )  -> 
( E. x  e.  A  ( g `  x )  =  (/)  <->  E. x  e.  A  (
( z  e.  A  |->  ( 1o  \  (
f `  z )
) ) `  x
)  =  (/) ) )
74, 6imbi12d 233 . . . . 5  |-  ( g  =  ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) )  -> 
( ( -.  A. x  e.  A  (
g `  x )  =  1o  ->  E. x  e.  A  ( g `  x )  =  (/) ) 
<->  ( -.  A. x  e.  A  ( (
z  e.  A  |->  ( 1o  \  ( f `
 z ) ) ) `  x )  =  1o  ->  E. x  e.  A  ( (
z  e.  A  |->  ( 1o  \  ( f `
 z ) ) ) `  x )  =  (/) ) ) )
8 elex 2669 . . . . . . 7  |-  ( A  e. Markov  ->  A  e.  _V )
9 ismkvmap 6994 . . . . . . . 8  |-  ( A  e.  _V  ->  ( A  e. Markov  <->  A. g  e.  ( 2o  ^m  A ) ( -.  A. x  e.  A  ( g `  x )  =  1o 
->  E. x  e.  A  ( g `  x
)  =  (/) ) ) )
109biimpd 143 . . . . . . 7  |-  ( A  e.  _V  ->  ( A  e. Markov  ->  A. g  e.  ( 2o  ^m  A
) ( -.  A. x  e.  A  (
g `  x )  =  1o  ->  E. x  e.  A  ( g `  x )  =  (/) ) ) )
118, 10mpcom 36 . . . . . 6  |-  ( A  e. Markov  ->  A. g  e.  ( 2o  ^m  A ) ( -.  A. x  e.  A  ( g `  x )  =  1o 
->  E. x  e.  A  ( g `  x
)  =  (/) ) )
1211adantr 272 . . . . 5  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  A. g  e.  ( 2o  ^m  A
) ( -.  A. x  e.  A  (
g `  x )  =  1o  ->  E. x  e.  A  ( g `  x )  =  (/) ) )
13 elmapi 6530 . . . . . . . . . 10  |-  ( f  e.  ( 2o  ^m  A )  ->  f : A --> 2o )
1413adantl 273 . . . . . . . . 9  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  f : A --> 2o )
1514ffvelrnda 5521 . . . . . . . 8  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  z  e.  A )  ->  (
f `  z )  e.  2o )
16 2oconcl 6302 . . . . . . . 8  |-  ( ( f `  z )  e.  2o  ->  ( 1o  \  ( f `  z ) )  e.  2o )
1715, 16syl 14 . . . . . . 7  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  z  e.  A )  ->  ( 1o  \  ( f `  z ) )  e.  2o )
1817fmpttd 5541 . . . . . 6  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  (
z  e.  A  |->  ( 1o  \  ( f `
 z ) ) ) : A --> 2o )
19 2onn 6383 . . . . . . . 8  |-  2o  e.  om
2019a1i 9 . . . . . . 7  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  2o  e.  om )
21 simpl 108 . . . . . . 7  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  A  e. Markov )
2220, 21elmapd 6522 . . . . . 6  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  (
( z  e.  A  |->  ( 1o  \  (
f `  z )
) )  e.  ( 2o  ^m  A )  <-> 
( z  e.  A  |->  ( 1o  \  (
f `  z )
) ) : A --> 2o ) )
2318, 22mpbird 166 . . . . 5  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  (
z  e.  A  |->  ( 1o  \  ( f `
 z ) ) )  e.  ( 2o 
^m  A ) )
247, 12, 23rspcdva 2766 . . . 4  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  ( -.  A. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  1o 
->  E. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  (/) ) )
25 eqid 2115 . . . . . . . . . 10  |-  ( z  e.  A  |->  ( 1o 
\  ( f `  z ) ) )  =  ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) )
26 fveq2 5387 . . . . . . . . . . 11  |-  ( z  =  x  ->  (
f `  z )  =  ( f `  x ) )
2726difeq2d 3162 . . . . . . . . . 10  |-  ( z  =  x  ->  ( 1o  \  ( f `  z ) )  =  ( 1o  \  (
f `  x )
) )
28 simpr 109 . . . . . . . . . 10  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  x  e.  A )
29 1oex 6287 . . . . . . . . . . 11  |-  1o  e.  _V
30 difexg 4037 . . . . . . . . . . 11  |-  ( 1o  e.  _V  ->  ( 1o  \  ( f `  x ) )  e. 
_V )
3129, 30mp1i 10 . . . . . . . . . 10  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  ( 1o  \  ( f `  x ) )  e. 
_V )
3225, 27, 28, 31fvmptd3 5480 . . . . . . . . 9  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( z  e.  A  |->  ( 1o  \  (
f `  z )
) ) `  x
)  =  ( 1o 
\  ( f `  x ) ) )
3332eqeq1d 2124 . . . . . . . 8  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  1o  <->  ( 1o  \  ( f `
 x ) )  =  1o ) )
34 difeq2 3156 . . . . . . . . . . . 12  |-  ( ( f `  x )  =  (/)  ->  ( 1o 
\  ( f `  x ) )  =  ( 1o  \  (/) ) )
35 dif0 3401 . . . . . . . . . . . 12  |-  ( 1o 
\  (/) )  =  1o
3634, 35syl6eq 2164 . . . . . . . . . . 11  |-  ( ( f `  x )  =  (/)  ->  ( 1o 
\  ( f `  x ) )  =  1o )
3736adantl 273 . . . . . . . . . 10  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  (/) )  ->  ( 1o  \ 
( f `  x
) )  =  1o )
38 1n0 6295 . . . . . . . . . . . . 13  |-  1o  =/=  (/)
3938nesymi 2329 . . . . . . . . . . . 12  |-  -.  (/)  =  1o
40 eqeq1 2122 . . . . . . . . . . . 12  |-  ( ( f `  x )  =  (/)  ->  ( ( f `  x )  =  1o  <->  (/)  =  1o ) )
4139, 40mtbiri 647 . . . . . . . . . . 11  |-  ( ( f `  x )  =  (/)  ->  -.  (
f `  x )  =  1o )
4241adantl 273 . . . . . . . . . 10  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  (/) )  ->  -.  ( f `  x )  =  1o )
4337, 422thd 174 . . . . . . . . 9  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  (/) )  ->  ( ( 1o 
\  ( f `  x ) )  =  1o  <->  -.  ( f `  x )  =  1o ) )
44 difid 3399 . . . . . . . . . . . . . 14  |-  ( 1o 
\  1o )  =  (/)
4544eqeq1i 2123 . . . . . . . . . . . . 13  |-  ( ( 1o  \  1o )  =  1o  <->  (/)  =  1o )
4639, 45mtbir 643 . . . . . . . . . . . 12  |-  -.  ( 1o  \  1o )  =  1o
47 difeq2 3156 . . . . . . . . . . . . 13  |-  ( ( f `  x )  =  1o  ->  ( 1o  \  ( f `  x ) )  =  ( 1o  \  1o ) )
4847eqeq1d 2124 . . . . . . . . . . . 12  |-  ( ( f `  x )  =  1o  ->  (
( 1o  \  (
f `  x )
)  =  1o  <->  ( 1o  \  1o )  =  1o ) )
4946, 48mtbiri 647 . . . . . . . . . . 11  |-  ( ( f `  x )  =  1o  ->  -.  ( 1o  \  (
f `  x )
)  =  1o )
5049adantl 273 . . . . . . . . . 10  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  1o )  ->  -.  ( 1o  \  ( f `  x ) )  =  1o )
51 notnot 601 . . . . . . . . . . 11  |-  ( ( f `  x )  =  1o  ->  -.  -.  ( f `  x
)  =  1o )
5251adantl 273 . . . . . . . . . 10  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  1o )  ->  -.  -.  (
f `  x )  =  1o )
5350, 522falsed 674 . . . . . . . . 9  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  1o )  ->  ( ( 1o  \  ( f `  x ) )  =  1o  <->  -.  ( f `  x )  =  1o ) )
5414ffvelrnda 5521 . . . . . . . . . . 11  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
f `  x )  e.  2o )
55 df2o3 6293 . . . . . . . . . . 11  |-  2o  =  { (/) ,  1o }
5654, 55syl6eleq 2208 . . . . . . . . . 10  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
f `  x )  e.  { (/) ,  1o }
)
57 elpri 3518 . . . . . . . . . 10  |-  ( ( f `  x )  e.  { (/) ,  1o }  ->  ( ( f `
 x )  =  (/)  \/  ( f `  x )  =  1o ) )
5856, 57syl 14 . . . . . . . . 9  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( f `  x
)  =  (/)  \/  (
f `  x )  =  1o ) )
5943, 53, 58mpjaodan 770 . . . . . . . 8  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( 1o  \  (
f `  x )
)  =  1o  <->  -.  (
f `  x )  =  1o ) )
6033, 59bitrd 187 . . . . . . 7  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  1o  <->  -.  ( f `  x
)  =  1o ) )
6160ralbidva 2408 . . . . . 6  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  ( A. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  1o  <->  A. x  e.  A  -.  ( f `  x
)  =  1o ) )
6261notbid 639 . . . . 5  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  ( -.  A. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  1o  <->  -. 
A. x  e.  A  -.  ( f `  x
)  =  1o ) )
63 ralnex 2401 . . . . . 6  |-  ( A. x  e.  A  -.  ( f `  x
)  =  1o  <->  -.  E. x  e.  A  ( f `  x )  =  1o )
6463notbii 640 . . . . 5  |-  ( -. 
A. x  e.  A  -.  ( f `  x
)  =  1o  <->  -.  -.  E. x  e.  A  (
f `  x )  =  1o )
6562, 64syl6bb 195 . . . 4  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  ( -.  A. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  1o  <->  -. 
-.  E. x  e.  A  ( f `  x
)  =  1o ) )
6632eqeq1d 2124 . . . . . 6  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  (/)  <->  ( 1o  \  ( f `  x ) )  =  (/) ) )
6735eqeq1i 2123 . . . . . . . . . . 11  |-  ( ( 1o  \  (/) )  =  (/) 
<->  1o  =  (/) )
6838, 67nemtbir 2372 . . . . . . . . . 10  |-  -.  ( 1o  \  (/) )  =  (/)
6934eqeq1d 2124 . . . . . . . . . 10  |-  ( ( f `  x )  =  (/)  ->  ( ( 1o  \  ( f `
 x ) )  =  (/)  <->  ( 1o  \  (/) )  =  (/) ) )
7068, 69mtbiri 647 . . . . . . . . 9  |-  ( ( f `  x )  =  (/)  ->  -.  ( 1o  \  ( f `  x ) )  =  (/) )
7170adantl 273 . . . . . . . 8  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  (/) )  ->  -.  ( 1o  \  ( f `  x
) )  =  (/) )
7271, 422falsed 674 . . . . . . 7  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  (/) )  ->  ( ( 1o 
\  ( f `  x ) )  =  (/) 
<->  ( f `  x
)  =  1o ) )
7347, 44syl6eq 2164 . . . . . . . . 9  |-  ( ( f `  x )  =  1o  ->  ( 1o  \  ( f `  x ) )  =  (/) )
7473adantl 273 . . . . . . . 8  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  1o )  ->  ( 1o  \  ( f `  x
) )  =  (/) )
75 simpr 109 . . . . . . . 8  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  1o )  ->  ( f `  x )  =  1o )
7674, 752thd 174 . . . . . . 7  |-  ( ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A ) )  /\  x  e.  A
)  /\  ( f `  x )  =  1o )  ->  ( ( 1o  \  ( f `  x ) )  =  (/) 
<->  ( f `  x
)  =  1o ) )
7772, 76, 58mpjaodan 770 . . . . . 6  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( 1o  \  (
f `  x )
)  =  (/)  <->  ( f `  x )  =  1o ) )
7866, 77bitrd 187 . . . . 5  |-  ( ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  (/)  <->  (
f `  x )  =  1o ) )
7978rexbidva 2409 . . . 4  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  ( E. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( f `  z
) ) ) `  x )  =  (/)  <->  E. x  e.  A  (
f `  x )  =  1o ) )
8024, 65, 793imtr3d 201 . . 3  |-  ( ( A  e. Markov  /\  f  e.  ( 2o  ^m  A
) )  ->  ( -.  -.  E. x  e.  A  ( f `  x )  =  1o 
->  E. x  e.  A  ( f `  x
)  =  1o ) )
8180ralrimiva 2480 . 2  |-  ( A  e. Markov  ->  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )
82 elex 2669 . . . . 5  |-  ( A  e.  V  ->  A  e.  _V )
8382adantr 272 . . . 4  |-  ( ( A  e.  V  /\  A. f  e.  ( 2o 
^m  A ) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o 
->  E. x  e.  A  ( f `  x
)  =  1o ) )  ->  A  e.  _V )
84 fveq1 5386 . . . . . . . . . . . 12  |-  ( f  =  ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) )  -> 
( f `  x
)  =  ( ( z  e.  A  |->  ( 1o  \  ( g `
 z ) ) ) `  x ) )
8584eqeq1d 2124 . . . . . . . . . . 11  |-  ( f  =  ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) )  -> 
( ( f `  x )  =  1o  <->  ( ( z  e.  A  |->  ( 1o  \  (
g `  z )
) ) `  x
)  =  1o ) )
8685rexbidv 2413 . . . . . . . . . 10  |-  ( f  =  ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) )  -> 
( E. x  e.  A  ( f `  x )  =  1o  <->  E. x  e.  A  ( ( z  e.  A  |->  ( 1o  \  (
g `  z )
) ) `  x
)  =  1o ) )
8786notbid 639 . . . . . . . . 9  |-  ( f  =  ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) )  -> 
( -.  E. x  e.  A  ( f `  x )  =  1o  <->  -. 
E. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o ) )
8887notbid 639 . . . . . . . 8  |-  ( f  =  ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) )  -> 
( -.  -.  E. x  e.  A  (
f `  x )  =  1o  <->  -.  -.  E. x  e.  A  ( (
z  e.  A  |->  ( 1o  \  ( g `
 z ) ) ) `  x )  =  1o ) )
8988, 86imbi12d 233 . . . . . . 7  |-  ( f  =  ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) )  -> 
( ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o )  <->  ( -.  -.  E. x  e.  A  ( ( z  e.  A  |->  ( 1o  \  (
g `  z )
) ) `  x
)  =  1o  ->  E. x  e.  A  ( ( z  e.  A  |->  ( 1o  \  (
g `  z )
) ) `  x
)  =  1o ) ) )
90 simplr 502 . . . . . . 7  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )
91 elmapi 6530 . . . . . . . . . . . 12  |-  ( g  e.  ( 2o  ^m  A )  ->  g : A --> 2o )
9291adantl 273 . . . . . . . . . . 11  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  g : A --> 2o )
9392ffvelrnda 5521 . . . . . . . . . 10  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  z  e.  A )  ->  (
g `  z )  e.  2o )
94 2oconcl 6302 . . . . . . . . . 10  |-  ( ( g `  z )  e.  2o  ->  ( 1o  \  ( g `  z ) )  e.  2o )
9593, 94syl 14 . . . . . . . . 9  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  z  e.  A )  ->  ( 1o  \  ( g `  z ) )  e.  2o )
9695fmpttd 5541 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  (
z  e.  A  |->  ( 1o  \  ( g `
 z ) ) ) : A --> 2o )
9719a1i 9 . . . . . . . . 9  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  2o  e.  om )
98 simpll 501 . . . . . . . . 9  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  A  e.  V )
9997, 98elmapd 6522 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  (
( z  e.  A  |->  ( 1o  \  (
g `  z )
) )  e.  ( 2o  ^m  A )  <-> 
( z  e.  A  |->  ( 1o  \  (
g `  z )
) ) : A --> 2o ) )
10096, 99mpbird 166 . . . . . . 7  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  (
z  e.  A  |->  ( 1o  \  ( g `
 z ) ) )  e.  ( 2o 
^m  A ) )
10189, 90, 100rspcdva 2766 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( -.  -.  E. x  e.  A  ( ( z  e.  A  |->  ( 1o 
\  ( g `  z ) ) ) `
 x )  =  1o  ->  E. x  e.  A  ( (
z  e.  A  |->  ( 1o  \  ( g `
 z ) ) ) `  x )  =  1o ) )
102 ralnex 2401 . . . . . . . 8  |-  ( A. x  e.  A  -.  ( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o  <->  -. 
E. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o )
103102notbii 640 . . . . . . 7  |-  ( -. 
A. x  e.  A  -.  ( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o  <->  -. 
-.  E. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o )
104 nfv 1491 . . . . . . . . . . 11  |-  F/ x  A  e.  V
105 nfcv 2256 . . . . . . . . . . . 12  |-  F/_ x
( 2o  ^m  A
)
106 nfre1 2451 . . . . . . . . . . . . . . 15  |-  F/ x E. x  e.  A  ( f `  x
)  =  1o
107106nfn 1619 . . . . . . . . . . . . . 14  |-  F/ x  -.  E. x  e.  A  ( f `  x
)  =  1o
108107nfn 1619 . . . . . . . . . . . . 13  |-  F/ x  -.  -.  E. x  e.  A  ( f `  x )  =  1o
109108, 106nfim 1534 . . . . . . . . . . . 12  |-  F/ x
( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o )
110105, 109nfralxy 2446 . . . . . . . . . . 11  |-  F/ x A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o 
->  E. x  e.  A  ( f `  x
)  =  1o )
111104, 110nfan 1527 . . . . . . . . . 10  |-  F/ x
( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )
112 nfv 1491 . . . . . . . . . 10  |-  F/ x  g  e.  ( 2o  ^m  A )
113111, 112nfan 1527 . . . . . . . . 9  |-  F/ x
( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )
114 eqid 2115 . . . . . . . . . . . . 13  |-  ( z  e.  A  |->  ( 1o 
\  ( g `  z ) ) )  =  ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) )
115 fveq2 5387 . . . . . . . . . . . . . 14  |-  ( z  =  x  ->  (
g `  z )  =  ( g `  x ) )
116115difeq2d 3162 . . . . . . . . . . . . 13  |-  ( z  =  x  ->  ( 1o  \  ( g `  z ) )  =  ( 1o  \  (
g `  x )
) )
117 simpr 109 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  x  e.  A )
118 difexg 4037 . . . . . . . . . . . . . 14  |-  ( 1o  e.  _V  ->  ( 1o  \  ( g `  x ) )  e. 
_V )
11929, 118mp1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  ( 1o  \  ( g `  x ) )  e. 
_V )
120114, 116, 117, 119fvmptd3 5480 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( z  e.  A  |->  ( 1o  \  (
g `  z )
) ) `  x
)  =  ( 1o 
\  ( g `  x ) ) )
121120eqeq1d 2124 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o  <->  ( 1o  \  ( g `
 x ) )  =  1o ) )
122121notbid 639 . . . . . . . . . 10  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  ( -.  ( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o  <->  -.  ( 1o  \  (
g `  x )
)  =  1o ) )
123 difeq2 3156 . . . . . . . . . . . . . . 15  |-  ( ( g `  x )  =  (/)  ->  ( 1o 
\  ( g `  x ) )  =  ( 1o  \  (/) ) )
124123, 35syl6eq 2164 . . . . . . . . . . . . . 14  |-  ( ( g `  x )  =  (/)  ->  ( 1o 
\  ( g `  x ) )  =  1o )
125124adantl 273 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  (/) )  ->  ( 1o  \  ( g `  x ) )  =  1o )
126125notnotd 602 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  (/) )  ->  -.  -.  ( 1o  \  (
g `  x )
)  =  1o )
127 eqeq1 2122 . . . . . . . . . . . . . 14  |-  ( ( g `  x )  =  (/)  ->  ( ( g `  x )  =  1o  <->  (/)  =  1o ) )
12839, 127mtbiri 647 . . . . . . . . . . . . 13  |-  ( ( g `  x )  =  (/)  ->  -.  (
g `  x )  =  1o )
129128adantl 273 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  (/) )  ->  -.  ( g `  x
)  =  1o )
130126, 1292falsed 674 . . . . . . . . . . 11  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  (/) )  ->  ( -.  ( 1o  \  (
g `  x )
)  =  1o  <->  ( g `  x )  =  1o ) )
131 difeq2 3156 . . . . . . . . . . . . . . 15  |-  ( ( g `  x )  =  1o  ->  ( 1o  \  ( g `  x ) )  =  ( 1o  \  1o ) )
132131eqeq1d 2124 . . . . . . . . . . . . . 14  |-  ( ( g `  x )  =  1o  ->  (
( 1o  \  (
g `  x )
)  =  1o  <->  ( 1o  \  1o )  =  1o ) )
13346, 132mtbiri 647 . . . . . . . . . . . . 13  |-  ( ( g `  x )  =  1o  ->  -.  ( 1o  \  (
g `  x )
)  =  1o )
134133adantl 273 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  1o )  ->  -.  ( 1o  \  (
g `  x )
)  =  1o )
135 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  1o )  ->  (
g `  x )  =  1o )
136134, 1352thd 174 . . . . . . . . . . 11  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  1o )  ->  ( -.  ( 1o  \  (
g `  x )
)  =  1o  <->  ( g `  x )  =  1o ) )
13791ad2antlr 478 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  g : A --> 2o )
138137, 117ffvelrnd 5522 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
g `  x )  e.  2o )
139138, 55syl6eleq 2208 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
g `  x )  e.  { (/) ,  1o }
)
140 elpri 3518 . . . . . . . . . . . 12  |-  ( ( g `  x )  e.  { (/) ,  1o }  ->  ( ( g `
 x )  =  (/)  \/  ( g `  x )  =  1o ) )
141139, 140syl 14 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( g `  x
)  =  (/)  \/  (
g `  x )  =  1o ) )
142130, 136, 141mpjaodan 770 . . . . . . . . . 10  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  ( -.  ( 1o  \  (
g `  x )
)  =  1o  <->  ( g `  x )  =  1o ) )
143122, 142bitrd 187 . . . . . . . . 9  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  ( -.  ( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o  <->  ( g `  x )  =  1o ) )
144113, 143ralbida 2406 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( A. x  e.  A  -.  ( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o  <->  A. x  e.  A  ( g `  x )  =  1o ) )
145144notbid 639 . . . . . . 7  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( -.  A. x  e.  A  -.  ( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o  <->  -. 
A. x  e.  A  ( g `  x
)  =  1o ) )
146103, 145syl5bbr 193 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( -.  -.  E. x  e.  A  ( ( z  e.  A  |->  ( 1o 
\  ( g `  z ) ) ) `
 x )  =  1o  <->  -.  A. x  e.  A  ( g `  x )  =  1o ) )
147 simpr 109 . . . . . . . . . 10  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  (/) )  ->  (
g `  x )  =  (/) )
148125, 1472thd 174 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  (/) )  ->  (
( 1o  \  (
g `  x )
)  =  1o  <->  ( g `  x )  =  (/) ) )
149128, 135nsyl3 598 . . . . . . . . . 10  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  1o )  ->  -.  ( g `  x
)  =  (/) )
150134, 1492falsed 674 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -. 
-.  E. x  e.  A  ( f `  x
)  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A ) )  /\  x  e.  A )  /\  (
g `  x )  =  1o )  ->  (
( 1o  \  (
g `  x )
)  =  1o  <->  ( g `  x )  =  (/) ) )
151148, 150, 141mpjaodan 770 . . . . . . . 8  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( 1o  \  (
g `  x )
)  =  1o  <->  ( g `  x )  =  (/) ) )
152121, 151bitrd 187 . . . . . . 7  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A
) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o  <->  ( g `  x )  =  (/) ) )
153113, 152rexbida 2407 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( E. x  e.  A  ( ( z  e.  A  |->  ( 1o  \ 
( g `  z
) ) ) `  x )  =  1o  <->  E. x  e.  A  ( g `  x )  =  (/) ) )
154101, 146, 1533imtr3d 201 . . . . 5  |-  ( ( ( A  e.  V  /\  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( -.  A. x  e.  A  ( g `  x
)  =  1o  ->  E. x  e.  A  ( g `  x )  =  (/) ) )
155154ralrimiva 2480 . . . 4  |-  ( ( A  e.  V  /\  A. f  e.  ( 2o 
^m  A ) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o 
->  E. x  e.  A  ( f `  x
)  =  1o ) )  ->  A. g  e.  ( 2o  ^m  A
) ( -.  A. x  e.  A  (
g `  x )  =  1o  ->  E. x  e.  A  ( g `  x )  =  (/) ) )
1569biimprd 157 . . . 4  |-  ( A  e.  _V  ->  ( A. g  e.  ( 2o  ^m  A ) ( -.  A. x  e.  A  ( g `  x )  =  1o 
->  E. x  e.  A  ( g `  x
)  =  (/) )  ->  A  e. Markov ) )
15783, 155, 156sylc 62 . . 3  |-  ( ( A  e.  V  /\  A. f  e.  ( 2o 
^m  A ) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o 
->  E. x  e.  A  ( f `  x
)  =  1o ) )  ->  A  e. Markov )
158157ex 114 . 2  |-  ( A  e.  V  ->  ( A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  ( f `  x )  =  1o 
->  E. x  e.  A  ( f `  x
)  =  1o )  ->  A  e. Markov )
)
15981, 158impbid2 142 1  |-  ( A  e.  V  ->  ( A  e. Markov  <->  A. f  e.  ( 2o  ^m  A ) ( -.  -.  E. x  e.  A  (
f `  x )  =  1o  ->  E. x  e.  A  ( f `  x )  =  1o ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 680    = wceq 1314    e. wcel 1463   A.wral 2391   E.wrex 2392   _Vcvv 2658    \ cdif 3036   (/)c0 3331   {cpr 3496    |-> cmpt 3957   omcom 4472   -->wf 5087   ` cfv 5091  (class class class)co 5740   1oc1o 6272   2oc2o 6273    ^m cmap 6508  Markovcmarkov 6991
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 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-rex 2397  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-iord 4256  df-on 4258  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-fv 5099  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1o 6279  df-2o 6280  df-map 6510  df-markov 6992
This theorem is referenced by:  subctctexmid  13030
  Copyright terms: Public domain W3C validator