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

Theorem tapeq1 7251
Description: Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
Assertion
Ref Expression
tapeq1  |-  ( R  =  S  ->  ( R TAp  A  <->  S TAp  A )
)

Proof of Theorem tapeq1
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3179 . . 3  |-  ( R  =  S  ->  ( R  C_  ( A  X.  A )  <->  S  C_  ( A  X.  A ) ) )
2 breq 4006 . . . . . 6  |-  ( R  =  S  ->  (
x R x  <->  x S x ) )
32notbid 667 . . . . 5  |-  ( R  =  S  ->  ( -.  x R x  <->  -.  x S x ) )
43ralbidv 2477 . . . 4  |-  ( R  =  S  ->  ( A. x  e.  A  -.  x R x  <->  A. x  e.  A  -.  x S x ) )
5 breq 4006 . . . . . 6  |-  ( R  =  S  ->  (
x R y  <->  x S
y ) )
6 breq 4006 . . . . . 6  |-  ( R  =  S  ->  (
y R x  <->  y S x ) )
75, 6imbi12d 234 . . . . 5  |-  ( R  =  S  ->  (
( x R y  ->  y R x )  <->  ( x S y  ->  y S x ) ) )
872ralbidv 2501 . . . 4  |-  ( R  =  S  ->  ( A. x  e.  A  A. y  e.  A  ( x R y  ->  y R x )  <->  A. x  e.  A  A. y  e.  A  ( x S y  ->  y S x ) ) )
94, 8anbi12d 473 . . 3  |-  ( R  =  S  ->  (
( A. x  e.  A  -.  x R x  /\  A. x  e.  A  A. y  e.  A  ( x R y  ->  y R x ) )  <-> 
( A. x  e.  A  -.  x S x  /\  A. x  e.  A  A. y  e.  A  ( x S y  ->  y S x ) ) ) )
10 breq 4006 . . . . . . . 8  |-  ( R  =  S  ->  (
x R z  <->  x S
z ) )
11 breq 4006 . . . . . . . 8  |-  ( R  =  S  ->  (
y R z  <->  y S
z ) )
1210, 11orbi12d 793 . . . . . . 7  |-  ( R  =  S  ->  (
( x R z  \/  y R z )  <->  ( x S z  \/  y S z ) ) )
135, 12imbi12d 234 . . . . . 6  |-  ( R  =  S  ->  (
( x R y  ->  ( x R z  \/  y R z ) )  <->  ( x S y  ->  (
x S z  \/  y S z ) ) ) )
1413ralbidv 2477 . . . . 5  |-  ( R  =  S  ->  ( A. z  e.  A  ( x R y  ->  ( x R z  \/  y R z ) )  <->  A. z  e.  A  ( x S y  ->  (
x S z  \/  y S z ) ) ) )
15142ralbidv 2501 . . . 4  |-  ( R  =  S  ->  ( A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x R y  ->  ( x R z  \/  y R z ) )  <->  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x S y  ->  (
x S z  \/  y S z ) ) ) )
165notbid 667 . . . . . 6  |-  ( R  =  S  ->  ( -.  x R y  <->  -.  x S y ) )
1716imbi1d 231 . . . . 5  |-  ( R  =  S  ->  (
( -.  x R y  ->  x  =  y )  <->  ( -.  x S y  ->  x  =  y ) ) )
18172ralbidv 2501 . . . 4  |-  ( R  =  S  ->  ( A. x  e.  A  A. y  e.  A  ( -.  x R
y  ->  x  =  y )  <->  A. x  e.  A  A. y  e.  A  ( -.  x S y  ->  x  =  y ) ) )
1915, 18anbi12d 473 . . 3  |-  ( R  =  S  ->  (
( A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x R y  ->  ( x R z  \/  y R z ) )  /\  A. x  e.  A  A. y  e.  A  ( -.  x R y  ->  x  =  y ) )  <-> 
( A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x S y  ->  ( x S z  \/  y S z ) )  /\  A. x  e.  A  A. y  e.  A  ( -.  x S y  ->  x  =  y ) ) ) )
201, 9, 193anbi123d 1312 . 2  |-  ( R  =  S  ->  (
( R  C_  ( A  X.  A )  /\  ( A. x  e.  A  -.  x R x  /\  A. x  e.  A  A. y  e.  A  (
x R y  -> 
y R x ) )  /\  ( A. x  e.  A  A. y  e.  A  A. z  e.  A  (
x R y  -> 
( x R z  \/  y R z ) )  /\  A. x  e.  A  A. y  e.  A  ( -.  x R y  ->  x  =  y )
) )  <->  ( S  C_  ( A  X.  A
)  /\  ( A. x  e.  A  -.  x S x  /\  A. x  e.  A  A. y  e.  A  (
x S y  -> 
y S x ) )  /\  ( A. x  e.  A  A. y  e.  A  A. z  e.  A  (
x S y  -> 
( x S z  \/  y S z ) )  /\  A. x  e.  A  A. y  e.  A  ( -.  x S y  ->  x  =  y )
) ) ) )
21 dftap2 7250 . 2  |-  ( R TAp 
A  <->  ( R  C_  ( A  X.  A
)  /\  ( A. x  e.  A  -.  x R x  /\  A. x  e.  A  A. y  e.  A  (
x R y  -> 
y R x ) )  /\  ( A. x  e.  A  A. y  e.  A  A. z  e.  A  (
x R y  -> 
( x R z  \/  y R z ) )  /\  A. x  e.  A  A. y  e.  A  ( -.  x R y  ->  x  =  y )
) ) )
22 dftap2 7250 . 2  |-  ( S TAp 
A  <->  ( S  C_  ( A  X.  A
)  /\  ( A. x  e.  A  -.  x S x  /\  A. x  e.  A  A. y  e.  A  (
x S y  -> 
y S x ) )  /\  ( A. x  e.  A  A. y  e.  A  A. z  e.  A  (
x S y  -> 
( x S z  \/  y S z ) )  /\  A. x  e.  A  A. y  e.  A  ( -.  x S y  ->  x  =  y )
) ) )
2320, 21, 223bitr4g 223 1  |-  ( R  =  S  ->  ( R TAp  A  <->  S TAp  A )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 708    /\ w3a 978    = wceq 1353   A.wral 2455    C_ wss 3130   class class class wbr 4004    X. cxp 4625   TAp wtap 7248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-ral 2460  df-in 3136  df-ss 3143  df-br 4005  df-pap 7247  df-tap 7249
This theorem is referenced by:  2omotaplemst  7257  exmidapne  7259  exmidmotap  7260
  Copyright terms: Public domain W3C validator