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

Theorem reg3exmidlemwe 4461
Description: Lemma for reg3exmid 4462. Our counterexample  A satisfies  We. (Contributed by Jim Kingdon, 3-Oct-2021.)
Hypothesis
Ref Expression
reg3exmidlemwe.a  |-  A  =  { x  e.  { (/)
,  { (/) } }  |  ( x  =  { (/) }  \/  (
x  =  (/)  /\  ph ) ) }
Assertion
Ref Expression
reg3exmidlemwe  |-  _E  We  A
Distinct variable group:    ph, x
Allowed substitution hint:    A( x)

Proof of Theorem reg3exmidlemwe
Dummy variables  a  b  c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zfregfr 4456 . 2  |-  _E  Fr  A
2 epel 4182 . . . . . 6  |-  ( a  _E  b  <->  a  e.  b )
3 epel 4182 . . . . . 6  |-  ( b  _E  c  <->  b  e.  c )
42, 3anbi12i 453 . . . . 5  |-  ( ( a  _E  b  /\  b  _E  c )  <->  ( a  e.  b  /\  b  e.  c )
)
5 simpr 109 . . . . . 6  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  -> 
( a  e.  b  /\  b  e.  c ) )
6 elirr 4424 . . . . . . . 8  |-  -.  { (/)
}  e.  { (/) }
7 simprr 504 . . . . . . . . . 10  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  -> 
b  e.  c )
8 noel 3335 . . . . . . . . . . . . 13  |-  -.  a  e.  (/)
9 eleq2 2179 . . . . . . . . . . . . 13  |-  ( b  =  (/)  ->  ( a  e.  b  <->  a  e.  (/) ) )
108, 9mtbiri 647 . . . . . . . . . . . 12  |-  ( b  =  (/)  ->  -.  a  e.  b )
11 simprl 503 . . . . . . . . . . . 12  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  -> 
a  e.  b )
1210, 11nsyl3 598 . . . . . . . . . . 11  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  ->  -.  b  =  (/) )
13 elrabi 2808 . . . . . . . . . . . . . . . 16  |-  ( b  e.  { x  e. 
{ (/) ,  { (/) } }  |  ( x  =  { (/) }  \/  ( x  =  (/)  /\  ph ) ) }  ->  b  e.  { (/) ,  { (/)
} } )
14 reg3exmidlemwe.a . . . . . . . . . . . . . . . 16  |-  A  =  { x  e.  { (/)
,  { (/) } }  |  ( x  =  { (/) }  \/  (
x  =  (/)  /\  ph ) ) }
1513, 14eleq2s 2210 . . . . . . . . . . . . . . 15  |-  ( b  e.  A  ->  b  e.  { (/) ,  { (/) } } )
16 elpri 3518 . . . . . . . . . . . . . . 15  |-  ( b  e.  { (/) ,  { (/)
} }  ->  (
b  =  (/)  \/  b  =  { (/) } ) )
1715, 16syl 14 . . . . . . . . . . . . . 14  |-  ( b  e.  A  ->  (
b  =  (/)  \/  b  =  { (/) } ) )
1817orcomd 701 . . . . . . . . . . . . 13  |-  ( b  e.  A  ->  (
b  =  { (/) }  \/  b  =  (/) ) )
19183ad2ant2 986 . . . . . . . . . . . 12  |-  ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A )  ->  ( b  =  { (/)
}  \/  b  =  (/) ) )
2019adantr 272 . . . . . . . . . . 11  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  -> 
( b  =  { (/)
}  \/  b  =  (/) ) )
2112, 20ecased 1310 . . . . . . . . . 10  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  -> 
b  =  { (/) } )
22 noel 3335 . . . . . . . . . . . . 13  |-  -.  b  e.  (/)
23 eleq2 2179 . . . . . . . . . . . . 13  |-  ( c  =  (/)  ->  ( b  e.  c  <->  b  e.  (/) ) )
2422, 23mtbiri 647 . . . . . . . . . . . 12  |-  ( c  =  (/)  ->  -.  b  e.  c )
2524, 7nsyl3 598 . . . . . . . . . . 11  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  ->  -.  c  =  (/) )
26 elrabi 2808 . . . . . . . . . . . . . . . 16  |-  ( c  e.  { x  e. 
{ (/) ,  { (/) } }  |  ( x  =  { (/) }  \/  ( x  =  (/)  /\  ph ) ) }  ->  c  e.  { (/) ,  { (/)
} } )
2726, 14eleq2s 2210 . . . . . . . . . . . . . . 15  |-  ( c  e.  A  ->  c  e.  { (/) ,  { (/) } } )
28 vex 2661 . . . . . . . . . . . . . . . 16  |-  c  e. 
_V
2928elpr 3516 . . . . . . . . . . . . . . 15  |-  ( c  e.  { (/) ,  { (/)
} }  <->  ( c  =  (/)  \/  c  =  { (/) } ) )
3027, 29sylib 121 . . . . . . . . . . . . . 14  |-  ( c  e.  A  ->  (
c  =  (/)  \/  c  =  { (/) } ) )
3130orcomd 701 . . . . . . . . . . . . 13  |-  ( c  e.  A  ->  (
c  =  { (/) }  \/  c  =  (/) ) )
32313ad2ant3 987 . . . . . . . . . . . 12  |-  ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A )  ->  ( c  =  { (/)
}  \/  c  =  (/) ) )
3332adantr 272 . . . . . . . . . . 11  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  -> 
( c  =  { (/)
}  \/  c  =  (/) ) )
3425, 33ecased 1310 . . . . . . . . . 10  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  -> 
c  =  { (/) } )
357, 21, 343eltr3d 2198 . . . . . . . . 9  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  ->  { (/) }  e.  { (/)
} )
3635ex 114 . . . . . . . 8  |-  ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A )  ->  ( ( a  e.  b  /\  b  e.  c )  ->  { (/) }  e.  { (/) } ) )
376, 36mtoi 636 . . . . . . 7  |-  ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A )  ->  -.  ( a  e.  b  /\  b  e.  c ) )
3837adantr 272 . . . . . 6  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  ->  -.  ( a  e.  b  /\  b  e.  c ) )
395, 38pm2.21dd 592 . . . . 5  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  e.  b  /\  b  e.  c ) )  -> 
a  _E  c )
404, 39sylan2b 283 . . . 4  |-  ( ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A
)  /\  ( a  _E  b  /\  b  _E  c ) )  -> 
a  _E  c )
4140ex 114 . . 3  |-  ( ( a  e.  A  /\  b  e.  A  /\  c  e.  A )  ->  ( ( a  _E  b  /\  b  _E  c )  ->  a  _E  c ) )
4241rgen3 2494 . 2  |-  A. a  e.  A  A. b  e.  A  A. c  e.  A  ( (
a  _E  b  /\  b  _E  c )  ->  a  _E  c )
43 df-wetr 4224 . 2  |-  (  _E  We  A  <->  (  _E  Fr  A  /\  A. a  e.  A  A. b  e.  A  A. c  e.  A  ( (
a  _E  b  /\  b  _E  c )  ->  a  _E  c ) ) )
441, 42, 43mpbir2an 909 1  |-  _E  We  A
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    \/ wo 680    /\ w3a 945    = wceq 1314    e. wcel 1463   A.wral 2391   {crab 2395   (/)c0 3331   {csn 3495   {cpr 3496   class class class wbr 3897    _E cep 4177    Fr wfr 4218    We wwe 4220
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-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099  ax-setind 4420
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  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-rab 2400  df-v 2660  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-br 3898  df-opab 3958  df-eprel 4179  df-frfor 4221  df-frind 4222  df-wetr 4224
This theorem is referenced by:  reg3exmid  4462
  Copyright terms: Public domain W3C validator