HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem dmsnop 3323
Description: The domain of a singleton of an ordered pair is the singleton of the first member.
Assertion
Ref Expression
dmsnop |- dom {<.A, B>.} = {A}
Proof of Theorem dmsnop
StepHypRef Expression
1 visset 1809 . . . . . . . . 9 |- x e. V
2 visset 1809 . . . . . . . . 9 |- y e. V
31, 2opthg 2783 . . . . . . . 8 |- (B e. V -> (<.x, y>. = <.A, B>. <-> (x = A /\ y = B)))
4 opex 2777 . . . . . . . . 9 |- <.x, y>. e. V
54elsnc 2427 . . . . . . . 8 |- (<.x, y>. e. {<.A, B>.} <-> <.x, y>. = <.A, B>.)
63, 5syl5bb 531 . . . . . . 7 |- (B e. V -> (<.x, y>. e. {<.A, B>.} <-> (x = A /\ y = B)))
76exbidv 1277 . . . . . 6 |- (B e. V -> (E.y<.x, y>. e. {<.A, B>.} <-> E.y(x = A /\ y = B)))
8 19.42v 1306 . . . . . 6 |- (E.y(x = A /\ y = B) <-> (x = A /\ E.y y = B))
97, 8syl6bb 535 . . . . 5 |- (B e. V -> (E.y<.x, y>. e. {<.A, B>.} <-> (x = A /\ E.y y = B)))
10 isset 1810 . . . . . 6 |- (B e. V <-> E.y y = B)
11 iba 641 . . . . . 6 |- (E.y y = B -> (x = A <-> (x = A /\ E.y y = B)))
1210, 11sylbi 199 . . . . 5 |- (B e. V -> (x = A <-> (x = A /\ E.y y = B)))
139, 12bitr4d 530 . . . 4 |- (B e. V -> (E.y<.x, y>. e. {<.A, B>.} <-> x = A))
1413abbidv 1574 . . 3 |- (B e. V -> {x | E.y<.x, y>. e. {<.A, B>.}} = {x | x = A})
15 dfdm3 3297 . . 3 |- dom {<.A, B>.} = {x | E.y<.x, y>. e. {<.A, B>.}}
16 df-sn 2408 . . 3 |- {A} = {x | x = A}
1714, 15, 163eqtr4g 1528 . 2 |- (B e. V -> dom {<.A, B>.} = {A})
18 opprc2 2495 . . . 4 |- (-. B e. V -> <.A, B>. = <.A, A>.)
19 sneq 2413 . . . 4 |- (<.A, B>. = <.A, A>. -> {<.A, B>.} = {<.A, A>.})
20 dmeq 3306 . . . 4 |- ({<.A, B>.} = {<.A, A>.} -> dom {<.A, B>.} = dom {<.A, A>.})
2118, 19, 203syl 20 . . 3 |- (-. B e. V -> dom {<.A, B>.} = dom {<.A, A>.})
221, 2opthg 2783 . . . . . . . . . 10 |- (A e. V -> (<.x, y>. = <.A, A>. <-> (x = A /\ y = A)))
234elsnc 2427 . . . . . . . . . 10 |- (<.x, y>. e. {<.A, A>.} <-> <.x, y>. = <.A, A>.)
2422, 23syl5bb 531 . . . . . . . . 9 |- (A e. V -> (<.x, y>. e. {<.A, A>.} <-> (x = A /\ y = A)))
2524exbidv 1277 . . . . . . . 8 |- (A e. V -> (E.y<.x, y>. e. {<.A, A>.} <-> E.y(x = A /\ y = A)))
26 19.42v 1306 . . . . . . . 8 |- (E.y(x = A /\ y = A) <-> (x = A /\ E.y y = A))
2725, 26syl6bb 535 . . . . . . 7 |- (A e. V -> (E.y<.x, y>. e. {<.A, A>.} <-> (x = A /\ E.y y = A)))
28 isset 1810 . . . . . . . 8 |- (A e. V <-> E.y y = A)
29 iba 641 . . . . . . . 8 |- (E.y y = A -> (x = A <-> (x = A /\ E.y y = A)))
3028, 29sylbi 199 . . . . . . 7 |- (A e. V -> (x = A <-> (x = A /\ E.y y = A)))
3127, 30bitr4d 530 . . . . . 6 |- (A e. V -> (E.y<.x, y>. e. {<.A, A>.} <-> x = A))
3231abbidv 1574 . . . . 5 |- (A e. V -> {x | E.y<.x, y>. e. {<.A, A>.}} = {x | x = A})
33 dfdm3 3297 . . . . 5 |- dom {<.A, A>.} = {x | E.y<.x, y>. e. {<.A, A>.}}
3432, 33, 163eqtr4g 1528 . . . 4 |- (A e. V -> dom {<.A, A>.} = {A})
35 dmsnsn0 3320 . . . . 5 |- dom {{(/)}} = (/)
36 anidm 432 . . . . . . 7 |- ((-. A e. V /\ -. A e. V) <-> -. A e. V)
37 opprc3 2792 . . . . . . 7 |- ((-. A e. V /\ -. A e. V) <-> <.A, A>. = {(/)})
3836, 37bitr3 175 . . . . . 6 |- (-. A e. V <-> <.A, A>. = {(/)})
39 sneq 2413 . . . . . . 7 |- (<.A, A>. = {(/)} -> {<.A, A>.} = {{(/)}})
4039dmeqd 3308 . . . . . 6 |- (<.A, A>. = {(/)} -> dom {<.A, A>.} = dom {{(/)}})
4138, 40sylbi 199 . . . . 5 |- (-. A e. V -> dom {<.A, A>.} = dom {{(/)}})
42 snprc 2439 . . . . . 6 |- (-. A e. V <-> {A} = (/))
4342biimp 151 . . . . 5 |- (-. A e. V -> {A} = (/))
4435, 41, 433eqtr4a 1529 . . . 4 |- (-. A e. V -> dom {<.A, A>.} = {A})
4534, 44pm2.61i 126 . . 3 |- dom {<.A, A>.} = {A}
4621, 45syl6eq 1520 . 2 |- (-. B e. V -> dom {<.A, B>.} = {A})
4717, 46pm2.61i 126 1 |- dom {<.A, B>.} = {A}
Colors of variables: wff set class
Syntax hints:  -. wn 2   <-> wb 146   /\ wa 223   = wceq 954   e. wcel 956  E.wex 978  {cab 1461  Vcvv 1807  (/)c0 2276  {csn 2405  <.cop 2407  dom cdm 3165
This theorem is referenced by:  dmsnsnsn 3324  op1sta 3440  rnsnop 3442  f1osn 3710  tfrlem10 3911  ringsn 8115  1alg 10534  1ded 10551  1cat 10572
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-br 2615  df-dm 3183
Copyright terms: Public domain