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

Theorem tapeq1 7253
Description: Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
Assertion
Ref Expression
tapeq1 (𝑅 = 𝑆 → (𝑅 TAp 𝐴𝑆 TAp 𝐴))

Proof of Theorem tapeq1
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3180 . . 3 (𝑅 = 𝑆 → (𝑅 ⊆ (𝐴 × 𝐴) ↔ 𝑆 ⊆ (𝐴 × 𝐴)))
2 breq 4007 . . . . . 6 (𝑅 = 𝑆 → (𝑥𝑅𝑥𝑥𝑆𝑥))
32notbid 667 . . . . 5 (𝑅 = 𝑆 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑥𝑆𝑥))
43ralbidv 2477 . . . 4 (𝑅 = 𝑆 → (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥𝐴 ¬ 𝑥𝑆𝑥))
5 breq 4007 . . . . . 6 (𝑅 = 𝑆 → (𝑥𝑅𝑦𝑥𝑆𝑦))
6 breq 4007 . . . . . 6 (𝑅 = 𝑆 → (𝑦𝑅𝑥𝑦𝑆𝑥))
75, 6imbi12d 234 . . . . 5 (𝑅 = 𝑆 → ((𝑥𝑅𝑦𝑦𝑅𝑥) ↔ (𝑥𝑆𝑦𝑦𝑆𝑥)))
872ralbidv 2501 . . . 4 (𝑅 = 𝑆 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑥) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑆𝑦𝑦𝑆𝑥)))
94, 8anbi12d 473 . . 3 (𝑅 = 𝑆 → ((∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑥)) ↔ (∀𝑥𝐴 ¬ 𝑥𝑆𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑆𝑦𝑦𝑆𝑥))))
10 breq 4007 . . . . . . . 8 (𝑅 = 𝑆 → (𝑥𝑅𝑧𝑥𝑆𝑧))
11 breq 4007 . . . . . . . 8 (𝑅 = 𝑆 → (𝑦𝑅𝑧𝑦𝑆𝑧))
1210, 11orbi12d 793 . . . . . . 7 (𝑅 = 𝑆 → ((𝑥𝑅𝑧𝑦𝑅𝑧) ↔ (𝑥𝑆𝑧𝑦𝑆𝑧)))
135, 12imbi12d 234 . . . . . 6 (𝑅 = 𝑆 → ((𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ↔ (𝑥𝑆𝑦 → (𝑥𝑆𝑧𝑦𝑆𝑧))))
1413ralbidv 2477 . . . . 5 (𝑅 = 𝑆 → (∀𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ↔ ∀𝑧𝐴 (𝑥𝑆𝑦 → (𝑥𝑆𝑧𝑦𝑆𝑧))))
15142ralbidv 2501 . . . 4 (𝑅 = 𝑆 → (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑆𝑦 → (𝑥𝑆𝑧𝑦𝑆𝑧))))
165notbid 667 . . . . . 6 (𝑅 = 𝑆 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑆𝑦))
1716imbi1d 231 . . . . 5 (𝑅 = 𝑆 → ((¬ 𝑥𝑅𝑦𝑥 = 𝑦) ↔ (¬ 𝑥𝑆𝑦𝑥 = 𝑦)))
18172ralbidv 2501 . . . 4 (𝑅 = 𝑆 → (∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦) ↔ ∀𝑥𝐴𝑦𝐴𝑥𝑆𝑦𝑥 = 𝑦)))
1915, 18anbi12d 473 . . 3 (𝑅 = 𝑆 → ((∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦)) ↔ (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑆𝑦 → (𝑥𝑆𝑧𝑦𝑆𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑆𝑦𝑥 = 𝑦))))
201, 9, 193anbi123d 1312 . 2 (𝑅 = 𝑆 → ((𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦))) ↔ (𝑆 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥𝐴 ¬ 𝑥𝑆𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑆𝑦𝑦𝑆𝑥)) ∧ (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑆𝑦 → (𝑥𝑆𝑧𝑦𝑆𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑆𝑦𝑥 = 𝑦)))))
21 dftap2 7252 . 2 (𝑅 TAp 𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦))))
22 dftap2 7252 . 2 (𝑆 TAp 𝐴 ↔ (𝑆 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥𝐴 ¬ 𝑥𝑆𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑆𝑦𝑦𝑆𝑥)) ∧ (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑆𝑦 → (𝑥𝑆𝑧𝑦𝑆𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑆𝑦𝑥 = 𝑦))))
2320, 21, 223bitr4g 223 1 (𝑅 = 𝑆 → (𝑅 TAp 𝐴𝑆 TAp 𝐴))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  w3a 978   = wceq 1353  wral 2455  wss 3131   class class class wbr 4005   × cxp 4626   TAp wtap 7250
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 3137  df-ss 3144  df-br 4006  df-pap 7249  df-tap 7251
This theorem is referenced by:  2omotaplemst  7259  exmidapne  7261  exmidmotap  7262
  Copyright terms: Public domain W3C validator