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

Theorem enq0enq 6413
 Description: Equivalence on positive fractions in terms of equivalence on non-negative fractions. (Contributed by Jim Kingdon, 12-Nov-2019.)
Assertion
Ref Expression
enq0enq ~Q = ( ~Q0 ∩ ((N × N) × (N × N)))

Proof of Theorem enq0enq
Dummy variables v u w x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-enq0 6406 . . 3 ~Q0 = {⟨x, y⟩ ∣ ((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))}
2 df-xp 4294 . . 3 ((N × N) × (N × N)) = {⟨x, y⟩ ∣ (x (N × N) y (N × N))}
31, 2ineq12i 3130 . 2 ( ~Q0 ∩ ((N × N) × (N × N))) = ({⟨x, y⟩ ∣ ((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))} ∩ {⟨x, y⟩ ∣ (x (N × N) y (N × N))})
4 inopab 4411 . 2 ({⟨x, y⟩ ∣ ((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))} ∩ {⟨x, y⟩ ∣ (x (N × N) y (N × N))}) = {⟨x, y⟩ ∣ (((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) (x (N × N) y (N × N)))}
5 an32 496 . . . . . 6 ((((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) (x (N × N) y (N × N))) ↔ (((x (𝜔 × N) y (𝜔 × N)) (x (N × N) y (N × N))) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
6 an4 520 . . . . . . . 8 (((x (𝜔 × N) y (𝜔 × N)) (x (N × N) y (N × N))) ↔ ((x (𝜔 × N) x (N × N)) (y (𝜔 × N) y (N × N))))
7 pinn 6293 . . . . . . . . . . . . 13 (x Nx 𝜔)
87ssriv 2943 . . . . . . . . . . . 12 N ⊆ 𝜔
9 xpss1 4391 . . . . . . . . . . . 12 (N ⊆ 𝜔 → (N × N) ⊆ (𝜔 × N))
108, 9ax-mp 7 . . . . . . . . . . 11 (N × N) ⊆ (𝜔 × N)
1110sseli 2935 . . . . . . . . . 10 (x (N × N) → x (𝜔 × N))
1211pm4.71ri 372 . . . . . . . . 9 (x (N × N) ↔ (x (𝜔 × N) x (N × N)))
1310sseli 2935 . . . . . . . . . 10 (y (N × N) → y (𝜔 × N))
1413pm4.71ri 372 . . . . . . . . 9 (y (N × N) ↔ (y (𝜔 × N) y (N × N)))
1512, 14anbi12i 433 . . . . . . . 8 ((x (N × N) y (N × N)) ↔ ((x (𝜔 × N) x (N × N)) (y (𝜔 × N) y (N × N))))
166, 15bitr4i 176 . . . . . . 7 (((x (𝜔 × N) y (𝜔 × N)) (x (N × N) y (N × N))) ↔ (x (N × N) y (N × N)))
1716anbi1i 431 . . . . . 6 ((((x (𝜔 × N) y (𝜔 × N)) (x (N × N) y (N × N))) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
185, 17bitri 173 . . . . 5 ((((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) (x (N × N) y (N × N))) ↔ ((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
19 eleq1 2097 . . . . . . . . . . . . . . . . . . 19 (x = ⟨z, w⟩ → (x (N × N) ↔ ⟨z, w (N × N)))
20 opelxp 4317 . . . . . . . . . . . . . . . . . . 19 (⟨z, w (N × N) ↔ (z N w N))
2119, 20syl6bb 185 . . . . . . . . . . . . . . . . . 18 (x = ⟨z, w⟩ → (x (N × N) ↔ (z N w N)))
22 eleq1 2097 . . . . . . . . . . . . . . . . . . 19 (y = ⟨v, u⟩ → (y (N × N) ↔ ⟨v, u (N × N)))
23 opelxp 4317 . . . . . . . . . . . . . . . . . . 19 (⟨v, u (N × N) ↔ (v N u N))
2422, 23syl6bb 185 . . . . . . . . . . . . . . . . . 18 (y = ⟨v, u⟩ → (y (N × N) ↔ (v N u N)))
2521, 24bi2anan9 538 . . . . . . . . . . . . . . . . 17 ((x = ⟨z, w y = ⟨v, u⟩) → ((x (N × N) y (N × N)) ↔ ((z N w N) (v N u N))))
2625pm5.32i 427 . . . . . . . . . . . . . . . 16 (((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) ↔ ((x = ⟨z, w y = ⟨v, u⟩) ((z N w N) (v N u N))))
2726anbi1i 431 . . . . . . . . . . . . . . 15 ((((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) (z ·𝑜 u) = (w ·𝑜 v)) ↔ (((x = ⟨z, w y = ⟨v, u⟩) ((z N w N) (v N u N))) (z ·𝑜 u) = (w ·𝑜 v)))
28 anass 381 . . . . . . . . . . . . . . 15 ((((x = ⟨z, w y = ⟨v, u⟩) ((z N w N) (v N u N))) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((x = ⟨z, w y = ⟨v, u⟩) (((z N w N) (v N u N)) (z ·𝑜 u) = (w ·𝑜 v))))
2927, 28bitri 173 . . . . . . . . . . . . . 14 ((((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((x = ⟨z, w y = ⟨v, u⟩) (((z N w N) (v N u N)) (z ·𝑜 u) = (w ·𝑜 v))))
30 mulpiord 6301 . . . . . . . . . . . . . . . . . 18 ((z N u N) → (z ·N u) = (z ·𝑜 u))
31 mulpiord 6301 . . . . . . . . . . . . . . . . . 18 ((w N v N) → (w ·N v) = (w ·𝑜 v))
3230, 31eqeqan12d 2052 . . . . . . . . . . . . . . . . 17 (((z N u N) (w N v N)) → ((z ·N u) = (w ·N v) ↔ (z ·𝑜 u) = (w ·𝑜 v)))
3332an42s 523 . . . . . . . . . . . . . . . 16 (((z N w N) (v N u N)) → ((z ·N u) = (w ·N v) ↔ (z ·𝑜 u) = (w ·𝑜 v)))
3433pm5.32i 427 . . . . . . . . . . . . . . 15 ((((z N w N) (v N u N)) (z ·N u) = (w ·N v)) ↔ (((z N w N) (v N u N)) (z ·𝑜 u) = (w ·𝑜 v)))
3534anbi2i 430 . . . . . . . . . . . . . 14 (((x = ⟨z, w y = ⟨v, u⟩) (((z N w N) (v N u N)) (z ·N u) = (w ·N v))) ↔ ((x = ⟨z, w y = ⟨v, u⟩) (((z N w N) (v N u N)) (z ·𝑜 u) = (w ·𝑜 v))))
3629, 35bitr4i 176 . . . . . . . . . . . . 13 ((((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((x = ⟨z, w y = ⟨v, u⟩) (((z N w N) (v N u N)) (z ·N u) = (w ·N v))))
37 anass 381 . . . . . . . . . . . . 13 ((((x = ⟨z, w y = ⟨v, u⟩) ((z N w N) (v N u N))) (z ·N u) = (w ·N v)) ↔ ((x = ⟨z, w y = ⟨v, u⟩) (((z N w N) (v N u N)) (z ·N u) = (w ·N v))))
3836, 37bitr4i 176 . . . . . . . . . . . 12 ((((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) (z ·𝑜 u) = (w ·𝑜 v)) ↔ (((x = ⟨z, w y = ⟨v, u⟩) ((z N w N) (v N u N))) (z ·N u) = (w ·N v)))
3926anbi1i 431 . . . . . . . . . . . 12 ((((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) (z ·N u) = (w ·N v)) ↔ (((x = ⟨z, w y = ⟨v, u⟩) ((z N w N) (v N u N))) (z ·N u) = (w ·N v)))
4038, 39bitr4i 176 . . . . . . . . . . 11 ((((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) (z ·𝑜 u) = (w ·𝑜 v)) ↔ (((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) (z ·N u) = (w ·N v)))
41 ancom 253 . . . . . . . . . . . 12 (((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) ↔ ((x (N × N) y (N × N)) (x = ⟨z, w y = ⟨v, u⟩)))
4241anbi1i 431 . . . . . . . . . . 11 ((((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) (z ·𝑜 u) = (w ·𝑜 v)) ↔ (((x (N × N) y (N × N)) (x = ⟨z, w y = ⟨v, u⟩)) (z ·𝑜 u) = (w ·𝑜 v)))
4341anbi1i 431 . . . . . . . . . . 11 ((((x = ⟨z, w y = ⟨v, u⟩) (x (N × N) y (N × N))) (z ·N u) = (w ·N v)) ↔ (((x (N × N) y (N × N)) (x = ⟨z, w y = ⟨v, u⟩)) (z ·N u) = (w ·N v)))
4440, 42, 433bitr3i 199 . . . . . . . . . 10 ((((x (N × N) y (N × N)) (x = ⟨z, w y = ⟨v, u⟩)) (z ·𝑜 u) = (w ·𝑜 v)) ↔ (((x (N × N) y (N × N)) (x = ⟨z, w y = ⟨v, u⟩)) (z ·N u) = (w ·N v)))
45 anass 381 . . . . . . . . . 10 ((((x (N × N) y (N × N)) (x = ⟨z, w y = ⟨v, u⟩)) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((x (N × N) y (N × N)) ((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
46 anass 381 . . . . . . . . . 10 ((((x (N × N) y (N × N)) (x = ⟨z, w y = ⟨v, u⟩)) (z ·N u) = (w ·N v)) ↔ ((x (N × N) y (N × N)) ((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))))
4744, 45, 463bitr3i 199 . . . . . . . . 9 (((x (N × N) y (N × N)) ((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((x (N × N) y (N × N)) ((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))))
48472exbii 1494 . . . . . . . 8 (vu((x (N × N) y (N × N)) ((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ vu((x (N × N) y (N × N)) ((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))))
49 19.42vv 1785 . . . . . . . 8 (vu((x (N × N) y (N × N)) ((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((x (N × N) y (N × N)) vu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
50 19.42vv 1785 . . . . . . . 8 (vu((x (N × N) y (N × N)) ((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))) ↔ ((x (N × N) y (N × N)) vu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))))
5148, 49, 503bitr3i 199 . . . . . . 7 (((x (N × N) y (N × N)) vu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((x (N × N) y (N × N)) vu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))))
52512exbii 1494 . . . . . 6 (zw((x (N × N) y (N × N)) vu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ zw((x (N × N) y (N × N)) vu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))))
53 19.42vv 1785 . . . . . 6 (zw((x (N × N) y (N × N)) vu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
54 19.42vv 1785 . . . . . 6 (zw((x (N × N) y (N × N)) vu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))) ↔ ((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))))
5552, 53, 543bitr3i 199 . . . . 5 (((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))))
5618, 55bitri 173 . . . 4 ((((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) (x (N × N) y (N × N))) ↔ ((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v))))
5756opabbii 3815 . . 3 {⟨x, y⟩ ∣ (((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) (x (N × N) y (N × N)))} = {⟨x, y⟩ ∣ ((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v)))}
58 df-enq 6331 . . 3 ~Q = {⟨x, y⟩ ∣ ((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v)))}
5957, 58eqtr4i 2060 . 2 {⟨x, y⟩ ∣ (((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) (x (N × N) y (N × N)))} = ~Q
603, 4, 593eqtrri 2062 1 ~Q = ( ~Q0 ∩ ((N × N) × (N × N)))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98   = wceq 1242  ∃wex 1378   ∈ wcel 1390   ∩ cin 2910   ⊆ wss 2911  ⟨cop 3370  {copab 3808  𝜔com 4256   × cxp 4286  (class class class)co 5455   ·𝑜 comu 5938  Ncnpi 6256   ·N cmi 6258   ~Q ceq 6263   ~Q0 ceq0 6270 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935 This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-xp 4294  df-rel 4295  df-res 4300  df-iota 4810  df-fv 4853  df-ov 5458  df-ni 6288  df-mi 6290  df-enq 6331  df-enq0 6406 This theorem is referenced by:  nqnq0pi  6420
 Copyright terms: Public domain W3C validator