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

Theorem xpiindim 4415
 Description: Distributive law for cross product over indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
Assertion
Ref Expression
xpiindim (y y A → (𝐶 × x A B) = x A (𝐶 × B))
Distinct variable groups:   x,y,A   x,𝐶,y
Allowed substitution hints:   B(x,y)

Proof of Theorem xpiindim
Dummy variables z w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relxp 4389 . . . . . 6 Rel (𝐶 × B)
21rgenw 2370 . . . . 5 x A Rel (𝐶 × B)
3 eleq1 2097 . . . . . . 7 (x = y → (x Ay A))
43cbvexv 1792 . . . . . 6 (x x Ay y A)
5 r19.2m 3303 . . . . . 6 ((x x A x A Rel (𝐶 × B)) → x A Rel (𝐶 × B))
64, 5sylanbr 269 . . . . 5 ((y y A x A Rel (𝐶 × B)) → x A Rel (𝐶 × B))
72, 6mpan2 401 . . . 4 (y y Ax A Rel (𝐶 × B))
8 reliin 4401 . . . 4 (x A Rel (𝐶 × B) → Rel x A (𝐶 × B))
97, 8syl 14 . . 3 (y y A → Rel x A (𝐶 × B))
10 relxp 4389 . . 3 Rel (𝐶 × x A B)
119, 10jctil 295 . 2 (y y A → (Rel (𝐶 × x A B) Rel x A (𝐶 × B)))
12 r19.28mv 3308 . . . . . . 7 (x x A → (x A (w 𝐶 z B) ↔ (w 𝐶 x A z B)))
134, 12sylbir 125 . . . . . 6 (y y A → (x A (w 𝐶 z B) ↔ (w 𝐶 x A z B)))
1413bicomd 129 . . . . 5 (y y A → ((w 𝐶 x A z B) ↔ x A (w 𝐶 z B)))
15 vex 2554 . . . . . . 7 z V
16 eliin 3652 . . . . . . 7 (z V → (z x A Bx A z B))
1715, 16ax-mp 7 . . . . . 6 (z x A Bx A z B)
1817anbi2i 430 . . . . 5 ((w 𝐶 z x A B) ↔ (w 𝐶 x A z B))
19 opelxp 4316 . . . . . 6 (⟨w, z (𝐶 × B) ↔ (w 𝐶 z B))
2019ralbii 2324 . . . . 5 (x Aw, z (𝐶 × B) ↔ x A (w 𝐶 z B))
2114, 18, 203bitr4g 212 . . . 4 (y y A → ((w 𝐶 z x A B) ↔ x Aw, z (𝐶 × B)))
22 opelxp 4316 . . . 4 (⟨w, z (𝐶 × x A B) ↔ (w 𝐶 z x A B))
23 vex 2554 . . . . . 6 w V
2423, 15opex 3956 . . . . 5 w, z V
25 eliin 3652 . . . . 5 (⟨w, z V → (⟨w, z x A (𝐶 × B) ↔ x Aw, z (𝐶 × B)))
2624, 25ax-mp 7 . . . 4 (⟨w, z x A (𝐶 × B) ↔ x Aw, z (𝐶 × B))
2721, 22, 263bitr4g 212 . . 3 (y y A → (⟨w, z (𝐶 × x A B) ↔ ⟨w, z x A (𝐶 × B)))
2827eqrelrdv2 4381 . 2 (((Rel (𝐶 × x A B) Rel x A (𝐶 × B)) y y A) → (𝐶 × x A B) = x A (𝐶 × B))
2911, 28mpancom 399 1 (y y A → (𝐶 × x A B) = x A (𝐶 × B))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301  Vcvv 2551  ⟨cop 3369  ∩ ciin 3648   × cxp 4285  Rel wrel 4292 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-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 3865  ax-pow 3917  ax-pr 3934 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-un 2916  df-in 2918  df-ss 2925  df-pw 3352  df-sn 3372  df-pr 3373  df-op 3375  df-iin 3650  df-opab 3809  df-xp 4293  df-rel 4294 This theorem is referenced by:  xpriindim  4416
 Copyright terms: Public domain W3C validator