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

Theorem xpcomco 6236
Description: Composition with the bijection of xpcomf1o 6235 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.)
Hypotheses
Ref Expression
xpcomf1o.1 𝐹 = (x (A × B) ↦ {x})
xpcomco.1 𝐺 = (y B, z A𝐶)
Assertion
Ref Expression
xpcomco (𝐺𝐹) = (z A, y B𝐶)
Distinct variable groups:   x,y,z,A   x,B,y,z   y,𝐹,z
Allowed substitution hints:   𝐶(x,y,z)   𝐹(x)   𝐺(x,y,z)

Proof of Theorem xpcomco
Dummy variables v u w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpcomf1o.1 . . . . . . . . . 10 𝐹 = (x (A × B) ↦ {x})
21xpcomf1o 6235 . . . . . . . . 9 𝐹:(A × B)–1-1-onto→(B × A)
3 f1ofun 5071 . . . . . . . . 9 (𝐹:(A × B)–1-1-onto→(B × A) → Fun 𝐹)
4 funbrfv2b 5161 . . . . . . . . 9 (Fun 𝐹 → (u𝐹w ↔ (u dom 𝐹 (𝐹u) = w)))
52, 3, 4mp2b 8 . . . . . . . 8 (u𝐹w ↔ (u dom 𝐹 (𝐹u) = w))
6 ancom 253 . . . . . . . 8 ((u dom 𝐹 (𝐹u) = w) ↔ ((𝐹u) = w u dom 𝐹))
7 eqcom 2039 . . . . . . . . 9 ((𝐹u) = ww = (𝐹u))
8 f1odm 5073 . . . . . . . . . . 11 (𝐹:(A × B)–1-1-onto→(B × A) → dom 𝐹 = (A × B))
92, 8ax-mp 7 . . . . . . . . . 10 dom 𝐹 = (A × B)
109eleq2i 2101 . . . . . . . . 9 (u dom 𝐹u (A × B))
117, 10anbi12i 433 . . . . . . . 8 (((𝐹u) = w u dom 𝐹) ↔ (w = (𝐹u) u (A × B)))
125, 6, 113bitri 195 . . . . . . 7 (u𝐹w ↔ (w = (𝐹u) u (A × B)))
1312anbi1i 431 . . . . . 6 ((u𝐹w w𝐺v) ↔ ((w = (𝐹u) u (A × B)) w𝐺v))
14 anass 381 . . . . . 6 (((w = (𝐹u) u (A × B)) w𝐺v) ↔ (w = (𝐹u) (u (A × B) w𝐺v)))
1513, 14bitri 173 . . . . 5 ((u𝐹w w𝐺v) ↔ (w = (𝐹u) (u (A × B) w𝐺v)))
1615exbii 1493 . . . 4 (w(u𝐹w w𝐺v) ↔ w(w = (𝐹u) (u (A × B) w𝐺v)))
17 vex 2554 . . . . . . 7 u V
181mptfvex 5199 . . . . . . 7 ((x {x} V u V) → (𝐹u) V)
1917, 18mpan2 401 . . . . . 6 (x {x} V → (𝐹u) V)
20 vex 2554 . . . . . . . . 9 x V
2120snex 3928 . . . . . . . 8 {x} V
2221cnvex 4799 . . . . . . 7 {x} V
2322uniex 4140 . . . . . 6 {x} V
2419, 23mpg 1337 . . . . 5 (𝐹u) V
25 breq1 3758 . . . . . 6 (w = (𝐹u) → (w𝐺v ↔ (𝐹u)𝐺v))
2625anbi2d 437 . . . . 5 (w = (𝐹u) → ((u (A × B) w𝐺v) ↔ (u (A × B) (𝐹u)𝐺v)))
2724, 26ceqsexv 2587 . . . 4 (w(w = (𝐹u) (u (A × B) w𝐺v)) ↔ (u (A × B) (𝐹u)𝐺v))
28 elxp 4305 . . . . . 6 (u (A × B) ↔ zy(u = ⟨z, y (z A y B)))
2928anbi1i 431 . . . . 5 ((u (A × B) (𝐹u)𝐺v) ↔ (zy(u = ⟨z, y (z A y B)) (𝐹u)𝐺v))
30 nfcv 2175 . . . . . . 7 z(𝐹u)
31 xpcomco.1 . . . . . . . 8 𝐺 = (y B, z A𝐶)
32 nfmpt22 5514 . . . . . . . 8 z(y B, z A𝐶)
3331, 32nfcxfr 2172 . . . . . . 7 z𝐺
34 nfcv 2175 . . . . . . 7 zv
3530, 33, 34nfbr 3799 . . . . . 6 z(𝐹u)𝐺v
363519.41 1573 . . . . 5 (z(y(u = ⟨z, y (z A y B)) (𝐹u)𝐺v) ↔ (zy(u = ⟨z, y (z A y B)) (𝐹u)𝐺v))
37 nfcv 2175 . . . . . . . . 9 y(𝐹u)
38 nfmpt21 5513 . . . . . . . . . 10 y(y B, z A𝐶)
3931, 38nfcxfr 2172 . . . . . . . . 9 y𝐺
40 nfcv 2175 . . . . . . . . 9 yv
4137, 39, 40nfbr 3799 . . . . . . . 8 y(𝐹u)𝐺v
424119.41 1573 . . . . . . 7 (y((u = ⟨z, y (z A y B)) (𝐹u)𝐺v) ↔ (y(u = ⟨z, y (z A y B)) (𝐹u)𝐺v))
43 anass 381 . . . . . . . . 9 (((u = ⟨z, y (z A y B)) (𝐹u)𝐺v) ↔ (u = ⟨z, y ((z A y B) (𝐹u)𝐺v)))
44 fveq2 5121 . . . . . . . . . . . . . 14 (u = ⟨z, y⟩ → (𝐹u) = (𝐹‘⟨z, y⟩))
45 opelxpi 4319 . . . . . . . . . . . . . . 15 ((z A y B) → ⟨z, y (A × B))
46 sneq 3378 . . . . . . . . . . . . . . . . . . 19 (x = ⟨z, y⟩ → {x} = {⟨z, y⟩})
4746cnveqd 4454 . . . . . . . . . . . . . . . . . 18 (x = ⟨z, y⟩ → {x} = {⟨z, y⟩})
4847unieqd 3582 . . . . . . . . . . . . . . . . 17 (x = ⟨z, y⟩ → {x} = {⟨z, y⟩})
49 vex 2554 . . . . . . . . . . . . . . . . . 18 z V
50 vex 2554 . . . . . . . . . . . . . . . . . 18 y V
51 opswapg 4750 . . . . . . . . . . . . . . . . . 18 ((z V y V) → {⟨z, y⟩} = ⟨y, z⟩)
5249, 50, 51mp2an 402 . . . . . . . . . . . . . . . . 17 {⟨z, y⟩} = ⟨y, z
5348, 52syl6eq 2085 . . . . . . . . . . . . . . . 16 (x = ⟨z, y⟩ → {x} = ⟨y, z⟩)
5450, 49opex 3957 . . . . . . . . . . . . . . . 16 y, z V
5553, 1, 54fvmpt 5192 . . . . . . . . . . . . . . 15 (⟨z, y (A × B) → (𝐹‘⟨z, y⟩) = ⟨y, z⟩)
5645, 55syl 14 . . . . . . . . . . . . . 14 ((z A y B) → (𝐹‘⟨z, y⟩) = ⟨y, z⟩)
5744, 56sylan9eq 2089 . . . . . . . . . . . . 13 ((u = ⟨z, y (z A y B)) → (𝐹u) = ⟨y, z⟩)
5857breq1d 3765 . . . . . . . . . . . 12 ((u = ⟨z, y (z A y B)) → ((𝐹u)𝐺v ↔ ⟨y, z𝐺v))
59 df-br 3756 . . . . . . . . . . . . . . . 16 (⟨y, z𝐺v ↔ ⟨⟨y, z⟩, v 𝐺)
60 df-mpt2 5460 . . . . . . . . . . . . . . . . . 18 (y B, z A𝐶) = {⟨⟨y, z⟩, v⟩ ∣ ((y B z A) v = 𝐶)}
6131, 60eqtri 2057 . . . . . . . . . . . . . . . . 17 𝐺 = {⟨⟨y, z⟩, v⟩ ∣ ((y B z A) v = 𝐶)}
6261eleq2i 2101 . . . . . . . . . . . . . . . 16 (⟨⟨y, z⟩, v 𝐺 ↔ ⟨⟨y, z⟩, v {⟨⟨y, z⟩, v⟩ ∣ ((y B z A) v = 𝐶)})
63 oprabid 5480 . . . . . . . . . . . . . . . 16 (⟨⟨y, z⟩, v {⟨⟨y, z⟩, v⟩ ∣ ((y B z A) v = 𝐶)} ↔ ((y B z A) v = 𝐶))
6459, 62, 633bitri 195 . . . . . . . . . . . . . . 15 (⟨y, z𝐺v ↔ ((y B z A) v = 𝐶))
6564baib 827 . . . . . . . . . . . . . 14 ((y B z A) → (⟨y, z𝐺vv = 𝐶))
6665ancoms 255 . . . . . . . . . . . . 13 ((z A y B) → (⟨y, z𝐺vv = 𝐶))
6766adantl 262 . . . . . . . . . . . 12 ((u = ⟨z, y (z A y B)) → (⟨y, z𝐺vv = 𝐶))
6858, 67bitrd 177 . . . . . . . . . . 11 ((u = ⟨z, y (z A y B)) → ((𝐹u)𝐺vv = 𝐶))
6968pm5.32da 425 . . . . . . . . . 10 (u = ⟨z, y⟩ → (((z A y B) (𝐹u)𝐺v) ↔ ((z A y B) v = 𝐶)))
7069pm5.32i 427 . . . . . . . . 9 ((u = ⟨z, y ((z A y B) (𝐹u)𝐺v)) ↔ (u = ⟨z, y ((z A y B) v = 𝐶)))
7143, 70bitri 173 . . . . . . . 8 (((u = ⟨z, y (z A y B)) (𝐹u)𝐺v) ↔ (u = ⟨z, y ((z A y B) v = 𝐶)))
7271exbii 1493 . . . . . . 7 (y((u = ⟨z, y (z A y B)) (𝐹u)𝐺v) ↔ y(u = ⟨z, y ((z A y B) v = 𝐶)))
7342, 72bitr3i 175 . . . . . 6 ((y(u = ⟨z, y (z A y B)) (𝐹u)𝐺v) ↔ y(u = ⟨z, y ((z A y B) v = 𝐶)))
7473exbii 1493 . . . . 5 (z(y(u = ⟨z, y (z A y B)) (𝐹u)𝐺v) ↔ zy(u = ⟨z, y ((z A y B) v = 𝐶)))
7529, 36, 743bitr2i 197 . . . 4 ((u (A × B) (𝐹u)𝐺v) ↔ zy(u = ⟨z, y ((z A y B) v = 𝐶)))
7616, 27, 753bitri 195 . . 3 (w(u𝐹w w𝐺v) ↔ zy(u = ⟨z, y ((z A y B) v = 𝐶)))
7776opabbii 3815 . 2 {⟨u, v⟩ ∣ w(u𝐹w w𝐺v)} = {⟨u, v⟩ ∣ zy(u = ⟨z, y ((z A y B) v = 𝐶))}
78 df-co 4297 . 2 (𝐺𝐹) = {⟨u, v⟩ ∣ w(u𝐹w w𝐺v)}
79 df-mpt2 5460 . . 3 (z A, y B𝐶) = {⟨⟨z, y⟩, v⟩ ∣ ((z A y B) v = 𝐶)}
80 dfoprab2 5494 . . 3 {⟨⟨z, y⟩, v⟩ ∣ ((z A y B) v = 𝐶)} = {⟨u, v⟩ ∣ zy(u = ⟨z, y ((z A y B) v = 𝐶))}
8179, 80eqtri 2057 . 2 (z A, y B𝐶) = {⟨u, v⟩ ∣ zy(u = ⟨z, y ((z A y B) v = 𝐶))}
8277, 78, 813eqtr4i 2067 1 (𝐺𝐹) = (z A, y B𝐶)
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98  wal 1240   = wceq 1242  wex 1378   wcel 1390  Vcvv 2551  {csn 3367  cop 3370   cuni 3571   class class class wbr 3755  {copab 3808  cmpt 3809   × cxp 4286  ccnv 4287  dom cdm 4288  ccom 4292  Fun wfun 4839  1-1-ontowf1o 4844  cfv 4845  {coprab 5456  cmpt2 5457
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-13 1401  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  ax-un 4136  ax-setind 4220
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-csb 2847  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-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator