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

Theorem tapeq1 7319
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 3206 . . 3  |-  ( R  =  S  ->  ( R  C_  ( A  X.  A )  <->  S  C_  ( A  X.  A ) ) )
2 breq 4035 . . . . . 6  |-  ( R  =  S  ->  (
x R x  <->  x S x ) )
32notbid 668 . . . . 5  |-  ( R  =  S  ->  ( -.  x R x  <->  -.  x S x ) )
43ralbidv 2497 . . . 4  |-  ( R  =  S  ->  ( A. x  e.  A  -.  x R x  <->  A. x  e.  A  -.  x S x ) )
5 breq 4035 . . . . . 6  |-  ( R  =  S  ->  (
x R y  <->  x S
y ) )
6 breq 4035 . . . . . 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 2521 . . . 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 4035 . . . . . . . 8  |-  ( R  =  S  ->  (
x R z  <->  x S
z ) )
11 breq 4035 . . . . . . . 8  |-  ( R  =  S  ->  (
y R z  <->  y S
z ) )
1210, 11orbi12d 794 . . . . . . 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 2497 . . . . 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 2521 . . . 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 668 . . . . . 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 2521 . . . 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 1323 . 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 7318 . 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 7318 . 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 709    /\ w3a 980    = wceq 1364   A.wral 2475    C_ wss 3157   class class class wbr 4033    X. cxp 4661   TAp wtap 7316
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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178
This theorem depends on definitions:  df-bi 117  df-3an 982  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-ral 2480  df-in 3163  df-ss 3170  df-br 4034  df-pap 7315  df-tap 7317
This theorem is referenced by:  2omotaplemst  7325  exmidapne  7327  exmidmotap  7328
  Copyright terms: Public domain W3C validator